Topology on archimedean groups and fields

In this file we prove the following theorems:

• Rat.denseRange_cast: the coercion from ℚ to a linear ordered archimedean field has dense range;

• AddSubgroup.dense_of_not_isolated_zero, AddSubgroup.dense_of_no_min: two sufficient conditions for a subgroup of an archimedean linear ordered additive commutative group to be dense;

• AddSubgroup.dense_or_cyclic: an additive subgroup of an archimedean linear ordered additive commutative group G with order topology either is dense in G or is a cyclic subgroup.

theorem Rat.denseRange_cast {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [Archimedean 𝕜] : DenseRange Rat.cast

Rational numbers are dense in a linear ordered archimedean field.

theorem Subgroup.dense_of_not_isolated_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) (hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Set.Ioo 1 ε) : Dense ↑S

A subgroup of an archimedean linear ordered multiplicative commutative group with order topology is dense provided that for all ε > 1 there exists an element of the subgroup that belongs to (1, ε).

theorem AddSubgroup.dense_of_not_isolated_zero {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) (hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Set.Ioo 0 ε) : Dense ↑S

An additive subgroup of an archimedean linear ordered additive commutative group with order topology is dense provided that for all positive ε there exists a positive element of the subgroup that is less than ε.

theorem Subgroup.dense_of_no_min {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) (hbot : S ≠ ⊥) (H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a) : Dense ↑S

Let S be a nontrivial subgroup in an archimedean linear ordered multiplicative commutative group G with order topology. If the set of elements of S that are greater than one does not have a minimal element, then S is dense G.

theorem AddSubgroup.dense_of_no_min {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) (hbot : S ≠ ⊥) (H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 0 < g} a) : Dense ↑S

Let S be a nontrivial additive subgroup in an archimedean linear ordered additive commutative group G with order topology. If the set of positive elements of S does not have a minimal element, then S is dense G.