topologicalClosure_map_le — Mathlib

English

If φ is a closed map, then the topological closure of the image of s is contained in the image under φ of the topological closure of s.

Русский

Если отображение φ является закрытым отображением, то замыкание образа s содержится в образе замыкания s.

LaTeX

$$For a closed map $\phi$, $(\mathrm{map} \phi\ s)^{\text{top.closure}} \le \mathrm{map} \phi\ (s^{\text{top.closure}})$$$

Lean4

theorem topologicalClosure_map_le [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A)
    (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap φ) : (map φ s).topologicalClosure ≤ map φ s.topologicalClosure :=
  hφ.closure_image_subset _

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