le_moveRight

Mathlib.SetTheory.Surreal.Basic

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

English

For any x numeric, x ≤ x.moveRight j for all j.

Русский

Для любого числового x и любого правого хода j выполняется x ≤ x.moveRight j.

LaTeX

$$$(Numeric(x)) \Rightarrow \forall j : x.RightMoves, x \le x.moveRight(j)$$$

Lean4

theorem le_moveRight {x : PGame} (o : Numeric x) (j) : x ≤ x.moveRight j :=
  (o.lt_moveRight j).le

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

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

Разделы

Аффилиация

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