deriv_comp_const_add — Mathlib

English

Shifting the input by a fixed a does not affect the derivative value, just the evaluation point.

Русский

Сдвиг входа на фиксированную величину 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_const_add : deriv (fun x ↦ f (a + x)) x = deriv f (a + x) := by
  simp only [deriv, fderiv_comp_add_left]

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