English
In a nontrivial densely ordered archimedean topological group G, a subgroup is either dense or cyclic, but not both. More precisely, for every subgroup S ≤ G, exactly one of the two holds: S is dense in G or S is cyclic (generated by some a ∈ G).
Русский
В неособой densely упорядоченной архимедовой топологической группе G подгруппа либо плотна в G, либо циклическая, но не обе одновременно.
LaTeX
$$$\text{Dense}(S) \;\oplus\; \exists a\in G,\; S = \langle a\rangle.$$$
Lean4
/-- In a nontrivial densely linear ordered archimedean topological multiplicative group,
a subgroup is either dense or is cyclic, but not both.
For a non-exclusive `Or` version with weaker assumptions, see `Subgroup.dense_or_cyclic` above. -/
@[to_additive dense_xor'_cyclic /-- In a nontrivial densely linear ordered archimedean topological additive group,
a subgroup is either dense or is cyclic, but not both.
For a non-exclusive `Or` version with weaker assumptions, see `AddSubgroup.dense_or_cyclic` above.
-/
]
theorem dense_xor'_cyclic (s : Subgroup G) : Xor' (Dense (s : Set G)) (∃ a, s = .zpowers a) := by
if hd : Dense (s : Set G) then
simp only [hd, xor_true]
rintro ⟨a, rfl⟩
exact not_denseRange_zpow hd
else
simp only [hd, xor_false, id, zpowers_eq_closure]
exact s.dense_or_cyclic.resolve_left hd
