fderiv_fun_add — Mathlib

English

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

Русский

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

LaTeX

$$$\displaystyle fderiv 𝕜 (f+g) x = fderiv 𝕜 f x + fderiv 𝕜 g x.$$$

Lean4

theorem fderiv_fun_add (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (fun y => f y + g y) x = fderiv 𝕜 f x + fderiv 𝕜 g x :=
  (hf.hasFDerivAt.add hg.hasFDerivAt).fderiv

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