Theorem iteratedFDerivWithin_const_of_ne

Modification history

2024-12-12 18:16

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

refactor(fderiv): redefine `fderivWithin` and `fderiv` (#19694) …

Modified iteratedFDerivWithin_const_of_ne View on Github →

2024-02-20 08:45

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

feat: Basic theorems for iteratedFDerivWithin (#10733) …

Added iteratedFDerivWithin_const_of_ne View on Github →