English
If there is an equivalence between the left/right move structures of x and y, then x ≡ y.
Русский
Если между структурами левых и правых ходов x и y существует эквивалентность, то x ≡ y.
LaTeX
$$$ \forall {x y : PGame} (l : x.LeftMoves \simeq y.LeftMoves) (r : x.RightMoves \simeq y.RightMoves), \forall hl hr, x \equiv y$$$
Lean4
/-- `Relabelling x y` says that `x` and `y` are really the same game, just dressed up differently.
Specifically, there is a bijection between the moves for Left in `x` and in `y`, and similarly
for Right, and under these bijections we inductively have `Relabelling`s for the consequent games.
-/
inductive Relabelling : PGame.{u} → PGame.{u} → Type (u + 1)
|
mk :
∀ {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves) (R : x.RightMoves ≃ y.RightMoves),
(∀ i, Relabelling (x.moveLeft i) (y.moveLeft (L i))) →
(∀ j, Relabelling (x.moveRight j) (y.moveRight (R j))) → Relabelling x y
