fun_add — Mathlib

English

If f and g are differentiable at x, then the derivative of f + g at x is the sum of the derivatives: deriv(f+g)(x) = deriv f(x) + deriv g(x).

Русский

Если f и 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

nonrec theorem fun_add (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) : HasDerivAt (fun x ↦ f x + g x) (f' + g') x :=
  hf.add hg

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