English
There is a canonical bijection between the sum of right moves x.RightMoves ⊕ y.RightMoves and the right moves of the sum (x+y).RightMoves; i.e., x.RightMoves ⊕ y.RightMoves ≃ (x+y).RightMoves.
Русский
Существует каноническая биекция между суммой правых ходов x.RightMoves ⊕ y.RightMoves и правыми ходами суммы (x+y).RightMoves; то есть x.RightMoves ⊕ y.RightMoves ≃ (x+y).RightMoves.
LaTeX
$$$ x.RightMoves \oplus y.RightMoves \cong (x+y).RightMoves $$$
Lean4
/-- Converts a right move for `x` or `y` into a right move for `x + y` and vice versa.
Even though these types are the same (not definitionally so), this is the preferred way to convert
between them. -/
def toRightMovesAdd {x y : PGame} : x.RightMoves ⊕ y.RightMoves ≃ (x + y).RightMoves :=
Equiv.cast (rightMoves_add x y).symm
