add_moveRight_inl — Mathlib

English

If i is a left move of y, then the corresponding right move on the right side in the sum yields x.moveRight i plus y; i.e., (x+y).moveRight (toRightMovesAdd (Sum.inl i)) = x.moveRight i + y.

Русский

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

LaTeX

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

Lean4

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

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