deriv_add — Mathlib

English

For differentiable within s, the derivative within s of f + g equals the within-s derivative of f plus that of g.

Русский

Для дифференцируемых внутри s функций сумма производной внутри s равна сумме производных внутри s.

LaTeX

$$$\text{DifferentiableWithinAt } f s x \land \text{DifferentiableWithinAt } g s x \Rightarrow \ derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x$$$

Lean4

@[simp]
theorem deriv_add (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    deriv (f + g) x = deriv f x + deriv g x :=
  (hf.hasDerivAt.add hg.hasDerivAt).deriv

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