English
If a subsemigroup is commutative, then its topological closure is a commutative semigroup.
Русский
Если подполугруппа коммутативна, то и её топологическое замыкание образует коммутативную полугруппу.
LaTeX
$$commSemigroupTopologicalClosure\left(s\right) : commutative$$
Lean4
/-- If a subsemigroup of a topological semigroup is commutative, then so is its topological
closure.
See note [reducible non-instances] -/
@[to_additive /-- If a submonoid of an additive topological monoid is commutative, then so is its
topological closure.
See note [reducible non-instances] -/
]
abbrev commSemigroupTopologicalClosure [T2Space M] (s : Subsemigroup M) (hs : ∀ x y : s, x * y = y * x) :
CommSemigroup s.topologicalClosure :=
{ MulMemClass.toSemigroup s.topologicalClosure with
mul_comm :=
have : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x := fun x hx y hy => congr_arg Subtype.val (hs ⟨x, hx⟩ ⟨y, hy⟩)
fun ⟨x, hx⟩ ⟨y, hy⟩ =>
Subtype.ext <| eqOn_closure₂ this continuous_mul (continuous_snd.mul continuous_fst) x hx y hy }
