add_moveLeft_inr — Mathlib

English

If i is a right move of y, then the corresponding left move of the sum coming from the y-side is x plus the move in y; i.e., (x+y).moveLeft (toLeftMovesAdd (Sum.inr i)) = x + y.moveLeft i.

Русский

Если i — правый ход y, то соответствующий левый ход суммы происходит на стороне y и равен x + y.moveLeft i.

LaTeX

$$$ (x+y).moveLeft\big(\mathrm{toLeftMovesAdd}(\mathrm{Sum.inr} i)\big) = x + y.moveLeft i $$$

Lean4

@[simp]
theorem add_moveLeft_inr (x : PGame) {y : PGame} (i) :
    (x + y).moveLeft (toLeftMovesAdd (Sum.inr i)) = x + y.moveLeft i :=
  by
  cases x
  cases y
  rfl

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