deriv_fun_add — Mathlib

English

If f and g are differentiable at x, then deriv (f + g) x = deriv f x + deriv g x.

Русский

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

LaTeX

$$$\text{DifferentiableAt } f x \land \text{DifferentiableAt } g x \Rightarrow \ deriv (f + g) x = deriv f x + deriv g x$$$

Lean4

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

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