toLeftMovesToPGame — Mathlib

English

There is a natural equivalence between Set.Iio(o) and o.toPGame.LeftMoves.

Русский

Существует естественная биекция между Set.Iio(o) и o.toPGame.LeftMoves.

LaTeX

$$$Set.Iio(o) \\simeq o.toPGame.LeftMoves.$$$

Lean4

/-- Converts an ordinal less than `o` into a move for the `PGame` corresponding to `o`, and vice
versa. -/
noncomputable def toLeftMovesToPGame {o : Ordinal} : Set.Iio o ≃ o.toPGame.LeftMoves :=
  (enumIsoToType o).toEquiv.trans (Equiv.cast (toPGame_leftMoves o).symm)

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