Commit 2024-09-28 09:50 488d6b54

View on Github →

feat(Topology): define IsOpenQuotientMap (#16549)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Constructions.lean

added theorem IsOpenQuotientMap.prodMap

Modified Mathlib/Topology/Defs/Basic.lean

added structure IsOpenQuotientMap

Created Mathlib/Topology/Maps/OpenQuotient.lean

added theorem IsOpenQuotientMap.comp

added theorem IsOpenQuotientMap.continuousAt_comp_iff

added theorem IsOpenQuotientMap.continuous_comp_iff

added theorem IsOpenQuotientMap.iff_isOpenMap_quotientMap

added theorem IsOpenQuotientMap.map_nhds_eq

added theorem IsOpenQuotientMap.of_isOpenMap_quotientMap

added theorem IsOpenQuotientMap.quotientMap