English
If a subgroup s of a topological group G is commutative (abelian), then its topological closure is a commutative group.
Русский
Если подгруппа s в топологической группе G коммутативна, то её топологическое замыкание тоже коммутативно.
LaTeX
$$$\text{CommGroup} (s.topologicalClosure)$$$
Lean4
/-- If a subgroup of a topological group is commutative, then so is its topological closure.
See note [reducible non-instances]. -/
@[to_additive /-- If a subgroup of an additive topological group is commutative, then so is its
topological closure.
See note [reducible non-instances]. -/
]
abbrev commGroupTopologicalClosure [T2Space G] (s : Subgroup G) (hs : ∀ x y : s, x * y = y * x) :
CommGroup s.topologicalClosure :=
{ s.topologicalClosure.toGroup, s.toSubmonoid.commMonoidTopologicalClosure hs with }
