iteratedDerivWithin_sub — Mathlib

English

Within s, iteratedDerivWithin of the Pi-negated function equals the negation of iteratedDerivWithin of the original function.

Русский

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

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (\\Pi.neg f) s x = -\\operatorname{iteratedDerivWithin}_n f s x$$$

Lean4

theorem iteratedDerivWithin_sub (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
    iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x := by
  rw [sub_eq_add_neg, sub_eq_add_neg, Pi.neg_def, iteratedDerivWithin_add hx h hf hg.neg, iteratedDerivWithin_fun_neg]

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