left_lt_right

Mathlib.SetTheory.Surreal.Basic

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

English

If x is numeric, then every left move x.moveLeft i is numeric.

Русский

Если x числовой, то каждый левый ход x.moveLeft i числовой.

LaTeX

$$$\text{Numeric}(x) \Rightarrow \forall i \in x.LeftMoves,\ \text{Numeric}(x.moveLeft i)$$$

Lean4

theorem left_lt_right {x : PGame} (o : Numeric x) (i : x.LeftMoves) (j : x.RightMoves) : x.moveLeft i < x.moveRight j :=
  by cases x; exact o.1 i j

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

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

Разделы

Аффилиация

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