derivWithin_comp_neg — Mathlib

English

For any f: 𝕜 → F and any set s, the derivative within s of the function x ↦ f(−x) at x equals minus the derivative within −s at −x.

Русский

Для любой функции f: 𝕜 → F и любого множества s производная внутри s от функции x ↦ f(−x) в точке x равна минус производной внутри −s в точке −x.

LaTeX

$$$\\mathrm{derivWithin}(f\\circ(\\,-\\cdot))\\; s\\; x = -\\mathrm{derivWithin}(f, -s, -x)$$$

Lean4

theorem derivWithin_comp_neg : derivWithin (f <| -·) s x = -derivWithin f (-s) (-x) := by
  simpa using derivWithin_comp_mul_left (-1) f s x

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