Theorem IsCoveringMapOn.of_isCoveringMap_restrictPreimage

Modification history

2025-12-15 21:03
Mathlib/Topology/Covering/Basic.lean
feat(Topology): IsCoveringMapOn ↔ IsCoveringMap restrictPreimage (#27197)
Added IsCoveringMapOn.of_isCoveringMap_restrictPreimageView on Github →