moveLeft_nim_heq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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