English
Let X, Y be topological spaces with Y Hausdorff. A map f: X → Y is proper if and only if f is continuous, closed, and for every cofinite subset of Y, its preimage under f is cocompact in X (equivalently, f tends to the cofinite filter along the cocompact filter on X).
Русский
Пусть X, Y — топологические пространства, Y удовлетворяет условию Т₂. Тогда отображение f: X → Y проперно тогда и только тогда, когда оно непрерывно, замкнуто и выполняется свойство стремления к кофинитному фильтруру: Tendsto f (cocompact X) cofinite.
LaTeX
$$$IsProperMap(f) \\quad\\Longleftrightarrow\\quad Continuous(f) \\land IsClosedMap(f) \\land Tendsto\\,f\\,(cocompact\\,X)\\,cofinite$$$
Lean4
/-- Version of `isProperMap_iff_isClosedMap_and_compact_fibers` in terms of `cofinite` and
`cocompact`. Only works when the codomain is `T1`. -/
theorem isProperMap_iff_isClosedMap_and_tendsto_cofinite [T1Space Y] :
IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite :=
by
simp_rw [isProperMap_iff_isClosedMap_and_compact_fibers, Tendsto, le_cofinite_iff_compl_singleton_mem, mem_map,
preimage_compl]
refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦ ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩
rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩
exact hK.of_isClosed_subset (isClosed_singleton.preimage f_cont) (compl_le_compl_iff_le.mp hKy)
