frontier under an open map (#11189)

Commit

4 years ago

feat(topology/maps): preimage of closure/frontier under an open map (#11189) We had lemmas about `interior`. Add versions about `frontier` and `closure`.

Author

urkud

Parents

8f391aa5

mathlib 71dc1eab - feat(topology/maps): preimage of closure/frontier under an open map (#11189)

mathlib
71dc1eab - feat(topology/maps): preimage of closure/frontier under an open map (#11189)