English
In a topological group G, for any subset s, the topological closure of the subgroup generated by s equals the topological closure of the submonoid generated by s.
Русский
В топологической группе G замыкание подгруппы, порождаемой множеством s, совпадает с замыканием подмоноида, порождаемого s.
LaTeX
$$$ (\\mathrm{Subgroup.closure} \\; s).topologicalClosure = (\\mathrm{Submonoid.closure} \\; s).topologicalClosure$$$
Lean4
@[to_additive]
theorem topologicalClosure_subgroupClosure_toSubmonoid (s : Set G) :
(Subgroup.closure s).toSubmonoid.topologicalClosure = (Submonoid.closure s).topologicalClosure :=
by
refine le_antisymm ?_ (closure_mono <| Subgroup.le_closure_toSubmonoid _)
refine Submonoid.topologicalClosure_minimal _ ?_ isClosed_closure
rw [Subgroup.closure_toSubmonoid, Submonoid.closure_le]
refine union_subset (Submonoid.subset_closure.trans subset_closure) fun x hx ↦ ?_
refine closure_mono (Submonoid.powers_le.2 (Submonoid.subset_closure <| Set.mem_inv.1 hx)) ?_
rw [Submonoid.coe_powers, ← closure_range_zpow_eq_pow, ← Subgroup.coe_zpowers, ← Subgroup.topologicalClosure_coe,
SetLike.mem_coe, ← inv_mem_iff]
exact subset_closure <| Subgroup.mem_zpowers _
