topologicalClosure — Mathlib

English

For NonUnitalStarSubalgebra, the closure of the image under a closed star-map equals the image of the closure.

Русский

Для NonUnitalStarSubalgebra замыкание образа при замкнутом звездном отображении равно изображению замыкания.

LaTeX

$$$\overline{\operatorname{map}_φ(S)} = \operatorname{map}_φ(\overline{S})$$$

Lean4

/-- The (topological) closure of a non-unital star subalgebra of a non-unital topological star
algebra is itself a non-unital star subalgebra. -/
def topologicalClosure (s : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra R A :=
  {
    s.toNonUnitalSubalgebra.topologicalClosure with
    star_mem' := fun h ↦ map_mem_closure continuous_star h fun _ ↦ star_mem
    carrier := _root_.closure (s : Set A) }

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