differentiableAt_iff_comp_add_const

English

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

Русский

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

LaTeX

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

Lean4

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

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