differentiableAt_comp_sub_const — Mathlib

English

For any a, b, differentiability of f at a is equivalent to differentiability of the shifted function at a − b.

Русский

Для любых a, b дифференцируемость f в a эквивалентна дифференцируемости после сдвига f в a − b.

LaTeX

$$$$ \text{DifferentiableAt } 𝕜 f a \iff \text{DifferentiableAt } 𝕜 (\lambda x, f x) (a - b). $$$$

Lean4

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

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