topologicalClosure_map_le — Mathlib

English

If φ is a closed map, then the closure of the image is contained in the image of the closure: cl(φ(S)) ⊆ φ(cl(S)).

Русский

Если отображение φ замкнутое, то замыкание образа содержится в образе замыкания: cl(φ(S)) ⊆ φ(cl(S)).

LaTeX

$$$\overline{\phi(S)} \subseteq \phi(\overline{S})$$$

Lean4

theorem topologicalClosure_map_le (hφ : IsClosedMap φ) : (map φ s).topologicalClosure ≤ map φ s.topologicalClosure :=
  hφ.closure_image_subset _

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