Commit 2024-12-12 18:16 54c954e5

View on Github →

refactor(fderiv): redefine fderivWithin and fderiv (#19694) Prefer 0 answer whenever it's possible. This way, fderivWithin_const is true without extra assumptions.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

modified theorem iteratedFDerivWithin_const_of_ne

modified theorem iteratedFDerivWithin_succ_const

modified theorem iteratedFDerivWithin_zero_fun

Modified Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

modified theorem derivWithin_const

Modified Mathlib/Analysis/Calculus/Deriv/Slope.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Add.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

added theorem fderivWithin_const

modified theorem fderivWithin_const_apply