Commit 2024-04-02 16:26 68ab53e5

View on Github →

feat: add image_restrictPreimage (#11640)

add the theorem image_restrictPreimage; use it to simplify the proof of Set.restrictPreimage_isClosedMap
add the equivalent for open maps Set.restrictPreimage_isOpenMap.
delete IsClosedMap.restrictPreimage, which duplicates Set.restrictPreimage_isClosedMap

Estimated changes

Modified Mathlib/Data/Set/Function.lean

added theorem Set.image_restrictPreimage

Modified Mathlib/Topology/Constructions.lean

deleted theorem IsClosedMap.restrictPreimage

Modified Mathlib/Topology/LocalAtTarget.lean

added theorem IsClosedMap.restrictPreimage

added theorem IsOpenMap.restrictPreimage

added theorem Set.restrictPreimage_isOpenMap