Commit 2025-10-24 15:50 f9c58afb

View on Github →

feat: isProperMap_fst_of_compactSpace, IsProperMap.restrictPreimage (#30410)

Estimated changes

Modified Mathlib/Topology/Compactness/Compact.lean

deleted theorem isClosedMap_fst_of_compactSpace

deleted theorem isClosedMap_snd_of_compactSpace

Modified Mathlib/Topology/IsClosedRestrict.lean

Modified Mathlib/Topology/LocalAtTarget.lean

added theorem IsProperMap.restrictPreimage

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

added theorem isClosedMap_fst_of_compactSpace

added theorem isClosedMap_snd_of_compactSpace

added theorem isProperMap_const

added theorem isProperMap_const_iff

added theorem isProperMap_fst_of_compactSpace

added theorem isProperMap_snd_of_compactSpace