iteratedDeriv_eq_iteratedFDeriv — Mathlib

English

The nth iterated derivative within s equals the nth iterate of the derivWithin operator starting from f.

Русский

(n)-я итеративная производная внутри s равна (n)-му итерационному применению оператора derivWithin к f.

LaTeX

$$$\operatorname{iteratedDeriv} n f x = \bigl(\operatorname{derivWithin} f s\bigr)^{[n]}(x)$$$

Lean4

theorem iteratedDeriv_eq_iteratedFDeriv :
    iteratedDeriv n f x = (iteratedFDeriv 𝕜 n f x : (Fin n → 𝕜) → F) fun _ : Fin n => 1 :=
  rfl

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