map_topologicalClosure_le — Mathlib

English

For a continuous φ, the image of the topological closure of s is contained in the topological closure of the image of s.

Русский

При непрерывном отображении φ образ топологического замыкания s содержится в топологическом замыкании образа s.

LaTeX

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

Lean4

theorem map_topologicalClosure_le (hφ : Continuous φ) : map φ s.topologicalClosure ≤ (map φ s).topologicalClosure :=
  image_closure_subset_closure_image hφ

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