iteratedFDeriv_zero_fun — Mathlib

English

The iterated derivative of the zero function is zero for all orders.

Русский

Итерационная производная нулевой функции равна нулю для всех порядков.

LaTeX

$$$\\forall i, \\ iteratedFDerivWithin 𝕜 i (\\lambda _ : E. 0)\\ s = 0$$$

Lean4

@[simp]
theorem iteratedFDeriv_zero_fun {n : ℕ} : (iteratedFDeriv 𝕜 n fun _ : E ↦ (0 : F)) = 0 :=
  funext fun x ↦ by simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_zero_fun]

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