map_topologicalClosure_le — Mathlib

English

If φ is closed and continuous, then the closure of the image equals the image of the closure.

Русский

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

LaTeX

$$(map φ s).topologicalClosure = map φ s.topologicalClosure$$

Lean4

theorem map_topologicalClosure_le [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A)
    (φ : A →⋆ₐ[R] B) (hφ : Continuous φ) : map φ s.topologicalClosure ≤ (map φ s).topologicalClosure :=
  image_closure_subset_closure_image hφ

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