deriv_sub — Mathlib

English

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

Русский

Если f и g дифференцируемы в точке x, то производная от f − g в точке x равна разности их производных в x.

LaTeX

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

Lean4

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

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