differentiableAt_comp_add_right — Mathlib

English

For any a ∈ E, differentiability at x of the translated function x ↦ f(x + a) is equivalent to differentiability at x + a of f.

Русский

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

LaTeX

$$$\text{DifferentiableAt}(\lambda x. f(x+a), x) \iff \text{DifferentiableAt}(f, x+a)$$$

Lean4

theorem differentiableAt_comp_add_right (a : E) :
    DifferentiableAt 𝕜 (fun x ↦ f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a) := by
  simp [DifferentiableAt, hasFDerivAt_comp_add_right]

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