neg_add_le

Mathlib.SetTheory.PGame.Algebra

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

English

For all x,y, -(x+y) ≤ -x + -y.

Русский

Для всех x,y выполняется -(x+y) ≤ -x + -y.

LaTeX

$$$-(x + y) \le -x + -y$$$

Lean4

theorem neg_add_le {x y : PGame} : -(x + y) ≤ -x + -y :=
  (x.neg_add y).le

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

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

Разделы

Аффилиация

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