toOfListsLeftMoves — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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

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