toRightMovesNim — Mathlib

English

There is a natural equivalence between ordinals less than o and the right moves of nim o, given by toRightMovesNim.

Русский

Существует естественная эквивалентность между ординалами меньше o и правыми ходами nim o, задаваемая toRightMovesNim.

LaTeX

$$$ Set.Iio(o) \cong (nim\ o).RightMoves $$$

Lean4

/-- Turns an ordinal less than `o` into a right move for `nim o` and vice versa. -/
noncomputable def toRightMovesNim {o : Ordinal} : Set.Iio o ≃ (nim o).RightMoves :=
  (enumIsoToType o).toEquiv.trans (Equiv.cast (rightMoves_nim o).symm)

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