# Combinatorial (pre-)games. #

The basic theory of combinatorial games, following Conway's book On Numbers and Games. We construct "pregames", define an ordering and arithmetic operations on them, then show that the operations descend to "games", defined via the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤ p.

The surreal numbers will be built as a quotient of a subtype of pregames.

A pregame (SetTheory.PGame below) is axiomatised via an inductive type, whose sole constructor takes two types (thought of as indexing the possible moves for the players Left and Right), and a pair of functions out of these types to SetTheory.PGame (thought of as describing the resulting game after making a move).

Combinatorial games themselves, as a quotient of pregames, are constructed in Game.lean.

## Conway induction #

By construction, the induction principle for pregames is exactly "Conway induction". That is, to prove some predicate SetTheory.PGame → Prop holds for all pregames, it suffices to prove that for every pregame g, if the predicate holds for every game resulting from making a move, then it also holds for g.

While it is often convenient to work "by induction" on pregames, in some situations this becomes awkward, so we also define accessor functions SetTheory.PGame.LeftMoves, SetTheory.PGame.RightMoves, SetTheory.PGame.moveLeft and SetTheory.PGame.moveRight. There is a relation PGame.Subsequent p q, saying that p can be reached by playing some non-empty sequence of moves starting from q, an instance WellFounded Subsequent, and a local tactic pgame_wf_tac which is helpful for discharging proof obligations in inductive proofs relying on this relation.

## Order properties #

Pregames have both a ≤ and a < relation, satisfying the usual properties of a Preorder. The relation 0 < x means that x can always be won by Left, while 0 ≤ x means that x can be won by Left as the second player.

It turns out to be quite convenient to define various relations on top of these. We define the "less or fuzzy" relation x ⧏ y as ¬ y ≤ x, the equivalence relation x ≈ y as x ≤ y ∧ y ≤ x, and the fuzzy relation x ‖ y as x ⧏ y ∧ y ⧏ x. If 0 ⧏ x, then x can be won by Left as the first player. If x ≈ 0, then x can be won by the second player. If x ‖ 0, then x can be won by the first player.

Statements like zero_le_lf, zero_lf_le, etc. unfold these definitions. The theorems le_def and lf_def give a recursive characterisation of each relation in terms of themselves two moves later. The theorems zero_le, zero_lf, etc. also take into account that 0 has no moves.

Later, games will be defined as the quotient by the ≈ relation; that is to say, the Antisymmetrization of SetTheory.PGame.

## Algebraic structures #

We next turn to defining the operations necessary to make games into a commutative additive group. Addition is defined for $x = \{xL | xR\}$ and $y = \{yL | yR\}$ by $x + y = \{xL + y, x + yL | xR + y, x + yR\}$. Negation is defined by $\{xL | xR\} = \{-xR | -xL\}$.

The order structures interact in the expected way with addition, so we have

theorem le_iff_sub_nonneg {x y : PGame} : x ≤ y ↔ 0 ≤ y - x := sorry
theorem lt_iff_sub_pos {x y : PGame} : x < y ↔ 0 < y - x := sorry


We show that these operations respect the equivalence relation, and hence descend to games. At the level of games, these operations satisfy all the laws of a commutative group. To prove the necessary equivalence relations at the level of pregames, we introduce the notion of a Relabelling of a game, and show, for example, that there is a relabelling between x + (y + z) and (x + y) + z.

## Future work #

• The theory of dominated and reversible positions, and unique normal form for short games.
• Analysis of basic domineering positions.
• Hex.
• Temperature.
• The development of surreal numbers, based on this development of combinatorial games, is still quite incomplete.

## References #

The material here is all drawn from

• [Conway, On numbers and games][conway2001]

An interested reader may like to formalise some of the material from

• [Andreas Blass, A game semantics for linear logic][MR1167694]
• [André Joyal, Remarques sur la théorie des jeux à deux personnes][joyal1997]

### Pre-game moves #

inductive SetTheory.PGame :
Type (u + 1)

The type of pre-games, before we have quotiented by equivalence (PGame.Setoid). 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 pre-game is built inductively from two families of pre-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.

• mk: (α β : Type u) → ()
Instances For

The indexing type for allowable moves by Left.

Equations
Instances For

The indexing type for allowable moves by Right.

Equations
Instances For

The new game after Left makes an allowed move.

Equations
Instances For

The new game after Right makes an allowed move.

Equations
Instances For
@[simp]
theorem SetTheory.PGame.leftMoves_mk {xl : Type u_1} {xr : Type u_1} {xL : } {xR : } :
(SetTheory.PGame.mk xl xr xL xR).LeftMoves = xl
@[simp]
theorem SetTheory.PGame.moveLeft_mk {xl : Type u_1} {xr : Type u_1} {xL : } {xR : } :
(SetTheory.PGame.mk xl xr xL xR).moveLeft = xL
@[simp]
theorem SetTheory.PGame.rightMoves_mk {xl : Type u_1} {xr : Type u_1} {xL : } {xR : } :
(SetTheory.PGame.mk xl xr xL xR).RightMoves = xr
@[simp]
theorem SetTheory.PGame.moveRight_mk {xl : Type u_1} {xr : Type u_1} {xL : } {xR : } :
(SetTheory.PGame.mk xl xr xL xR).moveRight = xR

Construct a pre-game from list of pre-games describing the available moves for Left and Right.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SetTheory.PGame.leftMoves_ofLists (L : ) (R : ) :
().LeftMoves = ULift.{u_1, 0} (Fin L.length)
theorem SetTheory.PGame.rightMoves_ofLists (L : ) (R : ) :
().RightMoves = ULift.{u_1, 0} (Fin R.length)
def SetTheory.PGame.toOfListsLeftMoves {L : } {R : } :
Fin L.length ().LeftMoves

Converts a number into a left move for ofLists.

Equations
• SetTheory.PGame.toOfListsLeftMoves = (().trans Equiv.ulift).symm
Instances For
def SetTheory.PGame.toOfListsRightMoves {L : } {R : } :
Fin R.length ().RightMoves

Converts a number into a right move for ofLists.

Equations
• SetTheory.PGame.toOfListsRightMoves = (().trans Equiv.ulift).symm
Instances For
theorem SetTheory.PGame.ofLists_moveLeft {L : } {R : } (i : Fin L.length) :
().moveLeft (SetTheory.PGame.toOfListsLeftMoves i) = L.get i
@[simp]
theorem SetTheory.PGame.ofLists_moveLeft' {L : } {R : } (i : ().LeftMoves) :
().moveLeft i = L.get (SetTheory.PGame.toOfListsLeftMoves.symm i)
theorem SetTheory.PGame.ofLists_moveRight {L : } {R : } (i : Fin R.length) :
().moveRight (SetTheory.PGame.toOfListsRightMoves i) = R.get i
@[simp]
theorem SetTheory.PGame.ofLists_moveRight' {L : } {R : } (i : ().RightMoves) :
().moveRight i = R.get (SetTheory.PGame.toOfListsRightMoves.symm i)
def SetTheory.PGame.moveRecOn {C : } (x : SetTheory.PGame) (IH : (y : SetTheory.PGame) → ((i : y.LeftMoves) → C (y.moveLeft i))((j : y.RightMoves) → C (y.moveRight j))C y) :
C x

A variant of PGame.recOn expressed in terms of PGame.moveLeft and PGame.moveRight.

Both this and PGame.recOn describe Conway induction on games.

Equations
Instances For
theorem SetTheory.PGame.isOption_iff :
∀ (a a_1 : SetTheory.PGame), a.IsOption a_1 (∃ (i : a_1.LeftMoves), a = a_1.moveLeft i) ∃ (i : a_1.RightMoves), a = a_1.moveRight i

IsOption x y means that x is either a left or right option for y.

• moveLeft: ∀ {x : SetTheory.PGame} (i : x.LeftMoves), (x.moveLeft i).IsOption x
• moveRight: ∀ {x : SetTheory.PGame} (i : x.RightMoves), (x.moveRight i).IsOption x
Instances For
theorem SetTheory.PGame.IsOption.mk_left {xl : Type u} {xr : Type u} (xL : ) (xR : ) (i : xl) :
(xL i).IsOption (SetTheory.PGame.mk xl xr xL xR)
theorem SetTheory.PGame.IsOption.mk_right {xl : Type u} {xr : Type u} (xL : ) (xR : ) (i : xr) :
(xR i).IsOption (SetTheory.PGame.mk xl xr xL xR)

Subsequent x y says that x can be obtained by playing some nonempty sequence of moves from y. It is the transitive closure of IsOption.

Equations
Instances For
theorem SetTheory.PGame.Subsequent.trans {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} :
x.Subsequent yy.Subsequent zx.Subsequent z
@[simp]
theorem SetTheory.PGame.Subsequent.moveLeft {x : SetTheory.PGame} (i : x.LeftMoves) :
(x.moveLeft i).Subsequent x
@[simp]
theorem SetTheory.PGame.Subsequent.moveRight {x : SetTheory.PGame} (j : x.RightMoves) :
(x.moveRight j).Subsequent x
@[simp]
theorem SetTheory.PGame.Subsequent.mk_left {xl : Type u_1} {xr : Type u_1} (xL : ) (xR : ) (i : xl) :
(xL i).Subsequent (SetTheory.PGame.mk xl xr xL xR)
@[simp]
theorem SetTheory.PGame.Subsequent.mk_right {xl : Type u_1} {xr : Type u_1} (xL : ) (xR : ) (j : xr) :
(xR j).Subsequent (SetTheory.PGame.mk xl xr xL xR)

Discharges proof obligations of the form ⊢ Subsequent .. arising in termination proofs of definitions using well-founded recursion on PGame.

Equations
Instances For
@[simp]
theorem SetTheory.PGame.Subsequent.mk_right' {xl : Type u_1} {xr : Type u_1} (xL : ) (xR : ) (j : (SetTheory.PGame.mk xl xr xL xR).RightMoves) :
(xR j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
@[simp]
theorem SetTheory.PGame.Subsequent.moveRight_mk_left {xl : Type u_1} {i : xl} {xr : Type u_1} {xR : } (xL : ) (j : (xL i).RightMoves) :
((xL i).moveRight j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
@[simp]
theorem SetTheory.PGame.Subsequent.moveRight_mk_right {xr : Type u_1} {i : xr} {xl : Type u_1} {xL : } (xR : ) (j : (xR i).RightMoves) :
((xR i).moveRight j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
@[simp]
theorem SetTheory.PGame.Subsequent.moveLeft_mk_left {xl : Type u_1} {i : xl} {xr : Type u_1} {xR : } (xL : ) (j : (xL i).LeftMoves) :
((xL i).moveLeft j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
@[simp]
theorem SetTheory.PGame.Subsequent.moveLeft_mk_right {xr : Type u_1} {i : xr} {xl : Type u_1} {xL : } (xR : ) (j : (xR i).LeftMoves) :
((xR i).moveLeft j).Subsequent (SetTheory.PGame.mk xl xr xL xR)

### Basic pre-games #

The pre-game Zero is defined by 0 = { | }.

Equations
@[simp]
@[simp]
Equations

The pre-game One is defined by 1 = { 0 | }.

Equations
@[simp]
@[simp]
@[simp]

### Pre-game order relations #

The less or equal relation on pre-games.

If 0 ≤ x, then Left can win x as the second player.

Equations
• One or more equations did not get rendered due to their size.

The less or fuzzy relation on pre-games.

If 0 ⧏ x, then Left can win x as the first player.

Equations
Instances For

The less or fuzzy relation on pre-games.

If 0 ⧏ x, then Left can win x as the first player.

Equations
Instances For
@[simp]
@[simp]
theorem LE.le.not_gf {x : SetTheory.PGame} {y : SetTheory.PGame} :
x y¬y.LF x
theorem SetTheory.PGame.le_iff_forall_lf {x : SetTheory.PGame} {y : SetTheory.PGame} :
x y (∀ (i : x.LeftMoves), (x.moveLeft i).LF y) ∀ (j : y.RightMoves), x.LF (y.moveRight j)

Definition of x ≤ y on pre-games, in terms of ⧏.

The ordering here is chosen so that And.left refer to moves by Left, and And.right refer to moves by Right.

@[simp]
theorem SetTheory.PGame.mk_le_mk {xl : Type u_1} {xr : Type u_1} {xL : } {xR : } {yl : Type u_1} {yr : Type u_1} {yL : } {yR : } :
SetTheory.PGame.mk xl xr xL xR SetTheory.PGame.mk yl yr yL yR (∀ (i : xl), (xL i).LF (SetTheory.PGame.mk yl yr yL yR)) ∀ (j : yr), (SetTheory.PGame.mk xl xr xL xR).LF (yR j)

Definition of x ≤ y on pre-games built using the constructor.

theorem SetTheory.PGame.le_of_forall_lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h₁ : ∀ (i : x.LeftMoves), (x.moveLeft i).LF y) (h₂ : ∀ (j : y.RightMoves), x.LF (y.moveRight j)) :
x y
theorem SetTheory.PGame.lf_iff_exists_le {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.LF y (∃ (i : y.LeftMoves), x y.moveLeft i) ∃ (j : x.RightMoves), x.moveRight j y

Definition of x ⧏ y on pre-games, in terms of ≤.

The ordering here is chosen so that or.inl refer to moves by Left, and or.inr refer to moves by Right.

@[simp]
theorem SetTheory.PGame.mk_lf_mk {xl : Type u_1} {xr : Type u_1} {xL : } {xR : } {yl : Type u_1} {yr : Type u_1} {yL : } {yR : } :
(SetTheory.PGame.mk xl xr xL xR).LF (SetTheory.PGame.mk yl yr yL yR) (∃ (i : yl), SetTheory.PGame.mk xl xr xL xR yL i) ∃ (j : xr), xR j SetTheory.PGame.mk yl yr yL yR

Definition of x ⧏ y on pre-games built using the constructor.

theorem SetTheory.PGame.moveLeft_lf_of_le {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x y) (i : x.LeftMoves) :
(x.moveLeft i).LF y
theorem LE.le.moveLeft_lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x y) (i : x.LeftMoves) :
(x.moveLeft i).LF y

Alias of SetTheory.PGame.moveLeft_lf_of_le.

theorem SetTheory.PGame.lf_moveRight_of_le {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x y) (j : y.RightMoves) :
x.LF (y.moveRight j)
theorem LE.le.lf_moveRight {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x y) (j : y.RightMoves) :
x.LF (y.moveRight j)

Alias of SetTheory.PGame.lf_moveRight_of_le.

theorem SetTheory.PGame.lf_of_moveRight_le {x : SetTheory.PGame} {y : SetTheory.PGame} {j : x.RightMoves} (h : x.moveRight j y) :
x.LF y
theorem SetTheory.PGame.lf_of_le_moveLeft {x : SetTheory.PGame} {y : SetTheory.PGame} {i : y.LeftMoves} (h : x y.moveLeft i) :
x.LF y
theorem SetTheory.PGame.lf_of_le_mk {xl : Type u_1} {xr : Type u_1} {xL : } {xR : } {y : SetTheory.PGame} :
SetTheory.PGame.mk xl xr xL xR y∀ (i : xl), (xL i).LF y
theorem SetTheory.PGame.lf_of_mk_le {x : SetTheory.PGame} {yl : Type u_1} {yr : Type u_1} {yL : } {yR : } :
x SetTheory.PGame.mk yl yr yL yR∀ (j : yr), x.LF (yR j)
theorem SetTheory.PGame.mk_lf_of_le {xl : Type u_1} {xr : Type u_1} {y : SetTheory.PGame} {j : xr} (xL : ) {xR : } :
xR j y(SetTheory.PGame.mk xl xr xL xR).LF y
theorem SetTheory.PGame.lf_mk_of_le {x : SetTheory.PGame} {yl : Type u_1} {yr : Type u_1} {yL : } (yR : ) {i : yl} :
x yL ix.LF (SetTheory.PGame.mk yl yr yL yR)
theorem SetTheory.PGame.lt_of_le_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h₁ : x y) (h₂ : x.LF y) :
x < y
theorem SetTheory.PGame.lf_of_lt {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x < y) :
x.LF y
theorem LT.lt.lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x < y) :
x.LF y

Alias of SetTheory.PGame.lf_of_lt.

theorem SetTheory.PGame.lf_of_le_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) (h₂ : y.LF z) :
x.LF z
instance SetTheory.PGame.instTransLeLF :
Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x.LF x_1) fun (x x_1 : SetTheory.PGame) => x.LF x_1
Equations
theorem SetTheory.PGame.lf_of_lf_of_le {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y z) :
x.LF z
instance SetTheory.PGame.instTransLFLe :
Trans (fun (x x_1 : SetTheory.PGame) => x.LF x_1) (fun (x x_1 : SetTheory.PGame) => x x_1) fun (x x_1 : SetTheory.PGame) => x.LF x_1
Equations
theorem LE.le.trans_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) (h₂ : y.LF z) :
x.LF z

Alias of SetTheory.PGame.lf_of_le_of_lf.

theorem SetTheory.PGame.LF.trans_le {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y z) :
x.LF z

Alias of SetTheory.PGame.lf_of_lf_of_le.

theorem SetTheory.PGame.lf_of_lt_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x < y) (h₂ : y.LF z) :
x.LF z
theorem SetTheory.PGame.lf_of_lf_of_lt {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y < z) :
x.LF z
theorem LT.lt.trans_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x < y) (h₂ : y.LF z) :
x.LF z

Alias of SetTheory.PGame.lf_of_lt_of_lf.

theorem SetTheory.PGame.LF.trans_lt {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y < z) :
x.LF z

Alias of SetTheory.PGame.lf_of_lf_of_lt.

theorem SetTheory.PGame.moveLeft_lf {x : SetTheory.PGame} (i : x.LeftMoves) :
(x.moveLeft i).LF x
theorem SetTheory.PGame.lf_moveRight {x : SetTheory.PGame} (j : x.RightMoves) :
x.LF (x.moveRight j)
theorem SetTheory.PGame.lf_mk {xl : Type u_1} {xr : Type u_1} (xL : ) (xR : ) (i : xl) :
(xL i).LF (SetTheory.PGame.mk xl xr xL xR)
theorem SetTheory.PGame.mk_lf {xl : Type u_1} {xr : Type u_1} (xL : ) (xR : ) (j : xr) :
(SetTheory.PGame.mk xl xr xL xR).LF (xR j)
theorem SetTheory.PGame.le_of_forall_lt {x : SetTheory.PGame} {y : SetTheory.PGame} (h₁ : ∀ (i : x.LeftMoves), x.moveLeft i < y) (h₂ : ∀ (j : y.RightMoves), x < y.moveRight j) :
x y

This special case of PGame.le_of_forall_lf is useful when dealing with surreals, where < is preferred over ⧏.

theorem SetTheory.PGame.le_def {x : SetTheory.PGame} {y : SetTheory.PGame} :
x y (∀ (i : x.LeftMoves), (∃ (i' : y.LeftMoves), x.moveLeft i y.moveLeft i') ∃ (j : (x.moveLeft i).RightMoves), (x.moveLeft i).moveRight j y) ∀ (j : y.RightMoves), (∃ (i : (y.moveRight j).LeftMoves), x (y.moveRight j).moveLeft i) ∃ (j' : x.RightMoves), x.moveRight j' y.moveRight j

The definition of x ≤ y on pre-games, in terms of ≤ two moves later.

theorem SetTheory.PGame.lf_def {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.LF y (∃ (i : y.LeftMoves), (∀ (i' : x.LeftMoves), (x.moveLeft i').LF (y.moveLeft i)) ∀ (j : (y.moveLeft i).RightMoves), x.LF ((y.moveLeft i).moveRight j)) ∃ (j : x.RightMoves), (∀ (i : (x.moveRight j).LeftMoves), ((x.moveRight j).moveLeft i).LF y) ∀ (j' : y.RightMoves), (x.moveRight j).LF (y.moveRight j')

The definition of x ⧏ y on pre-games, in terms of ⧏ two moves later.

theorem SetTheory.PGame.zero_le_lf {x : SetTheory.PGame} :
0 x ∀ (j : x.RightMoves), SetTheory.PGame.LF 0 (x.moveRight j)

The definition of 0 ≤ x on pre-games, in terms of 0 ⧏.

theorem SetTheory.PGame.le_zero_lf {x : SetTheory.PGame} :
x 0 ∀ (i : x.LeftMoves), (x.moveLeft i).LF 0

The definition of x ≤ 0 on pre-games, in terms of ⧏ 0.

theorem SetTheory.PGame.zero_lf_le {x : SetTheory.PGame} :
∃ (i : x.LeftMoves), 0 x.moveLeft i

The definition of 0 ⧏ x on pre-games, in terms of 0 ≤.

theorem SetTheory.PGame.lf_zero_le {x : SetTheory.PGame} :
x.LF 0 ∃ (j : x.RightMoves), x.moveRight j 0

The definition of x ⧏ 0 on pre-games, in terms of ≤ 0.

theorem SetTheory.PGame.zero_le {x : SetTheory.PGame} :
0 x ∀ (j : x.RightMoves), ∃ (i : (x.moveRight j).LeftMoves), 0 (x.moveRight j).moveLeft i

The definition of 0 ≤ x on pre-games, in terms of 0 ≤ two moves later.

theorem SetTheory.PGame.le_zero {x : SetTheory.PGame} :
x 0 ∀ (i : x.LeftMoves), ∃ (j : (x.moveLeft i).RightMoves), (x.moveLeft i).moveRight j 0

The definition of x ≤ 0 on pre-games, in terms of ≤ 0 two moves later.

theorem SetTheory.PGame.zero_lf {x : SetTheory.PGame} :
∃ (i : x.LeftMoves), ∀ (j : (x.moveLeft i).RightMoves), SetTheory.PGame.LF 0 ((x.moveLeft i).moveRight j)

The definition of 0 ⧏ x on pre-games, in terms of 0 ⧏ two moves later.

theorem SetTheory.PGame.lf_zero {x : SetTheory.PGame} :
x.LF 0 ∃ (j : x.RightMoves), ∀ (i : (x.moveRight j).LeftMoves), ((x.moveRight j).moveLeft i).LF 0

The definition of x ⧏ 0 on pre-games, in terms of ⧏ 0 two moves later.

noncomputable def SetTheory.PGame.rightResponse {x : SetTheory.PGame} (h : x 0) (i : x.LeftMoves) :
(x.moveLeft i).RightMoves

Given a game won by the right player when they play second, provide a response to any move by left.

Equations
Instances For
theorem SetTheory.PGame.rightResponse_spec {x : SetTheory.PGame} (h : x 0) (i : x.LeftMoves) :
(x.moveLeft i).moveRight 0

Show that the response for right provided by rightResponse preserves the right-player-wins condition.

noncomputable def SetTheory.PGame.leftResponse {x : SetTheory.PGame} (h : 0 x) (j : x.RightMoves) :
(x.moveRight j).LeftMoves

Given a game won by the left player when they play second, provide a response to any move by right.

Equations
Instances For
theorem SetTheory.PGame.leftResponse_spec {x : SetTheory.PGame} (h : 0 x) (j : x.RightMoves) :
0 (x.moveRight j).moveLeft

Show that the response for left provided by leftResponse preserves the left-player-wins condition.

theorem SetTheory.PGame.bddAbove_range_of_small {ι : Type u_1} [] (f : ) :

A small family of pre-games is bounded above.

A small set of pre-games is bounded above.

theorem SetTheory.PGame.bddBelow_range_of_small {ι : Type u_1} [] (f : ) :

A small family of pre-games is bounded below.

A small set of pre-games is bounded below.

The equivalence relation on pre-games. Two pre-games x, y are equivalent if x ≤ y and y ≤ x.

If x ≈ 0, then the second player can always win x.

Equations
Instances For
theorem SetTheory.PGame.le_of_le_of_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) (h₂ : y z) :
x z
instance SetTheory.PGame.instTransLeEquiv :
Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x x_1) fun (x x_1 : SetTheory.PGame) => x x_1
Equations
instance SetTheory.PGame.instTransEquivLe :
Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x x_1) fun (x x_1 : SetTheory.PGame) => x x_1
Equations
theorem SetTheory.PGame.le_congr_imp {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) (h : x₁ y₁) :
x₂ y₂
theorem SetTheory.PGame.le_congr {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
x₁ y₁ x₂ y₂
theorem SetTheory.PGame.le_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx : x₁ x₂) :
x₁ y x₂ y
theorem SetTheory.PGame.le_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hy : y₁ y₂) :
x y₁ x y₂
theorem SetTheory.PGame.lf_congr {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
x₁.LF y₁ x₂.LF y₂
theorem SetTheory.PGame.lf_congr_imp {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
x₁.LF y₁x₂.LF y₂
theorem SetTheory.PGame.lf_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx : x₁ x₂) :
x₁.LF y x₂.LF y
theorem SetTheory.PGame.lf_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hy : y₁ y₂) :
x.LF y₁ x.LF y₂
theorem SetTheory.PGame.lf_of_lf_of_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y z) :
x.LF z
theorem SetTheory.PGame.lf_of_equiv_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) :
y.LF zx.LF z
theorem SetTheory.PGame.lt_of_lt_of_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x < y) (h₂ : y z) :
x < z
instance SetTheory.PGame.instTransEquivLt :
Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x < x_1) fun (x x_1 : SetTheory.PGame) => x < x_1
Equations
theorem SetTheory.PGame.lt_congr_imp {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) (h : x₁ < y₁) :
x₂ < y₂
theorem SetTheory.PGame.lt_congr {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
x₁ < y₁ x₂ < y₂
theorem SetTheory.PGame.lt_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx : x₁ x₂) :
x₁ < y x₂ < y
theorem SetTheory.PGame.lt_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hy : y₁ y₂) :
x < y₁ x < y₂
theorem SetTheory.PGame.equiv_congr_left {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} :
y₁ y₂ ∀ (x₁ : SetTheory.PGame), x₁ y₁ x₁ y₂
theorem SetTheory.PGame.equiv_congr_right {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} :
x₁ x₂ ∀ (y₁ : SetTheory.PGame), x₁ y₁ x₂ y₁
theorem SetTheory.PGame.equiv_of_mk_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} (L : x.LeftMoves y.LeftMoves) (R : x.RightMoves y.RightMoves) (hl : ∀ (i : x.LeftMoves), x.moveLeft i y.moveLeft (L i)) (hr : ∀ (j : x.RightMoves), x.moveRight j y.moveRight (R j)) :
x y

The fuzzy, confused, or incomparable relation on pre-games.

If x ‖ 0, then the first player can always win x.

Equations
• x.Fuzzy y = (x.LF y y.LF x)
Instances For

The fuzzy, confused, or incomparable relation on pre-games.

If x ‖ 0, then the first player can always win x.

Equations
Instances For
theorem SetTheory.PGame.Fuzzy.swap {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.Fuzzy yy.Fuzzy x
Equations
theorem SetTheory.PGame.lf_of_fuzzy {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x.Fuzzy y) :
x.LF y
theorem SetTheory.PGame.Fuzzy.lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x.Fuzzy y) :
x.LF y

Alias of SetTheory.PGame.lf_of_fuzzy.

theorem SetTheory.PGame.lt_or_fuzzy_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.LF yx < y x.Fuzzy y
theorem SetTheory.PGame.fuzzy_congr {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
x₁.Fuzzy y₁ x₂.Fuzzy y₂
theorem SetTheory.PGame.fuzzy_congr_imp {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
x₁.Fuzzy y₁x₂.Fuzzy y₂
theorem SetTheory.PGame.fuzzy_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx : x₁ x₂) :
x₁.Fuzzy y x₂.Fuzzy y
theorem SetTheory.PGame.fuzzy_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hy : y₁ y₂) :
x.Fuzzy y₁ x.Fuzzy y₂
theorem SetTheory.PGame.fuzzy_of_fuzzy_of_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.Fuzzy y) (h₂ : y z) :
x.Fuzzy z
theorem SetTheory.PGame.fuzzy_of_equiv_of_fuzzy {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) (h₂ : y.Fuzzy z) :
x.Fuzzy z

Exactly one of the following is true (although we don't prove this here).

### Relabellings #

Relabelling x y says that x and y are really the same game, just dressed up differently. Specifically, there is a bijection between the moves for Left in x and in y, and similarly for Right, and under these bijections we inductively have Relabellings for the consequent games.

• mk: {x y : SetTheory.PGame} → (L : x.LeftMoves y.LeftMoves) → (R : x.RightMoves y.RightMoves) → ((i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i)))((j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j)))x.Relabelling y
Instances For

Relabelling x y says that x and y are really the same game, just dressed up differently. Specifically, there is a bijection between the moves for Left in x and in y, and similarly for Right, and under these bijections we inductively have Relabellings for the consequent games.

Equations
Instances For
def SetTheory.PGame.Relabelling.mk' {x : SetTheory.PGame} {y : SetTheory.PGame} (L : y.LeftMoves x.LeftMoves) (R : y.RightMoves x.RightMoves) (hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)) (hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)) :
x.Relabelling y

A constructor for relabellings swapping the equivalences.

Equations
Instances For
def SetTheory.PGame.Relabelling.leftMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.Relabelling yx.LeftMoves y.LeftMoves

The equivalence between left moves of x and y given by the relabelling.

Equations
• x.leftMovesEquiv = match x with | => L
Instances For
@[simp]
theorem SetTheory.PGame.Relabelling.mk_leftMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} {L : x.LeftMoves y.LeftMoves} {R : x.RightMoves y.RightMoves} {hL : (i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))} {hR : (j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))} :
().leftMovesEquiv = L
@[simp]
theorem SetTheory.PGame.Relabelling.mk'_leftMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} {L : y.LeftMoves x.LeftMoves} {R : y.RightMoves x.RightMoves} {hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)} {hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)} :
().leftMovesEquiv = L.symm
def SetTheory.PGame.Relabelling.rightMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.Relabelling yx.RightMoves y.RightMoves

The equivalence between right moves of x and y given by the relabelling.

Equations
• x.rightMovesEquiv = match x with | => R
Instances For
@[simp]
theorem SetTheory.PGame.Relabelling.mk_rightMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} {L : x.LeftMoves y.LeftMoves} {R : x.RightMoves y.RightMoves} {hL : (i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))} {hR : (j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))} :
().rightMovesEquiv = R
@[simp]
theorem SetTheory.PGame.Relabelling.mk'_rightMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} {L : y.LeftMoves x.LeftMoves} {R : y.RightMoves x.RightMoves} {hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)} {hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)} :
().rightMovesEquiv = R.symm
def SetTheory.PGame.Relabelling.moveLeft {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (i : x.LeftMoves) :
(x.moveLeft i).Relabelling (y.moveLeft (r.leftMovesEquiv i))

A left move of x is a relabelling of a left move of y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.Relabelling.moveLeftSymm {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (i : y.LeftMoves) :
(x.moveLeft (r.leftMovesEquiv.symm i)).Relabelling (y.moveLeft i)

A left move of y is a relabelling of a left move of x.

Equations
• x✝.moveLeftSymm x = match x✝, x with | , i => id (.mp (hL (L.symm i)))
Instances For
def SetTheory.PGame.Relabelling.moveRight {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (i : x.RightMoves) :
(x.moveRight i).Relabelling (y.moveRight (r.rightMovesEquiv i))

A right move of x is a relabelling of a right move of y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.Relabelling.moveRightSymm {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (i : y.RightMoves) :
(x.moveRight (r.rightMovesEquiv.symm i)).Relabelling (y.moveRight i)

A right move of y is a relabelling of a right move of x.

Equations
• x✝.moveRightSymm x = match x✝, x with | , i => id (.mp (hR (R.symm i)))
Instances For
@[irreducible]

The identity relabelling.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• = { default := }
def SetTheory.PGame.Relabelling.symm {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.Relabelling yy.Relabelling x

Flip a relabelling.

Equations
Instances For
@[irreducible]
theorem SetTheory.PGame.Relabelling.le {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) :
x y
theorem SetTheory.PGame.Relabelling.ge {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) :
y x
theorem SetTheory.PGame.Relabelling.equiv {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) :
x y

A relabelling lets us prove equivalence of games.

def SetTheory.PGame.Relabelling.trans {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} :
x.Relabelling yy.Relabelling zx.Relabelling z

Transitivity of relabelling.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SetTheory.PGame.Relabelling.isEmpty (x : SetTheory.PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] :
x.Relabelling 0

Any game without left or right moves is a relabelling of 0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SetTheory.PGame.Equiv.isEmpty (x : SetTheory.PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] :
x 0
instance SetTheory.PGame.instCoeRelabellingEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} :
Coe (x.Relabelling y) (x y)
Equations
• SetTheory.PGame.instCoeRelabellingEquiv = { coe := }
def SetTheory.PGame.relabel {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) :

Replace the types indexing the next moves for Left and Right by equivalent types.

Equations
Instances For
@[simp]
theorem SetTheory.PGame.relabel_moveLeft' {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) (i : xl') :
().moveLeft i = x.moveLeft (el i)
theorem SetTheory.PGame.relabel_moveLeft {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) (i : x.LeftMoves) :
().moveLeft (el.symm i) = x.moveLeft i
@[simp]
theorem SetTheory.PGame.relabel_moveRight' {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) (j : xr') :
().moveRight j = x.moveRight (er j)
theorem SetTheory.PGame.relabel_moveRight {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) (j : x.RightMoves) :
().moveRight (er.symm j) = x.moveRight j
def SetTheory.PGame.relabelRelabelling {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) :
x.Relabelling ()

The game obtained by relabelling the next moves is a relabelling of the original game.

Equations
• One or more equations did not get rendered due to their size.
Instances For

### Negation #

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

Equations
Instances For
@[simp]
theorem SetTheory.PGame.neg_def {xl : Type u_1} {xr : Type u_1} {xL : } {xR : } :
-SetTheory.PGame.mk xl xr xL xR = SetTheory.PGame.mk xr xl (fun (j : xr) => -xR j) fun (i : xl) => -xL i
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem SetTheory.PGame.neg_ofLists (L : ) (R : ) :
= SetTheory.PGame.ofLists (List.map (fun (x : SetTheory.PGame) => -x) R) (List.map (fun (x : SetTheory.PGame) => -x) L)
theorem SetTheory.PGame.isOption_neg {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.IsOption (-y) (-x).IsOption y
@[simp]
theorem SetTheory.PGame.isOption_neg_neg {x : SetTheory.PGame} {y : SetTheory.PGame} :
(-x).IsOption (-y) x.IsOption y
theorem SetTheory.PGame.leftMoves_neg (x : SetTheory.PGame) :
(-x).LeftMoves = x.RightMoves
theorem SetTheory.PGame.rightMoves_neg (x : SetTheory.PGame) :
(-x).RightMoves = x.LeftMoves
def SetTheory.PGame.toLeftMovesNeg {x : SetTheory.PGame} :
x.RightMoves (-x).LeftMoves

Turns a right move for x into a left move for -x and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations
• SetTheory.PGame.toLeftMovesNeg =
Instances For
def SetTheory.PGame.toRightMovesNeg {x : SetTheory.PGame} :
x.LeftMoves (-x).RightMoves

Turns a left move for x into a right move for -x and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations
• SetTheory.PGame.toRightMovesNeg =
Instances For
theorem SetTheory.PGame.moveLeft_neg {x : SetTheory.PGame} (i : x.RightMoves) :
(-x).moveLeft (SetTheory.PGame.toLeftMovesNeg i) = -x.moveRight i
@[simp]
theorem SetTheory.PGame.moveLeft_neg' {x : SetTheory.PGame} (i : (-x).LeftMoves) :
(-x).moveLeft i = -x.moveRight (SetTheory.PGame.toLeftMovesNeg.symm i)
theorem SetTheory.PGame.moveRight_neg {x : SetTheory.PGame} (i : x.LeftMoves) :
(-x).moveRight (SetTheory.PGame.toRightMovesNeg i) = -x.moveLeft i
@[simp]
theorem SetTheory.PGame.moveRight_neg' {x : SetTheory.PGame} (i : (-x).RightMoves) :
(-x).moveRight i = -x.moveLeft (SetTheory.PGame.toRightMovesNeg.symm i)
theorem SetTheory.PGame.moveLeft_neg_symm {x : SetTheory.PGame} (i : (-x).RightMoves) :
x.moveLeft (SetTheory.PGame.toRightMovesNeg.symm i) = -(-x).moveRight i
theorem SetTheory.PGame.moveLeft_neg_symm' {x : SetTheory.PGame} (i : x.LeftMoves) :
x.moveLeft i = -(-x).moveRight (SetTheory.PGame.toRightMovesNeg i)
theorem SetTheory.PGame.moveRight_neg_symm {x : SetTheory.PGame} (i : (-x).LeftMoves) :
x.moveRight (SetTheory.PGame.toLeftMovesNeg.symm i) = -(-x).moveLeft i
theorem SetTheory.PGame.moveRight_neg_symm' {x : SetTheory.PGame} (i : x.RightMoves) :
x.moveRight i = -(-x).moveLeft (SetTheory.PGame.toLeftMovesNeg i)
def SetTheory.PGame.Relabelling.negCongr {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.Relabelling y(-x).Relabelling (-y)

If x has the same moves as y, then -x has the same moves as -y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem SetTheory.PGame.neg_fuzzy_neg_iff {x : SetTheory.PGame} {y : SetTheory.PGame} :
(-x).Fuzzy (-y) x.Fuzzy y
theorem SetTheory.PGame.neg_fuzzy_iff {x : SetTheory.PGame} {y : SetTheory.PGame} :
(-x).Fuzzy y x.Fuzzy (-y)
@[simp]
theorem SetTheory.PGame.neg_fuzzy_zero_iff {x : SetTheory.PGame} :
(-x).Fuzzy 0 x.Fuzzy 0

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

Equations
• One or more equations did not get rendered due to their size.

The pre-game ((0+1)+⋯)+1.

Equations
@[simp]
theorem SetTheory.PGame.nat_succ (n : ) :
(n + 1) = n + 1
instance SetTheory.PGame.isEmpty_leftMoves_add (x : SetTheory.PGame) (y : SetTheory.PGame) [IsEmpty x.LeftMoves] [IsEmpty y.LeftMoves] :
IsEmpty (x + y).LeftMoves
Equations
• =
instance SetTheory.PGame.isEmpty_rightMoves_add (x : SetTheory.PGame) (y : SetTheory.PGame) [IsEmpty x.RightMoves] [IsEmpty y.RightMoves] :
IsEmpty (x + y).RightMoves
Equations
• =
@[irreducible]

x + 0 has exactly the same moves as x.

Equations
• One or more equations did not get rendered due to their size.
Instances For

x + 0 is equivalent to x.

0 + x has exactly the same moves as x.

Equations
• One or more equations did not get rendered due to their size.
Instances For

0 + x is equivalent to x.

theorem SetTheory.PGame.leftMoves_add (x : SetTheory.PGame) (y : SetTheory.PGame) :
(x + y).LeftMoves = (x.LeftMoves y.LeftMoves)
theorem SetTheory.PGame.rightMoves_add (x : SetTheory.PGame) (y : SetTheory.PGame) :
(x + y).RightMoves = (x.RightMoves y.RightMoves)
def SetTheory.PGame.toLeftMovesAdd {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.LeftMoves y.LeftMoves (x + y).LeftMoves

Converts a left move for x or y into a left move for x + y and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations
Instances For
def SetTheory.PGame.toRightMovesAdd {x : SetTheory.PGame} {y : SetTheory.PGame} :
x.RightMoves y.RightMoves (x + y).RightMoves

Converts a right move for x or y into a right move for x + y and vice versa.

Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

Equations
Instances For
@[simp]
theorem SetTheory.PGame.mk_add_moveLeft_inl {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : } {xR : } {yL : } {yR : } {i : xl} :
(SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveLeft () = (SetTheory.PGame.mk xl xr xL xR).moveLeft i + SetTheory.PGame.mk yl yr yL yR
@[simp]
theorem SetTheory.PGame.add_moveLeft_inl {x : SetTheory.PGame} (y : SetTheory.PGame) (i : x.LeftMoves) :
(x + y).moveLeft (SetTheory.PGame.toLeftMovesAdd ()) = x.moveLeft i + y
@[simp]
theorem SetTheory.PGame.mk_add_moveRight_inl {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : } {xR : } {yL : } {yR : } {i : xr} :
(SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveRight () = (SetTheory.PGame.mk xl xr xL xR).moveRight i + SetTheory.PGame.mk yl yr yL yR
@[simp]
theorem SetTheory.PGame.add_moveRight_inl {x : SetTheory.PGame} (y : SetTheory.PGame) (i : x.RightMoves) :
(x + y).moveRight (SetTheory.PGame.toRightMovesAdd ()) = x.moveRight i + y
@[simp]
theorem SetTheory.PGame.mk_add_moveLeft_inr {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : } {xR : } {yL : } {yR : } {i : yl} :
(SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveLeft () = SetTheory.PGame.mk xl xr xL xR + (SetTheory.PGame.mk yl yr yL yR).moveLeft i
@[simp]
theorem SetTheory.PGame.add_moveLeft_inr (x : SetTheory.PGame) {y : SetTheory.PGame} (i : y.LeftMoves) :
(x + y).moveLeft (SetTheory.PGame.toLeftMovesAdd ()) = x + y.moveLeft i
@[simp]
theorem SetTheory.PGame.mk_add_moveRight_inr {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : } {xR : } {yL : } {yR : } {i : yr} :
(SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveRight () = SetTheory.PGame.mk xl xr xL xR + (SetTheory.PGame.mk yl yr yL yR).moveRight i
@[simp]
theorem SetTheory.PGame.add_moveRight_inr (x : SetTheory.PGame) {y : SetTheory.PGame} (i : y.RightMoves) :
(x + y).moveRight (SetTheory.PGame.toRightMovesAdd ()) = x + y.moveRight i
theorem SetTheory.PGame.leftMoves_add_cases {x : SetTheory.PGame} {y : SetTheory.PGame} (k : (x + y).LeftMoves) {P : (x + y).LeftMovesProp} (hl : ∀ (i : x.LeftMoves), P (SetTheory.PGame.toLeftMovesAdd ())) (hr : ∀ (i : y.LeftMoves), P (SetTheory.PGame.toLeftMovesAdd ())) :
P k
theorem SetTheory.PGame.rightMoves_add_cases {x : SetTheory.PGame} {y : SetTheory.PGame} (k : (x + y).RightMoves) {P : (x + y).RightMovesProp} (hl : ∀ (j : x.RightMoves), P (SetTheory.PGame.toRightMovesAdd ())) (hr : ∀ (j : y.RightMoves), P (SetTheory.PGame.toRightMovesAdd ())) :
P k
instance SetTheory.PGame.isEmpty_nat_rightMoves (n : ) :
IsEmpty (n).RightMoves
Equations
• =
@[irreducible]
def SetTheory.PGame.Relabelling.addCongr {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} :
w.Relabelling xy.Relabelling z(w + y).Relabelling (x + z)

If w has the same moves as x and y has the same moves as z, then w + y has the same moves as x + z.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
@[simp]
def SetTheory.PGame.Relabelling.subCongr {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : w.Relabelling x) (h₂ : y.Relabelling z) :
(w - y).Relabelling (x - z)

If w has the same moves as x and y has the same moves as z, then w - y has the same moves as x - z.

Equations
• h₁.subCongr h₂ = h₁.addCongr h₂.negCongr
Instances For
@[irreducible]
def SetTheory.PGame.negAddRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) :
(-(x + y)).Relabelling (-x + -y)

-(x + y) has exactly the same moves as -x + -y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
def SetTheory.PGame.addCommRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) :
(x + y).Relabelling (y + x)

x + y has exactly the same moves as y + x.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
def SetTheory.PGame.addAssocRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) :
(x + y + z).Relabelling (x + (y + z))

(x + y) + z has exactly the same moves as x + (y + z).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SetTheory.PGame.add_lf_add_right {y : SetTheory.PGame} {z : SetTheory.PGame} (h : y.LF z) (x : SetTheory.PGame) :
(y + x).LF (z + x)
theorem SetTheory.PGame.add_lf_add_left {y : SetTheory.PGame} {z : SetTheory.PGame} (h : y.LF z) (x : SetTheory.PGame) :
(x + y).LF (x + z)
theorem SetTheory.PGame.add_lf_add_of_lf_of_le {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (hwx : w.LF x) (hyz : y z) :
(w + y).LF (x + z)
theorem SetTheory.PGame.add_lf_add_of_le_of_lf {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (hwx : w x) (hyz : y.LF z) :
(w + y).LF (x + z)
theorem SetTheory.PGame.add_congr {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : w x) (h₂ : y z) :
w + y x + z
theorem SetTheory.PGame.sub_congr {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : w x) (h₂ : y z) :
w - y x - z

### Special pre-games #

The pre-game star, which is fuzzy with zero.

Equations
Instances For
@[simp]