Theorem isClosedMap_fst_of_compactSpace

Modification history

2025-10-24 15:50
Mathlib/Topology/Compactness/Compact.lean
feat: `isProperMap_fst_of_compactSpace`, `IsProperMap.restrictPreimage` (#30410)
Modified isClosedMap_fst_of_compactSpaceView on Github →
2023-11-30 20:57
Mathlib/Topology/Compactness/Compact.lean
chore(Topology/{Compactness/Compact}, Irreducible}): rename type variables (#7591) …
Modified isClosedMap_fst_of_compactSpaceView on Github →
2023-10-26 12:30
Mathlib/Topology/Compactness/Compact.lean
feat: `Prod.fst : X × Y → X` is a closed map if `Y` is compact (#7936) …
Added isClosedMap_fst_of_compactSpaceView on Github →