deriv_comp_neg — Mathlib

English

The derivative of x ↦ f(−x) at x is the negative of the derivative of f at −x.

Русский

Производная функции x ↦ f(−x) в точке x равна отрицательной производной функции f в точке −x.

LaTeX

$$$\\mathrm{deriv}(\\lambda x, f(-x))\\; x = -\\mathrm{deriv}(f)(-x)$$$

Lean4

/-- The derivative of `x ↦ f (-x)` at `a` is the negative of the derivative of `f` at `-a`. -/
theorem deriv_comp_neg : deriv (fun x ↦ f (-x)) x = -deriv f (-x) := by simpa using deriv_comp_mul_left (-1) f x

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