closure_image_eq — Mathlib

English

For a closed embedding f and any set s, closure of the image equals the image of the closure.

Русский

Для замкнутого вложения f и любого множества s замыкание образа совпадает с образом замыкания: closure(f''s) = f''closure(s).

LaTeX

$$$\mathrm{closure}(f''s) = f''\mathrm{closure}(s)$$$

Lean4

theorem closure_image_eq (hf : IsClosedEmbedding f) (s : Set X) : closure (f '' s) = f '' closure s :=
  hf.isClosedMap.closure_image_eq_of_continuous hf.continuous s

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