neg

Mathlib.Analysis.Calculus.Deriv.Add

URI: https://scilib.ai/kg/mathlib#derivWithin.neg

English

The sum of derivatives inside derivWithin equals the derivWithin of the sum.

Русский

Сумма частных производных внутри derivWithin равна производной суммы внутри derivWithin.

LaTeX

$$$\\text{derivWithin}(\\sum_{i\\in u} A_i, s, x) = \\sum_{i\\in u} \\text{derivWithin}(A_i, s, x).$$$

Lean4

theorem neg : derivWithin (-f) s x = -derivWithin f s x :=
  derivWithin.fun_neg

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru