iteratedDeriv_const_sub — Mathlib

English

If 0 < n, adding a constant to f does not change the nth iterated derivative within s at x.

Русский

Если 0 < n, прибавление константы к f не меняет n-ю повторную производную внутри s в x.

LaTeX

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

Lean4

theorem iteratedDeriv_const_sub (hn : 0 < n) (c : F) : iteratedDeriv n (fun z => c - f z) x = iteratedDeriv n (-f) x :=
  by simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_sub hn c

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