differentiableAt_comp_add_const — Mathlib

English

Let f be a function between 𝕜 and F. For any a, b ∈ 𝕜, the function x ↦ f(x + b) is differentiable at a if and only if f is differentiable at a + b.

Русский

Пусть f: 𝕜 → F; для любых a, b ∈ 𝕜 выполняется: дифференцируемость x ↦ f(x + b) в точке a эквивалентна дифференцируемости f в точке a + b.

LaTeX

$$$ \\operatorname{DifferentiableAt}_{\\mathbb{k}} \\big( x \\mapsto f(x+b) \\big)\\,(a) \\; \\Longleftrightarrow \\; \\operatorname{DifferentiableAt}_{\\mathbb{k}} f(a+b). $$$

Lean4

theorem differentiableAt_comp_add_const {a b : 𝕜} :
    DifferentiableAt 𝕜 (fun x ↦ f (x + b)) a ↔ DifferentiableAt 𝕜 f (a + b) := by
  grind [add_comm, differentiableAt_comp_add_left]

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