fderivWithin_fun_add — Mathlib

English

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

Русский

Если f и g дифференцируемы внутри s в x, то производная внутри множества от суммы равна сумме производных внутри множества.

LaTeX

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

Lean4

theorem fderivWithin_fun_add (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) :
    fderivWithin 𝕜 (fun y => f y + g y) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x :=
  (hf.hasFDerivWithinAt.add hg.hasFDerivWithinAt).fderivWithin hxs

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