English
Let G be a commutative archimedean linearly ordered topological group with the order topology. For every subgroup S ≤ G, either S is dense in G (i.e., its closure is G), or there exists a ∈ G such that S equals the closure of the cyclic subgroup generated by a, i.e., S = cl⟨a⟩.
Русский
Пусть G — коммутативная архимедова линейно упорядоченная топологическая группа с топологией порядка. Для любой подгруппы S ≤ G либо S плотно в G (закрытие S равно G), либо существует a ∈ G, такое что S равно замкнутой циклической подгруппе, порожденной a, то есть S = cl⟨a⟩.
LaTeX
$$$\overline{S} = G \;\lor\; \exists a \in G,\; S = \overline{\langle a \rangle}.$$$
Lean4
/-- A subgroup of an archimedean linear ordered multiplicative commutative group `G` with order
topology either is dense in `G` or is a cyclic subgroup. -/
@[to_additive 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 dense_or_cyclic (S : Subgroup G) : Dense (S : Set G) ∨ ∃ a : G, S = closure { a } :=
by
refine (em _).imp (dense_of_not_isolated_one S) fun h => ?_
push_neg at h
rcases h with ⟨ε, ε1, hε⟩
exact cyclic_of_isolated_one ε1 (disjoint_left.2 hε)
