English
The (topological-space) closure of a subgroup of a topological group is itself a subgroup.
Русский
Замыкание подгруппы в топологической группе является самой подгруппой.
LaTeX
$$$def\ topologicalClosure(s:\ Subgroup G) : Subgroup G$ with $s.topologicalClosure$ is a subgroup$$
Lean4
/-- The (topological-space) closure of a subgroup of a topological group is
itself a subgroup. -/
@[to_additive /-- The (topological-space) closure of an additive subgroup of an additive topological group is
itself an additive subgroup. -/
]
def topologicalClosure (s : Subgroup G) : Subgroup G :=
{ s.toSubmonoid.topologicalClosure with
carrier := _root_.closure (s : Set G)
inv_mem' := fun {g} hg => by simpa only [← Set.mem_inv, inv_closure, inv_coe_set] using hg }
