Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous.is_closed_map

Modification history

2023-05-25 22:47
src/topology/separation.lean
feat(topology/{maps,separation}): add lemmas about closed and quotient maps (#19071) …
Deleted continuous.is_closed_mapView on Github →
2021-02-07 23:41
src/topology/separation.lean
feat(topology/separation): an injective map on a compact space is an embedding (#6057)
Added continuous.is_closed_mapView on Github →