ofLists_moveLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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