deriv_comp_add_const — Mathlib

English

The derivative of x ↦ f(x + a) at x equals the derivative of f at x + a.

Русский

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

LaTeX

$$$\\mathrm{deriv}(f(x+a))\\; x = \\mathrm{deriv}(f)(x+a)$$$

Lean4

/-- Translation in the domain does not change the derivative. -/
theorem deriv_comp_add_const : deriv (fun x ↦ f (x + a)) x = deriv f (x + a) := by
  simpa [add_comm] using deriv_comp_const_add f a x

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