hasFDerivWithinAt_comp_add_right — Mathlib

English

For every a ∈ E, HasFDerivWithinAt of the left-translation x ↦ f(x + a) with derivative f' inside s at x is equivalent to HasFDerivWithinAt of f with the same derivative inside the translated set a + s at x + a.

Русский

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

LaTeX

$$$\text{HasFDerivWithinAt}(f(x+a), f', s, x) \iff \text{HasFDerivWithinAt}(f, f', a+s, x+a)$$$

Lean4

theorem hasFDerivWithinAt_comp_add_right (a : E) :
    HasFDerivWithinAt (fun x ↦ f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a) := by
  simpa only [add_comm a] using hasFDerivWithinAt_comp_add_left a

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