Theorem Topology.IsInducing.IsQuotientMap.of_comp_of_eq_coinduced

Modification history

2026-04-01 14:12
Mathlib/Topology/Maps/Basic.lean
refactor(Topology): redefine `Topology.IsQuotientMap` with `Topology.IsCoinducing` (#36957) …
Deleted Topology.IsInducing.IsQuotientMap.of_comp_of_eq_coinducedView on Github →
2025-12-22 22:40
Mathlib/Topology/Maps/Basic.lean
feat: covering maps from properly discontinuous actions and discrete subgroups (#7596)
Added Topology.IsInducing.IsQuotientMap.of_comp_of_eq_coinducedView on Github →