Theorem derivWithin_const

Modification history

2024-12-12 18:16
Mathlib/Analysis/Calculus/Deriv/Basic.lean
refactor(fderiv): redefine `fderivWithin` and `fderiv` (#19694) …
Modified derivWithin_constView on Github →
2023-05-28 04:44
Mathlib/Analysis/Calculus/Deriv/Basic.lean
feat: port Analysis.Calculus.Deriv.Basic (#4434)
Added derivWithin_constView on Github →