English
A map f is closed if and only if for all open sets u, kernImage f u is open.
Русский
Отображение f замкнуто тогда и только тогда, когда для каждого открытого множества u верно, что kernImage f u открыто.
LaTeX
$$$IsClosedMap f \\iff \\forall {u}, IsOpen u \\rightarrow IsOpen (kernImage f u)$$$
Lean4
/-- A map is closed if and only if the `Set.kernImage` of every *open* set is open.
One way to understand this result is that `f : X → Y` is closed if and only if its fibers vary in an
**upper hemicontinuous** way: for any open subset `U ⊆ X`, the set of all `y ∈ Y` such that
`f ⁻¹' {y} ⊆ U` is open in `Y`. -/
theorem isClosedMap_iff_kernImage : IsClosedMap f ↔ ∀ {u : Set X}, IsOpen u → IsOpen (kernImage f u) :=
by
rw [IsClosedMap, compl_surjective.forall]
simp [kernImage_eq_compl]
