ofLists_moveRight — Mathlib

English

Let L and R be finite lists of games. If i is a finite index into R, then the right move corresponding to i yields the i-th element of R in the composite game built from L and R.

Русский

Пусть L и R — конечные списки игр. Если i — конечный индекс в R, то правый ход, соответствующий i, даёт i-й элемент R в игре, построенной из L и R.

LaTeX

$$$\forall L,R:\n\mathrm{List}\,\mathrm{PGame},\ \forall i:\n\mathrm{Fin}(R.\mathrm{length}),\ (\mathrm{ofLists}(L,R)).\mathrm{moveRight}(\mathrm{ULift}.up\ i) = R_i.$$$

Lean4

theorem ofLists_moveRight {L R : List PGame} (i : Fin R.length) : (ofLists L R).moveRight (ULift.up i) = R[i] :=
  rfl

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