moveLeft_lt

Mathlib.SetTheory.Surreal.Basic

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

English

For any x numeric, every left move x.moveLeft i is strictly less than x.

Русский

Для любого числового x каждый левый ход x.moveLeft i строго меньше x.

LaTeX

$$$\forall x \,(Numeric\,x) \Rightarrow \forall i : x.LeftMoves, x.moveLeft(i) < x$$$

Lean4

theorem moveLeft_lt {x : PGame} (o : Numeric x) (i) : x.moveLeft i < x :=
  (moveLeft_lf i).lt (o.moveLeft i) o

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

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

Разделы

Аффилиация

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