ofLists_moveLeft' — Mathlib

English

Let L and R be finite lists of games, and form the game from L and R via the ofLists construction. Then for every left move i of this game, the resulting position equals the i-th element of L.

Русский

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

LaTeX

$$$\forall L,R:\n\mathrm{List}\,\mathrm{PGame},\ \forall i \in \mathrm{LeftMoves}(\mathrm{ofLists}(L,R)),\ (\mathrm{ofLists}(L,R)).\mathrm{moveLeft}(i) = L_i.$$$

Lean4

@[simp]
theorem ofLists_moveLeft' {L R : List PGame} (i : (ofLists L R).LeftMoves) : (ofLists L R).moveLeft i = L[i.down.val] :=
  rfl

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