English
OpenNormalSubgroup G carries a natural partial order by inclusion.
Русский
OpenNormalSubgroup G имеет естественный частичный порядок по включению.
LaTeX
$$instPartialOrderOpenNormalSubgroup: PartialOrder(OpenNormalSubgroup(G))$$
Lean4
/-- A subgroup of an archimedean linear ordered multiplicative commutative group with order
topology is dense provided that for all `ε > 1` there exists an element of the subgroup
that belongs to `(1, ε)`. -/
@[to_additive /-- An additive subgroup of an archimedean linear ordered additive commutative group
with order topology is dense provided that for all positive `ε` there exists a positive element of
the subgroup that is less than `ε`. -/
]
theorem dense_of_not_isolated_one (S : Subgroup G) (hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε) : Dense (S : Set G) :=
by
cases subsingleton_or_nontrivial G
· refine fun x => _root_.subset_closure ?_
rw [Subsingleton.elim x 1]
exact one_mem S
refine dense_of_exists_between fun a b hlt => ?_
rcases hS (b / a) (one_lt_div'.2 hlt) with ⟨g, hgS, hg0, hg⟩
rcases (existsUnique_add_zpow_mem_Ioc hg0 1 a).exists with ⟨m, hm⟩
rw [one_mul] at hm
refine ⟨g ^ m, zpow_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
rwa [lt_div_iff_mul_lt'] at hg
