hasFDerivAt_comp_add_right — Mathlib

English

For any a ∈ E, differentiability within s of the translated function x ↦ f(x + a) at x is equivalent to differentiability within translation of f at x + a with respect to a + s.

Русский

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

LaTeX

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

Lean4

theorem hasFDerivAt_comp_add_right (a : E) : HasFDerivAt (fun x ↦ f (x + a)) f' x ↔ HasFDerivAt f f' (x + a) := by
  simp [← hasFDerivWithinAt_univ, hasFDerivWithinAt_comp_add_right]

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