hasFDerivWithinAt_comp_sub — Mathlib

English

The derivative within s of f(x − a) equals the derivative within −a + s at x − a.

Русский

Производная внутри s от f(x − a) равна производной внутри −a + s в точке x − a.

LaTeX

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

Lean4

theorem hasFDerivWithinAt_comp_sub (a : E) :
    HasFDerivWithinAt (fun x ↦ f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a) := by
  simpa [sub_eq_add_neg] using hasFDerivWithinAt_comp_add_right (-a)

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