hasFDerivWithinAt_comp_add_left — Mathlib

English

For any a ∈ E, HasFDerivWithinAt (x ↦ f(a + x)) f' s x is equivalent to HasFDerivWithinAt f f' (a + s) (a + x).

Русский

Для любого a ∈ E верно: HasFDerivWithinAt (x ↦ f(a + x)) f' s x эквивалентно HasFDerivWithinAt f f' (a + s) (a + x).

LaTeX

$$$ HasFDerivWithinAt (\\lambda x, f(a + x)) f' s x \\iff HasFDerivWithinAt f f' (a +\\!\\! s) (a + x) $$$

Lean4

theorem hasFDerivWithinAt_comp_add_left (a : E) :
    HasFDerivWithinAt (fun x ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x) :=
  by
  have : map (a + ·) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x) :=
    by
    simp only [nhdsWithin, Filter.map_inf (add_right_injective a)]
    simp [← Set.image_vadd]
  simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, ← this, Function.comp_def]

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