Documentation

Mathlib.Topology.Maps.Proper.CompactlyGenerated

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.

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)

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)