Combinatorial games.

In this file we construct an instance OrderedAddCommGroup SetTheory.Game.

Multiplication on pre-games

We define the operations of multiplication and inverse on pre-games, and prove a few basic theorems about them. Multiplication is not well-behaved under equivalence of pre-games i.e. x ≈ y does not imply x * z ≈ y * z. Hence, multiplication is not a well-defined operation on games. Nevertheless, the abelian group structure on games allows us to simplify many proofs for pre-games.

@[inline, reducible]

abbrev SetTheory.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

• SetTheory.Game = Quotient SetTheory.PGame.setoid

def SetTheory.Game.neg : SetTheory.Game → SetTheory.Game

Negation of games.

Equations

• SetTheory.Game.neg = Quot.lift (fun (x : SetTheory.PGame) => ⟦-x⟧) SetTheory.Game.neg.proof_1

instance SetTheory.Game.instAddCommGroupWithOneGame : AddCommGroupWithOne SetTheory.Game

Equations

• SetTheory.Game.instAddCommGroupWithOneGame = AddCommGroupWithOne.mk

instance SetTheory.Game.instInhabitedGame : Inhabited SetTheory.Game

Equations

• SetTheory.Game.instInhabitedGame = { default := 0 }

instance SetTheory.Game.instPartialOrderGame : PartialOrder SetTheory.Game

Equations

• SetTheory.Game.instPartialOrderGame = PartialOrder.mk SetTheory.Game.instPartialOrderGame.proof_6

def SetTheory.Game.LF : SetTheory.Game → SetTheory.Game → Prop

The less or fuzzy relation on games.

If 0 ⧏ x (less or fuzzy with), then Left can win x as the first player.

Equations

• SetTheory.Game.LF = Quotient.lift₂ SetTheory.PGame.LF SetTheory.Game.LF.proof_1

@[simp]

theorem SetTheory.Game.not_le {x : SetTheory.Game} {y : SetTheory.Game} : ¬x ≤ y ↔ SetTheory.Game.LF y x

On Game, simp-normal inequalities should use as few negations as possible.

@[simp]

theorem SetTheory.Game.not_lf {x : SetTheory.Game} {y : SetTheory.Game} : ¬SetTheory.Game.LF x y ↔ y ≤ x

On Game, simp-normal inequalities should use as few negations as possible.

instance SetTheory.Game.instIsTrichotomousGameLF : IsTrichotomous SetTheory.Game SetTheory.Game.LF

Equations

• SetTheory.Game.instIsTrichotomousGameLF = (_ : IsTrichotomous SetTheory.Game SetTheory.Game.LF)

It can be useful to use these lemmas to turn PGame inequalities into Game inequalities, as the AddCommGroup structure on Game often simplifies many proofs.

theorem SetTheory.Game.PGame.le_iff_game_le {x : SetTheory.PGame} {y : SetTheory.PGame} : x ≤ y ↔ ⟦x⟧ ≤ ⟦y⟧

theorem SetTheory.Game.PGame.lf_iff_game_lf {x : SetTheory.PGame} {y : SetTheory.PGame} : SetTheory.PGame.LF x y ↔ SetTheory.Game.LF ⟦x⟧ ⟦y⟧

theorem SetTheory.Game.PGame.lt_iff_game_lt {x : SetTheory.PGame} {y : SetTheory.PGame} : x < y ↔ ⟦x⟧ < ⟦y⟧

theorem SetTheory.Game.PGame.equiv_iff_game_eq {x : SetTheory.PGame} {y : SetTheory.PGame} : x ≈ y ↔ ⟦x⟧ = ⟦y⟧

def SetTheory.Game.Fuzzy : SetTheory.Game → SetTheory.Game → Prop

The fuzzy, confused, or incomparable relation on games.

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

Equations

• SetTheory.Game.Fuzzy = Quotient.lift₂ SetTheory.PGame.Fuzzy SetTheory.Game.Fuzzy.proof_1

theorem SetTheory.Game.PGame.fuzzy_iff_game_fuzzy {x : SetTheory.PGame} {y : SetTheory.PGame} : SetTheory.PGame.Fuzzy x y ↔ SetTheory.Game.Fuzzy ⟦x⟧ ⟦y⟧

instance SetTheory.Game.covariantClass_add_le : CovariantClass SetTheory.Game SetTheory.Game (fun (x x_1 : SetTheory.Game) => x + x_1) fun (x x_1 : SetTheory.Game) => x ≤ x_1

Equations

• SetTheory.Game.covariantClass_add_le = (_ : CovariantClass SetTheory.Game SetTheory.Game (fun (x x_1 : SetTheory.Game) => x + x_1) fun (x x_1 : SetTheory.Game) => x ≤ x_1)

instance SetTheory.Game.covariantClass_swap_add_le : CovariantClass SetTheory.Game SetTheory.Game (Function.swap fun (x x_1 : SetTheory.Game) => x + x_1) fun (x x_1 : SetTheory.Game) => x ≤ x_1

Equations

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

instance SetTheory.Game.covariantClass_add_lt : CovariantClass SetTheory.Game SetTheory.Game (fun (x x_1 : SetTheory.Game) => x + x_1) fun (x x_1 : SetTheory.Game) => x < x_1

Equations

• SetTheory.Game.covariantClass_add_lt = (_ : CovariantClass SetTheory.Game SetTheory.Game (fun (x x_1 : SetTheory.Game) => x + x_1) fun (x x_1 : SetTheory.Game) => x < x_1)

instance SetTheory.Game.covariantClass_swap_add_lt : CovariantClass SetTheory.Game SetTheory.Game (Function.swap fun (x x_1 : SetTheory.Game) => x + x_1) fun (x x_1 : SetTheory.Game) => x < x_1

Equations

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

theorem SetTheory.Game.add_lf_add_right {b : SetTheory.Game} {c : SetTheory.Game} : SetTheory.Game.LF b c → ∀ (a : SetTheory.Game), SetTheory.Game.LF (b + a) (c + a)

theorem SetTheory.Game.add_lf_add_left {b : SetTheory.Game} {c : SetTheory.Game} : SetTheory.Game.LF b c → ∀ (a : SetTheory.Game), SetTheory.Game.LF (a + b) (a + c)

instance SetTheory.Game.orderedAddCommGroup : OrderedAddCommGroup SetTheory.Game

Equations

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

@[simp]

theorem SetTheory.PGame.quot_neg (a : SetTheory.PGame) : ⟦-a⟧ = -⟦a⟧

@[simp]

theorem SetTheory.PGame.quot_add (a : SetTheory.PGame) (b : SetTheory.PGame) : ⟦a + b⟧ = ⟦a⟧ + ⟦b⟧

@[simp]

theorem SetTheory.PGame.quot_sub (a : SetTheory.PGame) (b : SetTheory.PGame) : ⟦a - b⟧ = ⟦a⟧ - ⟦b⟧

theorem SetTheory.PGame.quot_eq_of_mk'_quot_eq {x : SetTheory.PGame} {y : SetTheory.PGame} (L : SetTheory.PGame.LeftMoves x ≃ SetTheory.PGame.LeftMoves y) (R : SetTheory.PGame.RightMoves x ≃ SetTheory.PGame.RightMoves y) (hl : ∀ (i : SetTheory.PGame.LeftMoves x), ⟦SetTheory.PGame.moveLeft x i⟧ = ⟦SetTheory.PGame.moveLeft y (L i)⟧) (hr : ∀ (j : SetTheory.PGame.RightMoves x), ⟦SetTheory.PGame.moveRight x j⟧ = ⟦SetTheory.PGame.moveRight y (R j)⟧) : ⟦x⟧ = ⟦y⟧

Multiplicative operations can be defined at the level of pre-games, but to prove their properties we need to use the abelian group structure of games. Hence we define them here.

instance SetTheory.PGame.instMulPGame : Mul SetTheory.PGame

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

Equations

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

theorem SetTheory.PGame.leftMoves_mul (x : SetTheory.PGame) (y : SetTheory.PGame) : SetTheory.PGame.LeftMoves (x * y) = (SetTheory.PGame.LeftMoves x × SetTheory.PGame.LeftMoves y ⊕ SetTheory.PGame.RightMoves x × SetTheory.PGame.RightMoves y)

theorem SetTheory.PGame.rightMoves_mul (x : SetTheory.PGame) (y : SetTheory.PGame) : SetTheory.PGame.RightMoves (x * y) = (SetTheory.PGame.LeftMoves x × SetTheory.PGame.RightMoves y ⊕ SetTheory.PGame.RightMoves x × SetTheory.PGame.LeftMoves y)

def SetTheory.PGame.toLeftMovesMul {x : SetTheory.PGame} {y : SetTheory.PGame} : SetTheory.PGame.LeftMoves x × SetTheory.PGame.LeftMoves y ⊕ SetTheory.PGame.RightMoves x × SetTheory.PGame.RightMoves y ≃ SetTheory.PGame.LeftMoves (x * y)

Turns two left or right moves for x and 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

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

def SetTheory.PGame.toRightMovesMul {x : SetTheory.PGame} {y : SetTheory.PGame} : SetTheory.PGame.LeftMoves x × SetTheory.PGame.RightMoves y ⊕ SetTheory.PGame.RightMoves x × SetTheory.PGame.LeftMoves y ≃ SetTheory.PGame.RightMoves (x * y)

Turns a left and a right move for x and 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

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

@[simp]

theorem SetTheory.PGame.mk_mul_moveLeft_inl {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame} {i : xl} {j : yl} : SetTheory.PGame.moveLeft (SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR) (Sum.inl (i, j)) = xL i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yL j - xL i * yL j

@[simp]

theorem SetTheory.PGame.mul_moveLeft_inl {x : SetTheory.PGame} {y : SetTheory.PGame} {i : SetTheory.PGame.LeftMoves x} {j : SetTheory.PGame.LeftMoves y} : SetTheory.PGame.moveLeft (x * y) (SetTheory.PGame.toLeftMovesMul (Sum.inl (i, j))) = SetTheory.PGame.moveLeft x i * y + x * SetTheory.PGame.moveLeft y j - SetTheory.PGame.moveLeft x i * SetTheory.PGame.moveLeft y j

@[simp]

theorem SetTheory.PGame.mk_mul_moveLeft_inr {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame} {i : xr} {j : yr} : SetTheory.PGame.moveLeft (SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR) (Sum.inr (i, j)) = xR i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yR j - xR i * yR j

@[simp]

theorem SetTheory.PGame.mul_moveLeft_inr {x : SetTheory.PGame} {y : SetTheory.PGame} {i : SetTheory.PGame.RightMoves x} {j : SetTheory.PGame.RightMoves y} : SetTheory.PGame.moveLeft (x * y) (SetTheory.PGame.toLeftMovesMul (Sum.inr (i, j))) = SetTheory.PGame.moveRight x i * y + x * SetTheory.PGame.moveRight y j - SetTheory.PGame.moveRight x i * SetTheory.PGame.moveRight y j

@[simp]

theorem SetTheory.PGame.mk_mul_moveRight_inl {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame} {i : xl} {j : yr} : SetTheory.PGame.moveRight (SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR) (Sum.inl (i, j)) = xL i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yR j - xL i * yR j

@[simp]

theorem SetTheory.PGame.mul_moveRight_inl {x : SetTheory.PGame} {y : SetTheory.PGame} {i : SetTheory.PGame.LeftMoves x} {j : SetTheory.PGame.RightMoves y} : SetTheory.PGame.moveRight (x * y) (SetTheory.PGame.toRightMovesMul (Sum.inl (i, j))) = SetTheory.PGame.moveLeft x i * y + x * SetTheory.PGame.moveRight y j - SetTheory.PGame.moveLeft x i * SetTheory.PGame.moveRight y j

@[simp]

theorem SetTheory.PGame.mk_mul_moveRight_inr {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame} {i : xr} {j : yl} : SetTheory.PGame.moveRight (SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR) (Sum.inr (i, j)) = xR i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yL j - xR i * yL j

@[simp]

theorem SetTheory.PGame.mul_moveRight_inr {x : SetTheory.PGame} {y : SetTheory.PGame} {i : SetTheory.PGame.RightMoves x} {j : SetTheory.PGame.LeftMoves y} : SetTheory.PGame.moveRight (x * y) (SetTheory.PGame.toRightMovesMul (Sum.inr (i, j))) = SetTheory.PGame.moveRight x i * y + x * SetTheory.PGame.moveLeft y j - SetTheory.PGame.moveRight x i * SetTheory.PGame.moveLeft y j

theorem SetTheory.PGame.neg_mk_mul_moveLeft_inl {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame} {i : xl} {j : yr} : SetTheory.PGame.moveLeft (-(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR)) (Sum.inl (i, j)) = -(xL i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yR j - xL i * yR j)

theorem SetTheory.PGame.neg_mk_mul_moveLeft_inr {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame} {i : xr} {j : yl} : SetTheory.PGame.moveLeft (-(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR)) (Sum.inr (i, j)) = -(xR i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yL j - xR i * yL j)

theorem SetTheory.PGame.neg_mk_mul_moveRight_inl {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame} {i : xl} {j : yl} : SetTheory.PGame.moveRight (-(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR)) (Sum.inl (i, j)) = -(xL i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yL j - xL i * yL j)

theorem SetTheory.PGame.neg_mk_mul_moveRight_inr {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xl → SetTheory.PGame} {xR : xr → SetTheory.PGame} {yL : yl → SetTheory.PGame} {yR : yr → SetTheory.PGame} {i : xr} {j : yr} : SetTheory.PGame.moveRight (-(SetTheory.PGame.mk xl xr xL xR * SetTheory.PGame.mk yl yr yL yR)) (Sum.inr (i, j)) = -(xR i * SetTheory.PGame.mk yl yr yL yR + SetTheory.PGame.mk xl xr xL xR * yR j - xR i * yR j)

theorem SetTheory.PGame.leftMoves_mul_cases {x : SetTheory.PGame} {y : SetTheory.PGame} (k : SetTheory.PGame.LeftMoves (x * y)) {P : SetTheory.PGame.LeftMoves (x * y) → Prop} (hl : ∀ (ix : SetTheory.PGame.LeftMoves x) (iy : SetTheory.PGame.LeftMoves y), P (SetTheory.PGame.toLeftMovesMul (Sum.inl (ix, iy)))) (hr : ∀ (jx : SetTheory.PGame.RightMoves x) (jy : SetTheory.PGame.RightMoves y), P (SetTheory.PGame.toLeftMovesMul (Sum.inr (jx, jy)))) : P k

theorem SetTheory.PGame.rightMoves_mul_cases {x : SetTheory.PGame} {y : SetTheory.PGame} (k : SetTheory.PGame.RightMoves (x * y)) {P : SetTheory.PGame.RightMoves (x * y) → Prop} (hl : ∀ (ix : SetTheory.PGame.LeftMoves x) (jy : SetTheory.PGame.RightMoves y), P (SetTheory.PGame.toRightMovesMul (Sum.inl (ix, jy)))) (hr : ∀ (jx : SetTheory.PGame.RightMoves x) (iy : SetTheory.PGame.LeftMoves y), P (SetTheory.PGame.toRightMovesMul (Sum.inr (jx, iy)))) : P k

def SetTheory.PGame.mulCommRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) : SetTheory.PGame.Relabelling (x * y) (y * x)

x * y and y * x have the same moves.

Equations

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

theorem SetTheory.PGame.quot_mul_comm (x : SetTheory.PGame) (y : SetTheory.PGame) : ⟦x * y⟧ = ⟦y * x⟧

theorem SetTheory.PGame.mul_comm_equiv (x : SetTheory.PGame) (y : SetTheory.PGame) : x * y ≈ y * x

x * y is equivalent to y * x.

instance SetTheory.PGame.isEmpty_mul_zero_leftMoves (x : SetTheory.PGame) : IsEmpty (SetTheory.PGame.LeftMoves (x * 0))

Equations

• (_ : IsEmpty (SetTheory.PGame.LeftMoves (x * 0))) = (_ : IsEmpty (SetTheory.PGame.LeftMoves (x * 0)))

instance SetTheory.PGame.isEmpty_mul_zero_rightMoves (x : SetTheory.PGame) : IsEmpty (SetTheory.PGame.RightMoves (x * 0))

Equations

• (_ : IsEmpty (SetTheory.PGame.RightMoves (x * 0))) = (_ : IsEmpty (SetTheory.PGame.RightMoves (x * 0)))

instance SetTheory.PGame.isEmpty_zero_mul_leftMoves (x : SetTheory.PGame) : IsEmpty (SetTheory.PGame.LeftMoves (0 * x))

Equations

• (_ : IsEmpty (SetTheory.PGame.LeftMoves (0 * x))) = (_ : IsEmpty (SetTheory.PGame.LeftMoves (0 * x)))

instance SetTheory.PGame.isEmpty_zero_mul_rightMoves (x : SetTheory.PGame) : IsEmpty (SetTheory.PGame.RightMoves (0 * x))

Equations

• (_ : IsEmpty (SetTheory.PGame.RightMoves (0 * x))) = (_ : IsEmpty (SetTheory.PGame.RightMoves (0 * x)))

def SetTheory.PGame.mulZeroRelabelling (x : SetTheory.PGame) : SetTheory.PGame.Relabelling (x * 0) 0

x * 0 has exactly the same moves as 0.

Equations

• SetTheory.PGame.mulZeroRelabelling x = SetTheory.PGame.Relabelling.isEmpty (x * 0)

theorem SetTheory.PGame.mul_zero_equiv (x : SetTheory.PGame) : x * 0 ≈ 0

x * 0 is equivalent to 0.

@[simp]

theorem SetTheory.PGame.quot_mul_zero (x : SetTheory.PGame) : ⟦x * 0⟧ = ⟦0⟧

def SetTheory.PGame.zeroMulRelabelling (x : SetTheory.PGame) : SetTheory.PGame.Relabelling (0 * x) 0

0 * x has exactly the same moves as 0.

Equations

• SetTheory.PGame.zeroMulRelabelling x = SetTheory.PGame.Relabelling.isEmpty (0 * x)

theorem SetTheory.PGame.zero_mul_equiv (x : SetTheory.PGame) : 0 * x ≈ 0

0 * x is equivalent to 0.

@[simp]

theorem SetTheory.PGame.quot_zero_mul (x : SetTheory.PGame) : ⟦0 * x⟧ = ⟦0⟧

def SetTheory.PGame.negMulRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) : SetTheory.PGame.Relabelling (-x * y) (-(x * y))

-x * y and -(x * y) have the same moves.

@[simp]

theorem SetTheory.PGame.quot_neg_mul (x : SetTheory.PGame) (y : SetTheory.PGame) : ⟦-x * y⟧ = -⟦x * y⟧

def SetTheory.PGame.mulNegRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) : SetTheory.PGame.Relabelling (x * -y) (-(x * y))

x * -y and -(x * y) have the same moves.

Equations

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

@[simp]

theorem SetTheory.PGame.quot_mul_neg (x : SetTheory.PGame) (y : SetTheory.PGame) : ⟦x * -y⟧ = -⟦x * y⟧

@[simp]

theorem SetTheory.PGame.quot_left_distrib (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) : ⟦x * (y + z)⟧ = ⟦x * y⟧ + ⟦x * z⟧

theorem SetTheory.PGame.left_distrib_equiv (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) : x * (y + z) ≈ x * y + x * z

x * (y + z) is equivalent to x * y + x * z.

@[simp]

theorem SetTheory.PGame.quot_left_distrib_sub (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) : ⟦x * (y - z)⟧ = ⟦x * y⟧ - ⟦x * z⟧

@[simp]

theorem SetTheory.PGame.quot_right_distrib (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) : ⟦(x + y) * z⟧ = ⟦x * z⟧ + ⟦y * z⟧

theorem SetTheory.PGame.right_distrib_equiv (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) : (x + y) * z ≈ x * z + y * z

(x + y) * z is equivalent to x * z + y * z.

@[simp]

theorem SetTheory.PGame.quot_right_distrib_sub (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) : ⟦(y - z) * x⟧ = ⟦y * x⟧ - ⟦z * x⟧

def SetTheory.PGame.mulOneRelabelling (x : SetTheory.PGame) : SetTheory.PGame.Relabelling (x * 1) x

x * 1 has the same moves as x.

Equations

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

@[simp]

theorem SetTheory.PGame.quot_mul_one (x : SetTheory.PGame) : ⟦x * 1⟧ = ⟦x⟧

theorem SetTheory.PGame.mul_one_equiv (x : SetTheory.PGame) : x * 1 ≈ x

x * 1 is equivalent to x.

def SetTheory.PGame.oneMulRelabelling (x : SetTheory.PGame) : SetTheory.PGame.Relabelling (1 * x) x

1 * x has the same moves as x.

Equations

• SetTheory.PGame.oneMulRelabelling x = SetTheory.PGame.Relabelling.trans (SetTheory.PGame.mulCommRelabelling 1 x) (SetTheory.PGame.mulOneRelabelling x)

@[simp]

theorem SetTheory.PGame.quot_one_mul (x : SetTheory.PGame) : ⟦1 * x⟧ = ⟦x⟧

theorem SetTheory.PGame.one_mul_equiv (x : SetTheory.PGame) : 1 * x ≈ x

1 * x is equivalent to x.

theorem SetTheory.PGame.quot_mul_assoc (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) : ⟦x * y * z⟧ = ⟦x * (y * z)⟧

theorem SetTheory.PGame.mul_assoc_equiv (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) : x * y * z ≈ x * (y * z)

x * y * z is equivalent to x * (y * z).

inductive SetTheory.PGame.InvTy (l : Type u) (r : Type u) : Bool → Type u

Because the two halves of the definition of inv produce more elements on each side, we have to define the two families inductively. This is the indexing set for the function, and invVal is the function part.

• zero: {l r : Type u} → SetTheory.PGame.InvTy l r false
• left₁: {l r : Type u} → r → SetTheory.PGame.InvTy l r false → SetTheory.PGame.InvTy l r false
• left₂: {l r : Type u} → l → SetTheory.PGame.InvTy l r true → SetTheory.PGame.InvTy l r false
• right₁: {l r : Type u} → l → SetTheory.PGame.InvTy l r false → SetTheory.PGame.InvTy l r true
• right₂: {l r : Type u} → r → SetTheory.PGame.InvTy l r true → SetTheory.PGame.InvTy l r true

instance SetTheory.PGame.instIsEmptyInvTyTrue (l : Type u) (r : Type u) [IsEmpty l] [IsEmpty r] : IsEmpty (SetTheory.PGame.InvTy l r true)

Equations

• (_ : IsEmpty (SetTheory.PGame.InvTy l r true)) = (_ : IsEmpty (SetTheory.PGame.InvTy l r true))

instance SetTheory.PGame.InvTy.instInhabited (l : Type u) (r : Type u) : Inhabited (SetTheory.PGame.InvTy l r false)

Equations

• SetTheory.PGame.InvTy.instInhabited l r = { default := SetTheory.PGame.InvTy.zero }

instance SetTheory.PGame.uniqueInvTy (l : Type u) (r : Type u) [IsEmpty l] [IsEmpty r] : Unique (SetTheory.PGame.InvTy l r false)

Equations

• SetTheory.PGame.uniqueInvTy l r = let src := SetTheory.PGame.InvTy.instInhabited l r; { toInhabited := src, uniq := (_ : ∀ (a : SetTheory.PGame.InvTy l r false), a = default) }

def SetTheory.PGame.invVal {l : Type u_1} {r : Type u_1} (L : l → SetTheory.PGame) (R : r → SetTheory.PGame) (IHl : l → SetTheory.PGame) (IHr : r → SetTheory.PGame) {b : Bool} : SetTheory.PGame.InvTy l r b → SetTheory.PGame

Because the two halves of the definition of inv produce more elements of each side, we have to define the two families inductively. This is the function part, defined by recursion on InvTy.

Equations

• SetTheory.PGame.invVal L R IHl IHr SetTheory.PGame.InvTy.zero = 0
• SetTheory.PGame.invVal L R IHl IHr (SetTheory.PGame.InvTy.left₁ i j) = (1 + (R i - SetTheory.PGame.mk l r L R) * SetTheory.PGame.invVal L R IHl IHr j) * IHr i
• SetTheory.PGame.invVal L R IHl IHr (SetTheory.PGame.InvTy.left₂ i j) = (1 + (L i - SetTheory.PGame.mk l r L R) * SetTheory.PGame.invVal L R IHl IHr j) * IHl i
• SetTheory.PGame.invVal L R IHl IHr (SetTheory.PGame.InvTy.right₁ i j) = (1 + (L i - SetTheory.PGame.mk l r L R) * SetTheory.PGame.invVal L R IHl IHr j) * IHl i
• SetTheory.PGame.invVal L R IHl IHr (SetTheory.PGame.InvTy.right₂ i j) = (1 + (R i - SetTheory.PGame.mk l r L R) * SetTheory.PGame.invVal L R IHl IHr j) * IHr i

@[simp]

theorem SetTheory.PGame.invVal_isEmpty {l : Type u} {r : Type u} {b : Bool} (L : l → SetTheory.PGame) (R : r → SetTheory.PGame) (IHl : l → SetTheory.PGame) (IHr : r → SetTheory.PGame) (i : SetTheory.PGame.InvTy l r b) [IsEmpty l] [IsEmpty r] : SetTheory.PGame.invVal L R IHl IHr i = 0

def SetTheory.PGame.inv' : SetTheory.PGame → SetTheory.PGame

The inverse of a positive surreal number x = {L | R} is given by x⁻¹ = {0, (1 + (R - x) * x⁻¹L) * R, (1 + (L - x) * x⁻¹R) * L | (1 + (L - x) * x⁻¹L) * L, (1 + (R - x) * x⁻¹R) * R}. Because the two halves x⁻¹L, x⁻¹R of x⁻¹ are used in their own definition, the sets and elements are inductively generated.

Equations

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

theorem SetTheory.PGame.zero_lf_inv' (x : SetTheory.PGame) : SetTheory.PGame.LF 0 (SetTheory.PGame.inv' x)

def SetTheory.PGame.inv'Zero : SetTheory.PGame.Relabelling (SetTheory.PGame.inv' 0) 1

inv' 0 has exactly the same moves as 1.

Equations

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

theorem SetTheory.PGame.inv'_zero_equiv : SetTheory.PGame.inv' 0 ≈ 1

def SetTheory.PGame.inv'One : SetTheory.PGame.Relabelling (SetTheory.PGame.inv' 1) 1

inv' 1 has exactly the same moves as 1.

Equations

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

theorem SetTheory.PGame.inv'_one_equiv : SetTheory.PGame.inv' 1 ≈ 1

noncomputable instance SetTheory.PGame.instInvPGame : Inv SetTheory.PGame

The inverse of a pre-game in terms of the inverse on positive pre-games.

Equations

• SetTheory.PGame.instInvPGame = { inv := fun (x : SetTheory.PGame) => if x ≈ 0 then 0 else if 0 < x then SetTheory.PGame.inv' x else -SetTheory.PGame.inv' (-x) }

noncomputable instance SetTheory.PGame.instDivPGame : Div SetTheory.PGame

Equations

• SetTheory.PGame.instDivPGame = { div := fun (x y : SetTheory.PGame) => x * y⁻¹ }

theorem SetTheory.PGame.inv_eq_of_equiv_zero {x : SetTheory.PGame} (h : x ≈ 0) : x⁻¹ = 0

@[simp]

theorem SetTheory.PGame.inv_zero : 0⁻¹ = 0

theorem SetTheory.PGame.inv_eq_of_pos {x : SetTheory.PGame} (h : 0 < x) : x⁻¹ = SetTheory.PGame.inv' x

theorem SetTheory.PGame.inv_eq_of_lf_zero {x : SetTheory.PGame} (h : SetTheory.PGame.LF x 0) : x⁻¹ = -SetTheory.PGame.inv' (-x)

def SetTheory.PGame.invOne : SetTheory.PGame.Relabelling 1⁻¹ 1

1⁻¹ has exactly the same moves as 1.

Equations

• SetTheory.PGame.invOne = Eq.mpr SetTheory.PGame.invOne.proof_1 SetTheory.PGame.inv'One

theorem SetTheory.PGame.inv_one_equiv : 1⁻¹ ≈ 1