isOpenMap_iff_kernImage — Mathlib

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]

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