A map is proper iff preimage of compact sets are compact

This file proves that if Y is a Hausdorff and compactly generated space, a continuous map f : X → Y is proper if and only if preimage of compact sets are compact.

theorem isProperMap_iff_isCompact_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] [CompactlyGeneratedSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)

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_tendsto_cocompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] [CompactlyGeneratedSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)

Version of isProperMap_iff_isCompact_preimage in terms of cocompact.

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)