differentiableAt_comp_add_left — Mathlib

English

If f is differentiable within s at x, then it is differentiable within a translated set at the translated point.

Русский

Если f дифференцируема внутри s в точке x, то она дифференцируема внутри сдвинутого множества в сдвинутой точке.

LaTeX

$$$\text{DifferentiableWithinAt}(f, s, x) \Rightarrow \text{DifferentiableWithinAt}(f, a+s, x+a)$$$

Lean4

theorem differentiableAt_comp_add_left (a : E) :
    DifferentiableAt 𝕜 (fun x ↦ f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x) := by
  simp [DifferentiableAt, hasFDerivAt_comp_add_left]

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