iteratedFDerivWithin_zero_fun — Mathlib

English

The (n+1)st iterated derivative of a constant function is zero.

Русский

Потомность (n+1)-я производная константы есть ноль.

LaTeX

$$$\\operatorname{iteratedFDerivWithin} 𝕜 (n+1) (\\lambda _ : E, c) \\, s = 0$$$

Lean4

@[simp]
theorem iteratedFDerivWithin_zero_fun {i : ℕ} : iteratedFDerivWithin 𝕜 i (fun _ : E ↦ (0 : F)) s = 0 := by
  cases i with
  | zero => ext; simp
  | succ i => apply iteratedFDerivWithin_succ_const

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