Theorems · Theorem · order theory

Subgroup.dense_of_no_min

∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] (S : Subgroup G), S ≠ ⊥ → (¬∃ a, IsLeast {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.

Defined in

Mathlib.Topology.Algebra.Order.Archimedean

Cited by

0 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupLinearOrderIsOrderedMonoidTopologicalSpaceOrderTopologyMulArchimedean