fderiv_add — Mathlib

English

Same sum rule for fderivWithin as for fderiv: derivative within s of f+g equals sum of derivatives within s of f and g.

Русский

То же правило для fderivWithin: производная внутри s от f+g равна сумме производных внутри s.

LaTeX

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

Lean4

theorem fderiv_add (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (f + g) x = fderiv 𝕜 f x + fderiv 𝕜 g x :=
  fderiv_fun_add hf hg

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