Theorem isClosedMap_fst_of_compactSpace

Modification history

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 →