differentiableAt_iff_comp_sub_const

English

For any a, b, differentiability of f at a is equivalent to differentiability of the shifted function x ↦ f(x − b) at a + b.

Русский

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

LaTeX

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

Lean4

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

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