differentiableWithinAt_comp_add_left

English

Let a ∈ E. The differentiability within at x of the map x ↦ f(a + x) is equivalent to the differentiability within at a + s of f at a + x.

Русский

Пусть a ∈ E. Дифференцируемость внутри x отображения x ↦ f(a + x) равносильна дифференцируемости внутри a + s функции f в точке a + x.

LaTeX

$$$ DifferentiableWithinAt 𝕜 (\\lambda x, f(a + x)) s x \\iff DifferentiableWithinAt 𝕜 f (a + s) (a + x) $$$

Lean4

theorem differentiableWithinAt_comp_add_left (a : E) :
    DifferentiableWithinAt 𝕜 (fun x ↦ f (a + x)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (a + x) := by
  simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_add_left]

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