English
There is a natural equivalence between the disjoint union of pairs consisting of a left move of x with a right move of y, and a left move of x paired with a right move of y, and the set of right moves of the product x*y. Concretely, (LeftMoves(x) × RightMoves(y)) ⊕ (RightMoves(x) × LeftMoves(y)) is naturally in bijection with the RightMoves of the product x*y.
Русский
Существует естественный эквивелент между объединением пар, состоящих из левого хода x и правого хода y, и левого хода x, сопряженного с правым ходом y, и множеством правых ходов произведения x*y: (LeftMoves(x) × RightMoves(y)) ⊕ (RightMoves(x) × LeftMoves(y)) эквивалентно RightMoves(x*y).
LaTeX
$$$$(\\mathrm{LeftMoves}(x) \\times \\mathrm{RightMoves}(y)) \\oplus (\\mathrm{RightMoves}(x) \\times \\mathrm{LeftMoves}(y)) \\cong \\mathrm{RightMoves}(x \\cdot y).$$$$
Lean4
/-- Turns a left and a right move for `x` and `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 toRightMovesMul {x y : PGame} : (x.LeftMoves × y.RightMoves) ⊕ (x.RightMoves × y.LeftMoves) ≃ (x * y).RightMoves :=
Equiv.cast (rightMoves_mul x y).symm
