Theorem SeparationQuotient.isOpenQuotientMap_mk

Modification history

2024-09-28 23:34
Mathlib/Topology/Inseparable.lean
feat(SeparationQuotient): add missing instances (#17239) …
Added SeparationQuotient.isOpenQuotientMap_mkView on Github →