LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.Instances.AddCircle

`continuous_right_toIcoMod` theorem continuous_right_toIcoMod : ∀ {𝕜 : Type u_1} [inst : LinearOrderedAddCommGroup 𝕜] [inst_1 : Archimedean 𝕜] [inst_2 : TopologicalSpace 𝕜] [inst_3 : OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜), ContinuousWithinAt (toIcoMod hp a) (Set.Ici x) x This theorem states that for any linear ordered additive commutative group `𝕜` (which is also Archimedean and a topological space under an order topology) and any positive real number `p`, the function `toIcoMod` with parameters `hp` and `a`, is continuous at any point `x` within the interval from `x` to positive infinity (denoted by `Set.Ici x`). In mathematical terms, as `x` approaches a certain value within the specified interval, the value of `toIcoMod hp a` (which reduces the input to the interval `[a, a+p)`) also approaches its value at that certain value. This essentially encapsulates the idea of continuity within a specific range in the context of topological spaces. More concisely: For any Archimedean, additively commutative, topological linear ordered group `𝕜` and positive real number `p`, the function `toIcoMod` with parameters `hp` and `a` is continuous on `Set.Ici x` for any `x`.
`AddCircle.coe_image_Ico_eq` theorem AddCircle.coe_image_Ico_eq : ∀ {𝕜 : Type u_1} [inst : LinearOrderedAddCommGroup 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜], QuotientAddGroup.mk '' Set.Ico a (a + p) = Set.univ This theorem states that for any linearly ordered additive commutative group `𝕜` with an associated topological space and an order topology, given a positive element `p` of `𝕜` and any element `a` of `𝕜`, the image of the left-closed right-open interval from `a` to `a + p` under the quotient map from `𝕜` to the additive quotient group `𝕜 ⧸ p` covers the entire space. This holds true when the group `𝕜` satisfies the Archimedean property. In mathematical terms, it states that the image of the interval `[a, a + p)` under the quotient map is the entire set of `𝕜 ⧸ p`. More concisely: For any Archimedean linearly ordered additive commutative group `𝕜` with an order topology, the image of every left-closed right-open interval under the quotient map covers the entire additive quotient group.
`AddCircle.coe_image_Icc_eq` theorem AddCircle.coe_image_Icc_eq : ∀ {𝕜 : Type u_1} [inst : LinearOrderedAddCommGroup 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜], QuotientAddGroup.mk '' Set.Icc a (a + p) = Set.univ The theorem `AddCircle.coe_image_Icc_eq` states that for any type `𝕜` which is a linearly ordered additive commutative group, a topological space, has order topology, and is Archimedean, for any real number `p` greater than zero, and for any number `a` in this type `𝕜`, the image of the closed interval `[a, a+p]` under the quotient map (the map from an additive group to the quotient of the additive group by an additive subgroup) is the set of all elements of the type `𝕜`. In other words, every element of `𝕜` can be represented as the image of some element in the interval `[a, a+p]` under the quotient map. More concisely: For any Archimedean, linearly ordered additive commutative group `𝕜` with order topology and positive real number `p`, every element in `𝕜` is the image of some element in the interval `[a, a+p]` under the quotient map.
`AddCircle.coe_image_Ioc_eq` theorem AddCircle.coe_image_Ioc_eq : ∀ {𝕜 : Type u_1} [inst : LinearOrderedAddCommGroup 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜], QuotientAddGroup.mk '' Set.Ioc a (a + p) = Set.univ This theorem states that for any type `𝕜` which forms a linear ordered additive commutative group, a topological space, and it is archimedean; and for any positive real number `p` and any element `a` in `𝕜`, the image of the half-open interval (closed on the left and open on the right), denoted `[a, a + p)`, under the quotient map from `𝕜` to the additive circle group `AddCircle p`, covers the entire space `𝕜`. In simpler terms, every point in the space `𝕜` can be mapped from a point in the interval `[a, a + p)` via the quotient map. More concisely: For any archimedean, additively commutative group `𝕜` with a linear order and the topology of an additive abelian group, and for any `a` in `𝕜` and positive real number `p`, the quotient map from `[a, a + p)` to the additive circle group `AddCircle p` is surjective.
`AddCircle.continuous_mk'` theorem AddCircle.continuous_mk' : ∀ {𝕜 : Type u_1} [inst : LinearOrderedAddCommGroup 𝕜] [inst_1 : TopologicalSpace 𝕜] (p : 𝕜), Continuous ⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) This theorem, named `AddCircle.continuous_mk'`, states that for any given type `𝕜` which is a linearly ordered additive commutative group with a topological space structure, the additive group homomorphism from `𝕜` to the quotient group `𝕜/p𝕜` (where `p𝕜` is the subgroup generated by an element `p`) is continuous. Here, continuity is defined in the topological sense. This theorem basically links group theory and topology, asserting the continuity property of the mapping from a group to its quotient group with respect to a particular subgroup. More concisely: The additive group homomorphism from a linearly ordered additive commutative group equipped with a topology to its quotient group by a subgroup is continuous.
`continuous_left_toIocMod` theorem continuous_left_toIocMod : ∀ {𝕜 : Type u_1} [inst : LinearOrderedAddCommGroup 𝕜] [inst_1 : Archimedean 𝕜] [inst_2 : TopologicalSpace 𝕜] [inst_3 : OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜), ContinuousWithinAt (toIocMod hp a) (Set.Iic x) x This theorem states that for any type `𝕜` that forms a linear ordered additive commutative group, is Archimedean, and has a topological space structure with an order topology, and for any positive real number `p`, and two arbitrary elements `a` and `x` of type `𝕜`, the function `toIocMod` with parameters `hp` and `a` is continuous at the point `x` within the set of all elements less than or equal to `x` in the order of type `𝕜`. In simpler terms, if we are moving towards `x` only through values less than or equal to `x`, then `toIocMod` function will always move continuously without jumps or disruptions. More concisely: For any Archimedean, linearly ordered, additively commutative topological group `𝕜` and real number `p`, the function `toIocMod p` is continuous on the set of elements less than or equal to any given element `x` in `𝕜`.