English
A map f is open if and only if for every s ⊆ X, the closure of kernImage f s is contained in kernImage f of the closure of s; i.e., closure (kernImage f s) ⊆ kernImage f (closure s).
Русский
Отображение f открыто тогда и только тогда, когда для любого s ⊆ X замыкание kernImage f s содержится в kernImage f (closure s).
LaTeX
$$$\\text{Open}(f) \\iff ∀{s ⊆ X}, \\ \\overline{\\operatorname{kernImage} f s} \\subseteq \\operatorname{kernImage} f (\\overline{s})$$$
Lean4
/-- A map is open if and only if the `Set.kernImage` of every *closed* set is closed. -/
theorem isOpenMap_iff_closure_kernImage :
IsOpenMap f ↔ ∀ {s : Set X}, closure (kernImage f s) ⊆ kernImage f (closure s) :=
by
rw [isOpenMap_iff_image_interior, compl_surjective.forall]
simp [kernImage_eq_compl]
