fderivWithin_add — Mathlib

English

If f and g are differentiable within s at x, then fderivWithin of f+g at s,x equals sum of fderivWithin of f and g at s,x.

Русский

Если f и g дифференцируемы внутри s в x, то fderivWithin(f+g) = fderivWithin f + fderivWithin g.

LaTeX

$$$\displaystyle fderivWithin 𝕜 (f+g) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x$$$

Lean4

theorem fderivWithin_add (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) : fderivWithin 𝕜 (f + g) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x :=
  fderivWithin_fun_add hxs hf hg

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