AddSubgroup.dense_of_not_isolated_zero
theorem AddSubgroup.dense_of_not_isolated_zero :
∀ {G : Type u_1} [inst : LinearOrderedAddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : OrderTopology G]
[inst_3 : Archimedean G] (S : AddSubgroup G), (∀ ε > 0, ∃ g ∈ S, g ∈ Set.Ioo 0 ε) → Dense ↑S
This theorem states that in the context of an archimedean linear ordered additive commutative group with an order topology, an additive subgroup is dense if for every positive real number `ε`, there exists a positive element in the subgroup that is strictly between 0 and `ε`. Here, "dense" means that every point in the group belongs to the closure of the subgroup, "closure" being a topological concept that includes all the limit points of the subgroup. In simpler terms, we can get as close as we want to any point in the group by using elements of the subgroup, as long as we can find an element of the subgroup that is smaller than any given positive distance.
More concisely: In an archimedean linear ordered additive commutative group with an order topology, a subgroup is dense if for every positive real number `ε`, it contains an element strictly between 0 and `ε`.
|
AddSubgroup.dense_of_no_min
theorem AddSubgroup.dense_of_no_min :
∀ {G : Type u_1} [inst : LinearOrderedAddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : OrderTopology G]
[inst_3 : Archimedean G] (S : AddSubgroup G), S ≠ ⊥ → (¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a) → Dense ↑S
This theorem states that in an archimedean linear ordered additive commutative group `G` with order topology, if `S` is a nontrivial additive subgroup of `G` and if there is no minimal element in the set of positive elements of `S`, then `S` is dense in `G`. Here, a set being dense means that every point in `G` belongs to the closure of `S`. A set having no minimal element means that there does not exist an element in the set which is less than or equal to every other element in the set.
More concisely: In an archimedean linear ordered additive commutative group with order topology, a nontrivial subgroup without a minimal positive element is dense.
|
Rat.denseRange_cast
theorem Rat.denseRange_cast :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜]
[inst_3 : Archimedean 𝕜], DenseRange Rat.cast
This theorem states that the rational numbers are dense in any linear ordered Archimedean field. More specifically, it means that given any such field 𝕜, which is equipped with a linear order, a topological space structure, and an order topology, and is also Archimedean, the image of the function which casts rational numbers into 𝕜 forms a dense set. In other words, for every element in 𝕜, no matter how small a neighborhood we consider around that element, there will always be some rational number within that neighborhood.
More concisely: In any Archimedean linear ordered field with a topology, the rational numbers forms a dense subset.
|
AddSubgroup.dense_or_cyclic
theorem AddSubgroup.dense_or_cyclic :
∀ {G : Type u_1} [inst : LinearOrderedAddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : OrderTopology G]
[inst_3 : Archimedean G] (S : AddSubgroup G), Dense ↑S ∨ ∃ a, S = AddSubgroup.closure {a}
The theorem `AddSubgroup.dense_or_cyclic` asserts that for any additive subgroup `S` of an Archimedean linear ordered additive commutative group `G` equipped with an order topology, either the subgroup `S` is dense in `G` or `S` is a cyclic subgroup. In the latter case, this means that there exists an element `a` in the group such that the subgroup `S` is the additive subgroup generated by the set containing just `a`.
More concisely: In an Archimedean linear ordered additive commutative group equipped with an order topology, every proper dense-free additive subgroup is cyclic.
|