toOfListsRightMoves — Mathlib

English

There is an equivalence between Fin R.length and the RightMoves of ofLists L R.

Русский

Существует эквивалентность между Fin R.length и RightMoves у ofLists L R.

LaTeX

$$$ \\mathrm{Fin}(R.length) \\simeq (\\mathrm{ofLists}(L,R)).RightMoves $$$

Lean4

/-- Converts a number into a right move for `ofLists`.

This is just an abbreviation for `Equiv.ulift.symm` -/
abbrev toOfListsRightMoves {L R : List PGame} : Fin R.length ≃ (ofLists L R).RightMoves :=
  Equiv.ulift.symm

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