leftMoves_add — Mathlib

English

For any two games x and y, the left moves of the sum x+y correspond to the left moves of x and the left moves of y, i.e., there is a natural bijection between (x+y).LeftMoves and x.LeftMoves ⊕ y.LeftMoves.

Русский

Для любых игр x и y множество левых ходов суммы x+y эквивалентно объединению левых ходов x и левых ходов y; существует естественная биекция между (x+y).LeftMoves и x.LeftMoves ⊕ y.LeftMoves.

LaTeX

$$$ (x+y).LeftMoves \cong x.LeftMoves \oplus y.LeftMoves $$$

Lean4

/-- Use `toLeftMovesAdd` to cast between these two types. -/
theorem leftMoves_add : ∀ x y : PGame.{u}, (x + y).LeftMoves = (x.LeftMoves ⊕ y.LeftMoves)
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩ => rfl

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