[Merged by Bors] - feat(Topology): restriction of a QuotientMap

[urkud]

... to the preimage of an open set is a quotient map.

---

[github-actions]

PR summary 0668fd7d31

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ QuotientMap.continuousOn_isOpen_iff
+ QuotientMap.restrictPreimage_isOpen
+ image_val_preimage_restrictPreimage
+ preimage_restrictPreimage
+ restrictPreimage_mk

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style