Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_closed_map.to_quotient_map

Modification history

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