differentiableAt_comp_const_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem differentiableAt_comp_const_sub {a b : 𝕜} :
    DifferentiableAt 𝕜 (fun x ↦ f (b - x)) a ↔ DifferentiableAt 𝕜 f (b - a) :=
  by
  refine ⟨fun H ↦ ?_, fun H ↦ H.comp a (differentiable_id.const_sub _).differentiableAt⟩
  convert ((sub_sub_cancel _ a).symm ▸ H).comp (b - a) (differentiable_id.const_sub _).differentiableAt
  ext
  simp

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