moveRight_nim_heq — Mathlib

English

For every ordinal o, the right moves of nim o are in heterogeneous equivalence with nimbers nim((enumIsoToType o).symm i) via a right-move correspondence.

Русский

Для любого ординала o правые ходы nim o эквивалентны Nim-числам nim((enumIsoToType o).symm i) через отображение правого хода.

LaTeX

$$$ \forall o:\operatorname{Ordinal},\,\text{RightMoves}(nim\ o) \ \cong\ \{ nim\bigl((enumIsoToType\ o).symm\ i\bigr) \mid i\in o\} $$$

Lean4

theorem moveRight_nim_heq (o : Ordinal) : (nim o).moveRight ≍ fun i : o.toType => nim ((enumIsoToType o).symm i) := by
  rw [nim]; rfl

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