Documentation

Mathlib.Topology.Algebra.Order.Archimedean

Topology on archimedean groups and fields #

In this file we prove the following theorems:

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 : ε > 0, gS, 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 : 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.

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.