add_moveRight_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem add_moveRight_inr (x : PGame) {y : PGame} (i) :
    (x + y).moveRight (toRightMovesAdd (Sum.inr i)) = x + y.moveRight i :=
  by
  cases x
  cases y
  rfl

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