image_closure_subset_closure_image

English

For a continuous map f, the image of the closure of s is contained in the closure of the image of s.

Русский

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

LaTeX

$$$f \\text{ continuous} \\Rightarrow f[\\overline{s}] \\subseteq \\overline{f[s]}$$$

Lean4

/-- See also `IsClosedMap.closure_image_eq_of_continuous`. -/
theorem image_closure_subset_closure_image (h : Continuous f) : f '' closure s ⊆ closure (f '' s) :=
  ((mapsTo_image f s).closure h).image_subset

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