topologicalClosure_map_le — Mathlib

English

If φ is a closed map, then the closure of the image is contained in the image of the closure: (map φ s).topologicalClosure ≤ map φ s.topologicalClosure.

Русский

Если φ замкнутое отображение, то замыкание образа включено в образ замыкания: (map φ s).topologicalClosure ≤ map φ s.topologicalClosure.

LaTeX

$$$(map\ φ\ s).topologicalClosure \le map\ φ\ s.topologicalClosure$$$

Lean4

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

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