Commit 2024-07-22 09:09 262ae9e7

View on Github →

feat: Characterization of proper maps for Hausdorff and compactly generated spaces (#13635) A continuous map whose codomain is a Hausdorff and compactly generated space is proper if and only if the preimages of compact sets are compact. A Hausdorff and weakly locally compact space is compactly generated. A Hausdorff and sequential space is compactly generated.

Estimated changes

Modified Mathlib/Topology/Maps/Proper/Basic.lean

added theorem SequentialSpace.isProperMap_iff_isCompact_preimage

added theorem SequentialSpace.isProperMap_iff_tendsto_cocompact

added theorem WeaklyLocallyCompactSpace.isProperMap_iff_isCompact_preimage

added theorem WeaklyLocallyCompactSpace.isProperMap_iff_tendsto_cocompact

added theorem compactlyGenerated_of_sequentialSpace

added theorem compactlyGenerated_of_weaklyLocallyCompactSpace

modified theorem isProperMap_iff_isCompact_preimage

modified theorem isProperMap_iff_tendsto_cocompact