English
The (n+1)-st iterated derivative of f is the derivative of the n-th iterated derivative: iteratedDeriv (n+1) f = deriv (iteratedDeriv n f).
Русский
Пусть f имеет n+1 производную. Тогда (n+1)-я итеративная производная равна производной от n-ой итеративной производной: iteratedDeriv (n+1) f = deriv (iteratedDeriv n f).
LaTeX
$$$\\forall n \\in \\mathbb{N},\\; iteratedDeriv (n+1) f = deriv (iteratedDeriv n f)$$$
Lean4
/-- The `n+1`-th iterated derivative can be obtained by differentiating the `n`-th
iterated derivative. -/
theorem iteratedDeriv_succ : iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f) :=
by
ext x
rw [← iteratedDerivWithin_univ, ← iteratedDerivWithin_univ, ← derivWithin_univ]
exact iteratedDerivWithin_succ
