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).

source
@[protected, instance]
def pgame.setoid  :
setoid pgame
Equations
source
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
source
def game.le  :
game → game → Prop

The relation x ≤ y on games.

Equations
source
@[protected, instance]
def game.has_le  :
has_le game
Equations
source
theorem game.le_refl (x : game) :
x ≤ x
source
theorem game.le_trans (x y z : game) :
x ≤ y → y ≤ z → x ≤ z
source
theorem game.le_antisymm (x y : game) :
x ≤ y → y ≤ x → x = y
source
def game.lt  :
game → game → Prop

The relation x < y on games.

Equations
source
theorem game.not_le {x y : game} :
¬x ≤ y ↔ y.lt x
source
@[protected, instance]
def game.has_zero  :
has_zero game
Equations
source
@[protected, instance]
def game.inhabited  :
inhabited game
Equations
source
@[protected, instance]
def game.has_one  :
has_one game
Equations
source
def game.neg  :
game → game

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

Equations
source
@[protected, instance]
def game.has_neg  :
has_neg game
Equations
source
def game.add  :
game → game → game

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

Equations
source
@[protected, instance]
def game.has_add  :
has_add game
Equations
source
theorem game.add_assoc (x y z : game) :
x + y + z = x + (y + z)
source
@[protected, instance]
def game.add_semigroup  :
add_semigroup game
Equations
source
theorem game.add_zero (x : game) :
x + 0 = x
source
theorem game.zero_add (x : game) :
0 + x = x
source
@[protected, instance]
def game.add_monoid  :
add_monoid game
Equations
source
theorem game.add_left_neg (x : game) :
-x + x = 0
source
@[protected, instance]
def game.add_group  :
add_group game
Equations
source
theorem game.add_comm (x y : game) :
x + y = y + x
source
@[protected, instance]
def game.add_comm_semigroup  :
add_comm_semigroup game
Equations
source
@[protected, instance]
def game.add_comm_group  :
add_comm_group game
Equations
source
theorem game.add_le_add_left (a b : game) :
a ≤ b → ∀ (c : game), c + a ≤ c + b
source
def game.game_partial_order  :
partial_order game

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

Equations
source
def game.ordered_add_comm_group_game  :
ordered_add_comm_group game

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

Equations