English
If a subgroup H of a linearly ordered commutative group is disjoint with the interval (1, a) for some a > 1, then H is cyclic.
Русский
Если подгруппа H линейно упорядоченной коммутативной группы не пересекает интервал (1, a) для некоторого a > 1, то H циклична.
LaTeX
$$$ H = \overline{\langle b \rangle} \quad \text{for some } b. $$$
Lean4
/-- If a subgroup of a linear ordered commutative group is disjoint with the
interval `Set.Ioo 1 a` for some `1 < a`, then this is a cyclic subgroup. -/
@[to_additive AddSubgroup.cyclic_of_isolated_zero /-- If an additive subgroup of a linear ordered
additive commutative group is disjoint with the interval `Set.Ioo 0 a` for some positive `a`, then
this is a cyclic subgroup. -/
]
theorem cyclic_of_isolated_one {H : Subgroup G} {a : G} (h₀ : 1 < a) (hd : Disjoint (H : Set G) (Ioo 1 a)) :
∃ b, H = closure { b } := by
rcases eq_or_ne H ⊥ with rfl | hbot
· exact ⟨1, closure_singleton_one.symm⟩
· exact (exists_isLeast_one_lt hbot h₀ hd).imp fun _ => cyclic_of_min
