commSemiringTopologicalClosure — Mathlib

English

Same as above in a version stated for Subalgebra.topologicalClosure_comap_homeomorph.

Русский

То же самое в версии для Subalgebra.topologicalClosure_comap_homeomorph.

LaTeX

$$$ s.topologicalClosure.comap f = (s.comap f).topologicalClosure $$$

Lean4

/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.

See note [reducible non-instances]. -/
abbrev commSemiringTopologicalClosure [T2Space A] (s : Subalgebra R A) (hs : ∀ x y : s, x * y = y * x) :
    CommSemiring s.topologicalClosure :=
  { s.topologicalClosure.toSemiring, s.toSubmonoid.commMonoidTopologicalClosure hs with }

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