Theorems · Theorem · order theory

AddSubgroup.dense_or_cyclic

∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : 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.

Defined in

Mathlib.Topology.Algebra.Order.Archimedean

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidTopologicalSpaceOrderTopologyArchimedean