fderiv_fun_sub — Mathlib

English

The classical derivative of a difference equals the difference of derivatives.

Русский

Классическое правило дифференцирования разности: производная разности равна разности производных.

LaTeX

$$$\\text{fderiv}_{\\mathbb{k}}(f - g) x \\equiv \\text{fderiv}_{\\mathbb{k}} f x - \\text{fderiv}_{\\mathbb{k}} g x$$$

Lean4

theorem fderiv_fun_sub (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (fun y => f y - g y) x = fderiv 𝕜 f x - fderiv 𝕜 g x :=
  (hf.hasFDerivAt.sub hg.hasFDerivAt).fderiv

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