deriv_comp_const_sub — 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

theorem deriv_comp_const_sub : deriv (fun x ↦ f (a - x)) x = -deriv f (a - x) := by
  simp_rw [sub_eq_add_neg, deriv_comp_neg (f <| a + ·), deriv_comp_const_add]

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