deriv_fun_sub — Mathlib

English

If f and g are differentiable at x, then the derivative of f − g at x equals the derivative of f at x minus the derivative of g at x.

Русский

Пусть f и g дифференцируемы в точке x. Тогда производная от f − g в x равна производной f в x минус производная g в x.

LaTeX

$$$$ \operatorname{deriv}(f - g) x = \operatorname{deriv} f x - \operatorname{deriv} g x. $$$$

Lean4

@[simp]
theorem deriv_fun_sub (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    deriv (fun y ↦ f y - g y) x = deriv f x - deriv g x :=
  (hf.hasDerivAt.sub hg.hasDerivAt).deriv

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