topologicalClosure_star_comm — Mathlib

English

The topological closure of a star-subalgebra commutes with the star operation, i.e., the star of the closure equals the closure of the star.

Русский

Замыкание звездо-подалгебры коммутирует со звездой: звезда замыкания равна замыканию звезды.

LaTeX

$$"star" of s.topologicalClosure equals (star s).topologicalClosure$$

Lean4

theorem _root_.Subalgebra.topologicalClosure_star_comm (s : Subalgebra R A) :
    (star s).topologicalClosure = star s.topologicalClosure :=
  by
  suffices ∀ t : Subalgebra R A, (star t).topologicalClosure ≤ star t.topologicalClosure from
    le_antisymm (this s) (by simpa only [star_star] using Subalgebra.star_mono (this (star s)))
  exact fun t =>
    (star t).topologicalClosure_minimal (Subalgebra.star_mono subset_closure)
      (isClosed_closure.preimage continuous_star)

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