toPGame_moveLeft — Mathlib

English

For any i in the left-moves of o.toPGame, applying moveLeft at the corresponding index yields the PGame associated with that ordinal.

Русский

Для любого i из левых ходов o.toPGame применение moveLeft по соответствующему индексу дает PGame, соответствующий данному ординалу.

LaTeX

$$$\\\\forall i : (o.toPGame. LeftMoves), \\\\text{moveLeft} \\\\text{(toLeftMovesToPGame} \\\\text{i)} = i.val.toPGame.$$$

Lean4

theorem toPGame_moveLeft {o : Ordinal} (i) : o.toPGame.moveLeft (toLeftMovesToPGame i) = i.val.toPGame := by simp

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