derivWithin_comp_const_sub — Mathlib

English

Derivative within s of the function f(a − x) equals the negative derivative within −s of f at a − x.

Русский

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

LaTeX

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

Lean4

theorem derivWithin_comp_const_sub : derivWithin (f <| a - ·) s x = -derivWithin f (a +ᵥ -s) (a - x) :=
  by
  simp only [sub_eq_add_neg]
  rw [derivWithin_comp_neg (f <| a + ·), derivWithin_comp_const_add]

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