toLeftMovesNim — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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