ofLists_moveRight' — Mathlib

English

Let L and R be finite lists of games. Then for every right move i of the composite game, the resulting position equals the i-th element of R.

Русский

Пусть L и R — конечные списки игр. Тогда для каждого правого хода i образованной игры результат равен i-му элементу R.

LaTeX

$$$\forall L,R:\n\mathrm{List}\,\mathrm{PGame},\ \forall i \in \mathrm{RightMoves}(\mathrm{ofLists}(L,R)),\ (\mathrm{ofLists}(L,R)).\mathrm{moveRight}(i) = R_i.$$$

Lean4

@[simp]
theorem ofLists_moveRight' {L R : List PGame} (i : (ofLists L R).RightMoves) :
    (ofLists L R).moveRight i = R[i.down.val] :=
  rfl

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