fderiv_comp_add_left — Mathlib

English

For any a ∈ E and x ∈ E, the derivative of the left-translated function at x equals the derivative of f at x + a.

Русский

Для любого a ∈ E и x ∈ E производная левой транспозиции функции x ↦ f(a + x) в точке x равна производной f в точке x + a.

LaTeX

$$$\text{fderiv}\ 𝕜\left(\lambda x. f(a+x)\right)(x) = \text{fderiv}\ 𝕜\ f(a+x)$$$

Lean4

theorem fderiv_comp_add_left (a : E) : fderiv 𝕜 (fun x ↦ f (a + x)) x = fderiv 𝕜 f (a + x) := by
  simpa [add_comm a] using fderiv_comp_add_right a

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