rightMoves_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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