fderiv_comp_add_right — Mathlib

English

The derivative of the translated function x ↦ f(x + a) at x coincides with the derivative of f at x + a.

Русский

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

LaTeX

$$$fderiv\ 𝕜$\lambda x. f(x+a)$\ x = fderiv\ 𝕜\ f\ (x+a)$$$

Lean4

theorem fderiv_comp_add_right (a : E) : fderiv 𝕜 (fun x ↦ f (x + a)) x = fderiv 𝕜 f (x + a) := by
  simp [← fderivWithin_univ, fderivWithin_comp_add_right]

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