Theorem Monotone.countable_not_continuousWithinAt_Ioi
Modification history
2025-06-19 19:44
Mathlib/Topology/Order/LeftRightLim.lean
feat: more API for monotone functions wrt topology (#26113)
Deleted Monotone.countable_not_continuousWithinAt_IoiView on Github →