iteratedFDeriv_neg_apply — Mathlib

English

For every i, iteratedFDeriv 𝕜 i (-f) x = - iteratedFDeriv 𝕜 i f x.

Русский

Для любого i выполняется D^i(-f)(x) = - D^i f(x).

LaTeX

$$$\operatorname{iteratedFDeriv}_{\mathbb{K}} i (-f) x = - \operatorname{iteratedFDeriv}_{\mathbb{K}} i f x$$$

Lean4

theorem iteratedFDeriv_neg_apply {i : ℕ} {f : E → F} : iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x :=
  by
  simp_rw [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)

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