iteratedDerivWithin_fun_neg — Mathlib

English

Within s, the nth iterated derivative of the negated function equals the negation of the nth iterated derivative of the original function.

Русский

Внутри s n-я повторная производная от отрицательной функции равна отрицанию n-й повторной производной исходной функции.

LaTeX

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

Lean4

theorem iteratedDerivWithin_fun_neg : iteratedDerivWithin n (fun z => -f z) s x = -iteratedDerivWithin n f s x :=
  iteratedDerivWithin_neg f

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