Commit 2025-12-09 19:21 e62d5b59

View on Github →

feat: add ContDiffAt.continuousAt_fderiv etc (#32319)

Estimated changes

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

added theorem ContDiffAt.continuousAt_fderiv

added theorem ContDiffAt.continuousAt_iteratedFDeriv

added theorem ContDiffWithinAt.continuousWithinAt_fderivWithin

added theorem ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin

added theorem ContinuousOn.continuousOn_iteratedFDeriv

added theorem ContinuousOn.continuousOn_iteratedFDerivWithin