toPGame_moveLeft' — Mathlib

English

For any i, the left-move applied to o.toPGame equals the PGame corresponding to i under the left-move correspondence.

Русский

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

LaTeX

$$$o.toPGame.moveLeft\\, i = (toLeftMovesToPGame.symm\\, i).\\\\val.toPGame.$$$

Lean4

@[simp]
theorem toPGame_moveLeft' {o : Ordinal} (i) : o.toPGame.moveLeft i = (toLeftMovesToPGame.symm i).val.toPGame :=
  (congr_heq toPGame_moveLeft_hEq.symm (cast_heq _ i)).symm

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