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]
[CompactlyCoherentSpace Y]
{f : X → Y}
:
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]
[CompactlyCoherentSpace Y]
{f : X → 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)