add_moveLeft_inl — Mathlib

English

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

Русский

Если i — левый ход x, то соответствующий левый ход суммы x+y, происходящий от стороны x, равен x.moveLeft i плюс y; то есть (x+y).moveLeft (toLeftMovesAdd (Sum.inl i)) = x.moveLeft i + y.

LaTeX

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

Lean4

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

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