iteratedDeriv_succ' — Mathlib

English

The (n+1)-st iterated derivative equals the n-th iterated derivative of the derivative: iteratedDeriv (n+1) f = iteratedDeriv n (deriv f).

Русский

Пусть (n+1)-я итеративная производная равна n-й итеративной производной от производной: iteratedDeriv (n+1) f = iteratedDeriv n (deriv f).

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; iteratedDeriv (n+1) f = iteratedDeriv n (deriv f)$$$

Lean4

/-- The `n+1`-th iterated derivative can be obtained by taking the `n`-th derivative of the
derivative. -/
theorem iteratedDeriv_succ' : iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f) := by
  rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate, Function.iterate_succ_apply]

Похожие утверждения