Commit 2024-08-07 14:53 6c05c5da

View on Github →

feat(Calculus/MeanValue): A function is not differentiable if its derivative tends to infinity (#15200) This PR shows that a function f : ℝ → ℝ is not differentiable at a point if its derivative tends to infinity at that point.

Estimated changes

Modified Mathlib/Analysis/Calculus/MeanValue.lean

added theorem exists_deriv_eq_slope'

added theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio

added theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi

added theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio

added theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi

Modified Mathlib/Topology/Order/LeftRightNhds.lean

added theorem nhdsWithin_Iio_basis