closure_image_subset — Mathlib

English

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

Русский

Для замкнутого отображения f замыкание образа множества s вложено в образ замыкания s.

LaTeX

$$$IsClosedMap(f) \\to \\forall s, \\overline{f''s} \\subseteq f''\\overline{s}$$$

Lean4

theorem closure_image_subset (hf : IsClosedMap f) (s : Set X) : closure (f '' s) ⊆ f '' closure s :=
  closure_minimal (image_mono subset_closure) (hf _ isClosed_closure)

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