iteratedDerivWithin_fun_add — Mathlib

English

Within s, the nth iterated derivative of f + g equals the sum of nth iterated derivatives of f and g, given differentiability conditions at x.

Русский

Внутри s n-я повторная производная для f+g равна сумме n-й повторной производной f и g при заданных условиях дифференцируемости в x.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (f+g)\\ s\\ x = \\operatorname{iteratedDerivWithin}_n f\\ s\\ x + \\operatorname{iteratedDerivWithin}_n g\\ s\\ x$$

Lean4

theorem iteratedDerivWithin_fun_add (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
    iteratedDerivWithin n (fun z ↦ f z + g z) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x := by
  simpa using iteratedDerivWithin_add hx h hf hg

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