iteratedDeriv_fun_neg — Mathlib

English

If f is 0< n, the nth iterated derivative within s of c - f z equals the nth iterated derivative within s of -f z.

Русский

Если n > 0, n-я повторная производная внутри s от c - f z равна n-й повторной производной внутри s от -f z.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (\\lambda z. c - f z) s x = \\operatorname{iteratedDerivWithin}_n (\\lambda z. -f z) s x$$

Lean4

theorem iteratedDeriv_fun_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) :
    iteratedDeriv n (fun x ↦ -(f x)) a = -(iteratedDeriv n f a) := by
  simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f

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