Commit 2025-07-15 08:52 3d1fc475

View on Github →

fix(Topology/Covering): switch to standard definition (#24983) As discussed in [#mathlib4 > edge cases not covered by `IsCoveringMap` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.

Estimated changes