differentiableAt_iff_comp_const_add

English

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

Русский

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

LaTeX

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

Lean4

theorem differentiableAt_iff_comp_const_add {a b : 𝕜} :
    DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (b + x)) (-b + a) := by simp [differentiableAt_comp_add_left]

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