Mathlib Changelog
v4
Changelog
About
Github
Theorem
isClosedMap_restrict_of_compactSpace
Modification history
2025-03-28 10:45
Mathlib/Topology/IsClosedRestrict.lean
feat: the restriction of a closed compact set to a subset of coordinates is closed (#22687) …
Added
isClosedMap_restrict_of_compactSpace
View on Github →