Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quotient_map.of_surjective_continuous

Modification history

2023-05-25 22:47
src/topology/separation.lean
feat(topology/{maps,separation}): add lemmas about closed and quotient maps (#19071) …
Added quotient_map.of_surjective_continuousView on Github →