Commit 2023-07-21 14:16 88fb181b

View on Github →

feat(Topology.Constructions): restriction of a closed map (#6013)

Estimated changes

Modified Mathlib/Data/Set/Function.lean

added theorem Set.MapsTo.restrict_commutes

Modified Mathlib/Topology/Constructions.lean

added theorem IsClosedMap.restrictPreimage

Modified Mathlib/Topology/Maps.lean

added theorem isClosedMap_iff_clusterPt