Theorem Monotone.countable_not_continuousWithinAt_Iio
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_IioView on Github →