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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [Archimedean 𝕜] : DenseRange Rat.cast

Rational numbers are dense in a linear ordered archimedean field.

theorem AddSubgroup.dense_of_not_isolated_zero {G : Type u_1} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) (hS : ∀ (ε : G), ε > 0 → ∃ g, 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 AddSubgroup.dense_of_no_min {G : Type u_1} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) (hbot : S ≠ ⊥) (H : ¬∃ a, IsLeast {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.

theorem AddSubgroup.dense_or_cyclic {G : Type u_1} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) : Dense ↑S ∨ ∃ a, S = AddSubgroup.closure {a}

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.