English
An open map is characterized by the closedness of kernImage of closed sets.
Русский
Открытое отображение эквивалентно тому, что kernImage отображения сохраняет замкнутые множества.
LaTeX
$$$$IsOpenMap(f) \\leftrightarrow \\forall \\{u : Set X\\}, IsClosed(u) \\rightarrow IsClosed( kernImage(f, u) )$$$$
Lean4
theorem isOpenMap_iff_kernImage : IsOpenMap f ↔ ∀ {u : Set X}, IsClosed u → IsClosed (kernImage f u) :=
by
rw [IsOpenMap, compl_surjective.forall]
simp [kernImage_eq_compl]