differentiableWithinAt_comp_add_right

English

For every a ∈ E, differentiability within s of the function x ↦ f(x + a) at x is equivalent to differentiability within the translated set a + s at x + a.

Русский

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

LaTeX

$$$\text{DifferentiableWithinAt}(\lambda x. f(x+a), s, x) \iff \text{DifferentiableWithinAt}(f, a+s, x+a)$$$

Lean4

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

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