fderiv_neg — Mathlib

English

The same relation holds for any differentiable f: f′(x) = derivative of f at x implies (−f)′(x) = −f′(x).

Русский

То же соотношение справедливо для любой дифференцируемой функции f: (−f)′(x) = −f′(x).

LaTeX

$$$fderiv_{\mathbb{K}}(-f)\, x = -\, fderiv_{\mathbb{K}} f\, x$$$

Lean4

/-- Version of `fderiv_neg` where the function is written `-f` instead of `fun y ↦ - f y`. -/
theorem fderiv_neg : fderiv 𝕜 (-f) x = -fderiv 𝕜 f x :=
  fderiv_fun_neg

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