feat: add `image_restrictPreimage`

[BGuillemet]

• 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.

[grunweg]

Welcome to mathlib and thank you for your contribution!

Is your pull request ready for review? Then you can label it awaiting-review, so reviewers will look at it :-) (Have you seen the contribution guidelines already? They explain this detail under "Lifecycle of a PR".)

I took the liberty to tweak your PR title and description a bit: for instance, the paragraph you wrote below the line could (imho) also go into the commit message.

[BGuillemet]

Thank you very much for your advice! I hadn't seen the contribution guidelines, so I read it and added the awaiting-review label.

[fpvandoorn]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style