derivWithin_comp_sub_const — Mathlib

English

Derivative within s of f(x − a) equals derivative within f at x − a with shifted set.

Русский

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

LaTeX

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

Lean4

theorem derivWithin_comp_sub_const : derivWithin (fun x ↦ f (x - a)) s x = derivWithin f (-a +ᵥ s) (x - a) := by
  simp_rw [sub_eq_add_neg, derivWithin_comp_add_const]

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