English
If the components rα and rβ are well-founded, then their product in GameAdd is well-founded.
Русский
Если rα и rβ гладко основаны, то их произведение в GameAdd хорошо основано.
LaTeX
$$$\\text{WellFounded } r_\\alpha \\land \\text{WellFounded } r_β \\Rightarrow \\text{WellFounded } (Prod.GameAdd r_α r_β)$$$
Lean4
/-- `Prod.GameAdd rα rβ x y` means that `x` can be reached from `y` by decreasing either entry with
respect to the relations `rα` and `rβ`.
It is so called, as it models game addition within combinatorial game theory. If `rα a₁ a₂` means
that `a₂ ⟶ a₁` is a valid move in game `α`, and `rβ b₁ b₂` means that `b₂ ⟶ b₁` is a valid move
in game `β`, then `GameAdd rα rβ` specifies the valid moves in the juxtaposition of `α` and `β`:
the player is free to choose one of the games and make a move in it, while leaving the other game
unchanged.
See `Sym2.GameAdd` for the unordered pair analog. -/
inductive GameAdd : α × β → α × β → Prop
| fst {a₁ a₂ b} : rα a₁ a₂ → GameAdd (a₁, b) (a₂, b)
| snd {a b₁ b₂} : rβ b₁ b₂ → GameAdd (a, b₁) (a, b₂)
