add_comm_le

Mathlib.SetTheory.PGame.Algebra

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

English

For all x,y, x+y ≤ y+x.

Русский

Для любых x,y выполняется x+y ≤ y+x.

LaTeX

$$$x + y \le y + x$$$

Lean4

theorem add_comm_le {x y : PGame} : x + y ≤ y + x :=
  (x.add_comm y).le

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

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

Разделы

Аффилиация

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