Documentation

CombinatorialGames.GameForm.OrdinalSum

Ordinal sums #

$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$ The ordinal sum G : H of two game forms is played on G (the base) and H (the branch) at once, but a move in the base destroys the branch: $$ G : H = \form<G^\mathcal{L}, G : H^\mathcal{L}>[G^\mathcal{R}, G : H^\mathcal{R}]. $$ Blue-Red Hackenbush stalks and forests are built from ordinal sums.

@[irreducible]

def GameForm.ordinalSum (x y : GameForm) :

The ordinal sum ordinalSum x y = x : y, see the module docstring.

Equations

x.ordinalSum y = !{fun (p : Player) => Moves.moves p x ∪ Set.range fun (z : ↑(Moves.moves p y)) => x.ordinalSum ↑z}

Instances For

theorem GameForm.moves_ordinalSum (p : Player) (x y : GameForm) :

Moves.moves p (x.ordinalSum y) = Moves.moves p x ∪ x.ordinalSum '' Moves.moves p y

theorem GameForm.mem_moves_ordinalSum_iff {p : Player} {x y z : GameForm} :

z ∈ Moves.moves p (x.ordinalSum y) ↔ z ∈ Moves.moves p x ∨ ∃ y' ∈ Moves.moves p y, z = x.ordinalSum y'

theorem GameForm.mem_moves_ordinalSum_base {p : Player} {x x' : GameForm} (y : GameForm) (h : x' ∈ Moves.moves p x) :

x' ∈ Moves.moves p (x.ordinalSum y)

theorem GameForm.mem_moves_ordinalSum_branch {p : Player} {y y' : GameForm} (x : GameForm) (h : y' ∈ Moves.moves p y) :

x.ordinalSum y' ∈ Moves.moves p (x.ordinalSum y)

theorem GameForm.isOption_ordinalSum_iff {x y z : GameForm} :

Moves.IsOption z (x.ordinalSum y) ↔ Moves.IsOption z x ∨ ∃ (y' : GameForm), Moves.IsOption y' y ∧ z = x.ordinalSum y'

theorem GameForm.IsOption.ordinalSum_base {x x' : GameForm} (y : GameForm) (h : Moves.IsOption x' x) :

Moves.IsOption x' (x.ordinalSum y)

theorem GameForm.IsOption.ordinalSum_branch {y y' : GameForm} (x : GameForm) (h : Moves.IsOption y' y) :

Moves.IsOption (x.ordinalSum y') (x.ordinalSum y)

@[simp]

theorem GameForm.isEnd_ordinalSum_iff {p : Player} {x y : GameForm} :

Form.IsEnd p (x.ordinalSum y) ↔ Form.IsEnd p x ∧ Form.IsEnd p y

@[simp]

theorem GameForm.ordinalSum_zero (x : GameForm) :

x.ordinalSum 0 = x

@[simp, irreducible]

theorem GameForm.zero_ordinalSum (y : GameForm) :

ordinalSum 0 y = y

@[simp]

theorem GameForm.ordinalSum_eq_zero_iff {x y : GameForm} :

x.ordinalSum y = 0 ↔ x = 0 ∧ y = 0

theorem GameForm.ordinalSum_ne_zero {x : GameForm} (y : GameForm) (h : x ≠ 0) :

x.ordinalSum y ≠ 0

@[irreducible]

theorem GameForm.neg_ordinalSum (x y : GameForm) :

-x.ordinalSum y = (-x).ordinalSum (-y)

@[irreducible]

theorem GameForm.ordinalSum_assoc (x y z : GameForm) :

(x.ordinalSum y).ordinalSum z = x.ordinalSum (y.ordinalSum z)