English
Let L and R be bijections between the left moves and the right moves of x and y, respectively. If each left move matches an equivalent left move under L and each right move matches an equivalent right move under R, then x is equivalent to y.
Русский
Пусть L и R — биекция между левых ходами x и y и между правых ходами x и y соответственно. Если каждый левый ход соответствует эквивалентному левому ходу через L, и каждый правый ход через R, то x эквивалентно y.
LaTeX
$$$L: x.LeftMoves \cong y.LeftMoves,\; R: x.RightMoves \cong y.RightMoves,\; (\forall i, x.moveLeft i \approx y.moveLeft (L i)) \\ (\forall j, x.moveRight j \approx y.moveRight (R j)) \Rightarrow x \approx y$$$
Lean4
theorem of_equiv {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves) (R : x.RightMoves ≃ y.RightMoves)
(hl : ∀ i, x.moveLeft i ≈ y.moveLeft (L i)) (hr : ∀ j, x.moveRight j ≈ y.moveRight (R j)) : x ≈ y :=
by
apply Equiv.of_exists <;> intro i
exacts [⟨_, hl i⟩, ⟨_, hr i⟩, ⟨_, by simpa using hl (L.symm i)⟩, ⟨_, by simpa using hr (R.symm i)⟩]
