commMonoidTopologicalClosure — Mathlib

English

If a Submonoid is commutative, then its topological closure is a commutative monoid.

Русский

Если подмножество моноида коммутативно, то его топологическое замыкание образует коммутативный моноид.

LaTeX

$$commMonoidTopologicalClosure\left(s\right)$$

Lean4

/-- If a submonoid of a topological monoid is commutative, then so is its topological closure. -/
@[to_additive /-- If a submonoid of an additive topological monoid is commutative, then so is its
    topological closure.

    See note [reducible non-instances]. -/
    ]
abbrev commMonoidTopologicalClosure [T2Space M] (s : Submonoid M) (hs : ∀ x y : s, x * y = y * x) :
    CommMonoid s.topologicalClosure :=
  { s.topologicalClosure.toMonoid, s.toSubsemigroup.commSemigroupTopologicalClosure hs with }

Похожие утверждения