Theorems · Inductive type · order theory

Prod.GameAdd

{α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop

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.

Defined in

Mathlib.Order.GameAdd

Cited by

18 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms