Commit 2023-05-28 20:08 5e71308b

View on Github →

feat: add lemmas about closed and quotient maps (#4455) Forward-port of leanprover-community/mathlib#19071

Estimated changes

Modified Mathlib/Topology/Maps.lean

added theorem IsClosedMap.to_quotientMap

modified theorem quotientMap_iff

added theorem quotientMap_iff_closed

Modified Mathlib/Topology/Separation.lean

deleted theorem Continuous.isClosedMap

added theorem QuotientMap.of_surjective_continuous