fderiv_fun_neg — Mathlib

English

Let f: E → F be a differentiable function. Then the derivative of −f at x equals the negation of the derivative of f at x: f′(x) for −f equals −f′(x).

Русский

Пусть f: E → F дифференцируема. Тогда производная функции −f в точке x равна минусу производной f в точке x: (−f)′(x) = −f′(x).

LaTeX

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

Lean4

@[simp]
theorem fderiv_fun_neg : fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x := by
  simp only [← fderivWithin_univ, fderivWithin_fun_neg uniqueDiffWithinAt_univ]

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