listShortGet — Mathlib

English

Same as above: left-move case analysis for the product of games.

Русский

То же самое: разбор случаев левых ходов для произведения игр.

LaTeX

$$$\forall x,y : PGame, (k) : (x * y).LeftMoves, (hl) : \forall ix,iy, P( toLeftMovesMul(\text{Sum.inl} ⟨ix,iy⟩ )), (hr) : \forall jx, jy, P( toLeftMovesMul(\text{Sum.inr} ⟨jx, jy⟩ )) \Rightarrow P(k)$$$

Lean4

instance listShortGet : ∀ (L : List PGame.{u}) [ListShort L] (i : Nat) (h : i < List.length L), Short L[i]
  | _ :: _, ListShort.cons' S _, 0, _ => S
  | _ :: tl, ListShort.cons' _ S, n + 1, h => @listShortGet tl S n ((add_lt_add_iff_right 1).mp h)

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