feat: add `image_restrictPreimage`

[BGuillemet]

trafficstars

• 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

---

This PR adds the theorem image_restrictPreimage and uses it to simplify the proof of Set.restrictPreimage_isClosedMap. It also adds the equivalent for open maps Set.restrictPreimage_isOpenMap. The duplicate IsClosedMap.restrictPreimage of Set.restrictPreimage_isClosedMap has been deleted.