mathlib documentation

set_theory.game

Combinatorial games.

In this file we define the quotient of pre-games by the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤ p, and construct an instance add_comm_group game, as well as an instance partial_order game (although note carefully the warning that the < field in this instance is not the usual relation on combinatorial games).

@[instance]

Equations
def game  :
Type (u_1+1)

The type of combinatorial games. In ZFC, a combinatorial game is constructed from two sets of combinatorial games that have been constructed at an earlier stage. To do this in type theory, we say that a combinatorial pre-game is built inductively from two families of combinatorial games indexed over any type in Type u. The resulting type pgame.{u} lives in Type (u+1), reflecting that it is a proper class in ZFC. A combinatorial game is then constructed by quotienting by the equivalence x ≈ y ↔ x ≤ y ∧ y ≤ x.

Equations
def game.le  :
gamegame → Prop

The relation x ≤ y on games.

Equations
@[instance]

Equations
theorem game.le_refl (x : game) :
x x

theorem game.le_trans (x y z : game) :
x yy zx z

theorem game.le_antisymm (x y : game) :
x yy xx = y

def game.lt  :
gamegame → Prop

The relation x < y on games.

Equations
theorem game.not_le {x y : game} :
¬x y y.lt x

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
def game.neg  :

The negation of {L | R} is {-R | -L}.

Equations
@[instance]

Equations
def game.add  :
gamegamegame

The sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.

Equations
@[instance]

Equations
theorem game.add_assoc (x y z : game) :
x + y + z = x + (y + z)

theorem game.add_zero (x : game) :
x + 0 = x

theorem game.zero_add (x : game) :
0 + x = x

theorem game.add_left_neg (x : game) :
-x + x = 0

theorem game.add_comm (x y : game) :
x + y = y + x

theorem game.add_le_add_left (a b : game) (a_1 : a b) (c : game) :
c + a c + b

The < operation provided by this partial order is not the usual < on games!

Equations