closure_image_eq_of_continuous — Mathlib

English

Let f be a closed map and continuous. Then for every subset s of X, the closure of the image f''s equals the image of the closure of s: cl(f''s) = f''cl(s).

Русский

Пусть f — замкнутое отображение и непрерывно. Тогда для любого подмножества s ⊆ X выполняется равенство замыкания образа: cl(f''s) = f''cl(s).

LaTeX

$$$ \overline{f''S} = f''\overline{S} $$$

Lean4

theorem closure_image_eq_of_continuous (f_closed : IsClosedMap f) (f_cont : Continuous f) (s : Set X) :
    closure (f '' s) = f '' closure s :=
  subset_antisymm (f_closed.closure_image_subset s) (image_closure_subset_closure_image f_cont)

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