Theorem nhdsWithin_Iio_basis

Modification history

2024-12-23 08:37
Mathlib/Topology/Order/LeftRightNhds.lean
chore(*): rename lemmas about `𝓝[≥] a` etc (#20188) …
Deleted nhdsWithin_Iio_basisView on Github →
2024-08-07 14:53
Mathlib/Topology/Order/LeftRightNhds.lean
feat(Calculus/MeanValue): A function is not differentiable if its derivative tends to infinity (#15200) …
Added nhdsWithin_Iio_basisView on Github →