English
If the codomain Y is Hausdorff and compactly generated, then a map f: X → Y is proper iff it is continuous and the preimage of every compact set is compact.
Русский
Если \(Y\) Хаусдорфово и компактно порождаемое, тогда отображение \(f:X→Y\) пропорно тогда и только тогда, когда оно непрерывно и образ предобраза любой компактной множество является компактным.
LaTeX
$$$IsProperMap(f) \\iff (Continuous(f) \\land \\forall K\\subseteq Y, IsCompact(K) \\rightarrow IsCompact(f^{-1}(K)))$$$
Lean4
/-- If `Y` is Hausdorff and compactly generated, then proper maps `X → Y` are exactly
continuous maps such that the preimage of any compact set is compact. This is in particular true
if `Y` is Hausdorff and sequential or locally compact.
There was an older version of this theorem which was changed to this one to make use
of the `CompactlyGeneratedSpace` typeclass. (since 2024-11-10) -/
theorem isProperMap_iff_isCompact_preimage : IsProperMap f ↔ Continuous f ∧ ∀ ⦃K⦄, IsCompact K → IsCompact (f ⁻¹' K)
where
mp hf := ⟨hf.continuous, fun _ ↦ hf.isCompact_preimage⟩
mpr := fun ⟨hf, h⟩ ↦
isProperMap_iff_isClosedMap_and_compact_fibers.2
⟨hf, fun _ hs ↦
CompactlyGeneratedSpace.isClosed fun _ hK ↦
image_inter_preimage .. ▸ (((h hK).inter_left hs).image hf).isClosed,
fun _ ↦ h isCompact_singleton⟩
