derivWithin_comp_add_const — Mathlib

English

Derivative within s of the composition f(·+a) equals the derivative of f within the shifted set a+s at x+a.

Русский

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

LaTeX

$$$\\mathrm{derivWithin}(f(\\cdot + a), s, x) = \\mathrm{derivWithin}(f, a +\\!\\! s, x+a)$$$

Lean4

/-- Translation in the domain does not change the derivative. -/
theorem derivWithin_comp_add_const : derivWithin (f <| · + a) s x = derivWithin f (a +ᵥ s) (x + a) := by
  simp only [derivWithin, fderivWithin_comp_add_right]

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