neg_sub'

Mathlib.SetTheory.PGame.Algebra

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.neg_sub'

English

Negation distributes over subtraction: -(x - y) = -x - -y.

Русский

Отрицание распределяется над вычитанием: -(x - y) = -x - (-y).

LaTeX

$$$-(x - y) = -x - (-y)$$$

Lean4

/-- This lemma is named to match `neg_sub'`. -/
protected theorem neg_sub' (x y : PGame) : -(x - y) = -x - -y :=
  PGame.neg_add _ _

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

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

Разделы

Аффилиация

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