Theorem coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing

Modification history

2025-05-13 16:40
Mathlib/Topology/Maps/OpenQuotient.lean
feat(Topology): subspace of quotient topology is quotient of subspace topology (#23527)
Added coinduced_eq_induced_of_isOpenQuotientMap_of_isInducingView on Github →