moveRight_toRightMovesNim — Mathlib

English

The right move in nim o corresponding to toRightMovesNim i yields nim i, i.e., (nim o).moveRight (toRightMovesNim i) = nim i.

Русский

Правый ход в nim o, соответствующий toRightMovesNim i, даёт nim i; то есть (nim o).moveRight (toRightMovesNim i) = nim i.

LaTeX

$$$ \forall i:\operatorname{Iio}(o),\; (nim\ o).moveRight\,(toRightMovesNim\ i) = nim\ i. $$$

Lean4

theorem moveRight_toRightMovesNim {o : Ordinal} (i) : (nim o).moveRight (toRightMovesNim i) = nim i := by simp

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