topologicalClosure_map — Mathlib

English

Continuous star-algebra homomorphisms from a closed map preserve closures, yielding equality of the topological closure of the image and the image of the topological closure.

Русский

Непрерывные гомоморфизмы звездных алгебр сохраняют замыкания, давая равенство замыкания образа и образа замыкания.

LaTeX

$$Equality: $(\mathrm{map}\,\phi\ s)^{\text{top.closure}} = \mathrm{map}\,\phi\ s^{\text{top.closure}}$$$

Lean4

theorem topologicalClosure_map [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A)
    (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap φ) (hφ' : Continuous φ) :
    (map φ s).topologicalClosure = map φ s.topologicalClosure :=
  SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _

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