Theorem Topology.IsInducing.IsQuotientMap.of_comp_isQuotientMap

Modification history

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_isQuotientMapView on Github →