moveLeft_nim — Mathlib

English

For any i in (nim o).LeftMoves, (nim o).moveLeft i equals nim of the corresponding left option, i.e., nim((toLeftMovesNim.symm i).val).

Русский

Для любого i из (nim o).LeftMoves, (nim o).moveLeft i равняется nimbers nim соответствующего левого хода, то есть nim((toLeftMovesNim.symm i).val).

LaTeX

$$$ \forall i\in (nim\ o).LeftMoves,\; (nim\ o).moveLeft\,i = nim\bigl((toLeftMovesNim.symm\ i).val\bigr) $$$

Lean4

@[simp]
theorem moveLeft_nim {o : Ordinal} (i) : (nim o).moveLeft i = nim (toLeftMovesNim.symm i).val :=
  (congr_heq (moveLeft_nim_heq o).symm (cast_heq _ i)).symm

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