English
IsClosedMap f is equivalent to comap-nhds inequality for nhds on Y.
Русский
IsClosedMap f эквивалентно неравенству comap-nhds для nhds на Y.
LaTeX
$$$IsClosedMap f \\iff ∀ {s : Set Y}, comap f (𝓝 s) ≤ 𝓝ˢ (f^{-1} s)$$$
Lean4
/-- A map `f : X → Y` is closed if and only if for all sets `s`, any cluster point of `f '' s` is
the image by `f` of some cluster point of `s`.
If you require this for all filters instead of just principal filters, and also that `f` is
continuous, you get the notion of **proper map**. See `isProperMap_iff_clusterPt`. -/
theorem isClosedMap_iff_clusterPt : IsClosedMap f ↔ ∀ s y, MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s) :=
by simp [MapClusterPt, isClosedMap_iff_closure_image, subset_def, mem_closure_iff_clusterPt, and_comm]
