Theorem ContDiffOn.continuousOn_iteratedDerivWithin

Modification history

2024-11-25 11:42

Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

feat: extend `ContDiff` to take a smoothness exponent in `WithTop ℕ∞` (#19442) …

Modified ContDiffOn.continuousOn_iteratedDerivWithin View on Github →

2023-06-01 10:18

Mathlib/Analysis/Calculus/IteratedDeriv.lean

feat: port Analysis.Calculus.IteratedDeriv (#4545)

Added ContDiffOn.continuousOn_iteratedDerivWithin View on Github →