Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-25 22:47 d91e7f7a

View on Github →

feat(topology/{maps,separation}): add lemmas about closed and quotient maps (#19071) Lemma statements are from Shamrock-Frost/BrouwerFixedPoint

Estimated changes

Modified src/topology/maps.lean

added theorem is_closed_map.to_quotient_map

modified theorem quotient_map_iff

added theorem quotient_map_iff_closed

Modified src/topology/separation.lean

deleted theorem continuous.is_closed_map

added theorem quotient_map.of_surjective_continuous