Commit 2025-05-13 16:40 400dde68

View on Github →

feat(Topology): subspace of quotient topology is quotient of subspace topology (#23527)

Estimated changes

Modified Mathlib/Topology/Maps/OpenQuotient.lean

added theorem coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing

added theorem isEmbedding_of_isOpenQuotientMap_of_isInducing

added theorem isQuotientMap_of_isOpenQuotientMap_of_isInducing