Algebraic structure on pregames

This file defines the operations necessary to make games into an additive commutative 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, the notion of a Relabelling of a game is used (defined in Mathlib/SetTheory/PGame/Basic.lean); for example, there is a relabelling between x + (y + z) and (x + y) + z.

Negation

def SetTheory.PGame.neg : PGame → PGame

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

Equations

• (SetTheory.PGame.mk l r L R).neg = SetTheory.PGame.mk r l (fun (i : r) => (R i).neg) fun (i : l) => (L i).neg

instance SetTheory.PGame.instNeg : Neg PGame

Equations

• SetTheory.PGame.instNeg = { neg := SetTheory.PGame.neg }

@[simp]

theorem SetTheory.PGame.neg_def {xl xr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} : -mk xl xr xL xR = mk xr xl (fun (x : xr) => -xR x) fun (x : xl) => -xL x

instance SetTheory.PGame.instInvolutiveNeg : InvolutiveNeg PGame

Equations

• SetTheory.PGame.instInvolutiveNeg = { toNeg := inferInstanceAs (Neg SetTheory.PGame), neg_neg := SetTheory.PGame.instInvolutiveNeg._proof_1 }

instance SetTheory.PGame.instNegZeroClass : NegZeroClass PGame

Equations

• SetTheory.PGame.instNegZeroClass = { toZero := inferInstanceAs (Zero SetTheory.PGame), toNeg := inferInstanceAs (Neg SetTheory.PGame), neg_zero := SetTheory.PGame.instNegZeroClass._proof_2 }

@[simp]

theorem SetTheory.PGame.neg_ofLists (L R : List PGame) : -ofLists L R = ofLists (List.map (fun (x : PGame) => -x) R) (List.map (fun (x : PGame) => -x) L)

theorem SetTheory.PGame.isOption_neg {x y : PGame} : x.IsOption (-y) ↔ (-x).IsOption y

@[simp]

theorem SetTheory.PGame.isOption_neg_neg {x y : PGame} : (-x).IsOption (-y) ↔ x.IsOption y

theorem SetTheory.PGame.leftMoves_neg (x : PGame) : (-x).LeftMoves = x.RightMoves

Use toLeftMovesNeg to cast between these two types.

theorem SetTheory.PGame.rightMoves_neg (x : PGame) : (-x).RightMoves = x.LeftMoves

Use toRightMovesNeg to cast between these two types.

def SetTheory.PGame.toLeftMovesNeg {x : 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 = Equiv.cast ⋯

def SetTheory.PGame.toRightMovesNeg {x : 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 = Equiv.cast ⋯

@[simp]

theorem SetTheory.PGame.moveLeft_neg {x : PGame} (i : (-x).LeftMoves) : (-x).moveLeft i = -x.moveRight (toLeftMovesNeg.symm i)

@[deprecated SetTheory.PGame.moveLeft_neg (since := "2024-10-30")]

theorem SetTheory.PGame.moveLeft_neg' {x : PGame} (i : (-x).LeftMoves) : (-x).moveLeft i = -x.moveRight (toLeftMovesNeg.symm i)

Alias of SetTheory.PGame.moveLeft_neg.

theorem SetTheory.PGame.moveLeft_neg_toLeftMovesNeg {x : PGame} (i : x.RightMoves) : (-x).moveLeft (toLeftMovesNeg i) = -x.moveRight i

@[simp]

theorem SetTheory.PGame.moveRight_neg {x : PGame} (i : (-x).RightMoves) : (-x).moveRight i = -x.moveLeft (toRightMovesNeg.symm i)

@[deprecated SetTheory.PGame.moveRight_neg (since := "2024-10-30")]

theorem SetTheory.PGame.moveRight_neg' {x : PGame} (i : (-x).RightMoves) : (-x).moveRight i = -x.moveLeft (toRightMovesNeg.symm i)

Alias of SetTheory.PGame.moveRight_neg.

theorem SetTheory.PGame.moveRight_neg_toRightMovesNeg {x : PGame} (i : x.LeftMoves) : (-x).moveRight (toRightMovesNeg i) = -x.moveLeft i

@[deprecated SetTheory.PGame.moveRight_neg (since := "2024-10-30")]

theorem SetTheory.PGame.moveLeft_neg_symm {x : PGame} (i : (-x).RightMoves) : x.moveLeft (toRightMovesNeg.symm i) = -(-x).moveRight i

@[deprecated SetTheory.PGame.moveRight_neg (since := "2024-10-30")]

theorem SetTheory.PGame.moveLeft_neg_symm' {x : PGame} (i : x.LeftMoves) : x.moveLeft i = -(-x).moveRight (toRightMovesNeg i)

@[deprecated SetTheory.PGame.moveLeft_neg (since := "2024-10-30")]

theorem SetTheory.PGame.moveRight_neg_symm {x : PGame} (i : (-x).LeftMoves) : x.moveRight (toLeftMovesNeg.symm i) = -(-x).moveLeft i

@[deprecated SetTheory.PGame.moveLeft_neg (since := "2024-10-30")]

theorem SetTheory.PGame.moveRight_neg_symm' {x : PGame} (i : x.RightMoves) : x.moveRight i = -(-x).moveLeft (toLeftMovesNeg i)

@[simp]

theorem SetTheory.PGame.forall_leftMoves_neg {x : PGame} {p : (-x).LeftMoves → Prop} : (∀ (i : (-x).LeftMoves), p i) ↔ ∀ (i : x.RightMoves), p (toLeftMovesNeg i)

@[simp]

theorem SetTheory.PGame.exists_leftMoves_neg {x : PGame} {p : (-x).LeftMoves → Prop} : (∃ (i : (-x).LeftMoves), p i) ↔ ∃ (i : x.RightMoves), p (toLeftMovesNeg i)

@[simp]

theorem SetTheory.PGame.forall_rightMoves_neg {x : PGame} {p : (-x).RightMoves → Prop} : (∀ (i : (-x).RightMoves), p i) ↔ ∀ (i : x.LeftMoves), p (toRightMovesNeg i)

@[simp]

theorem SetTheory.PGame.exists_rightMoves_neg {x : PGame} {p : (-x).RightMoves → Prop} : (∃ (i : (-x).RightMoves), p i) ↔ ∃ (i : x.LeftMoves), p (toRightMovesNeg i)

theorem SetTheory.PGame.leftMoves_neg_cases {x : PGame} (k : (-x).LeftMoves) {P : (-x).LeftMoves → Prop} (h : ∀ (i : x.RightMoves), P (toLeftMovesNeg i)) : P k

theorem SetTheory.PGame.rightMoves_neg_cases {x : PGame} (k : (-x).RightMoves) {P : (-x).RightMoves → Prop} (h : ∀ (i : x.LeftMoves), P (toRightMovesNeg i)) : P k

theorem SetTheory.PGame.Identical.neg {x₁ x₂ : PGame} : x₁.Identical x₂ → (-x₁).Identical (-x₂)

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

theorem SetTheory.PGame.Identical.of_neg {x₁ x₂ : PGame} : (-x₁).Identical (-x₂) → x₁.Identical x₂

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

theorem SetTheory.PGame.memₗ_neg_iff {x y : PGame} : x.memₗ (-y) ↔ ∃ (z : PGame), z.memᵣ y ∧ x.Identical (-z)

theorem SetTheory.PGame.memᵣ_neg_iff {x y : PGame} : x.memᵣ (-y) ↔ ∃ (z : PGame), z.memₗ y ∧ x.Identical (-z)

def SetTheory.PGame.Relabelling.negCongr {x y : 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.

@[simp]

theorem SetTheory.PGame.neg_le_neg_iff {x y : PGame} : -y ≤ -x ↔ x ≤ y

@[simp]

theorem SetTheory.PGame.neg_lf_neg_iff {x y : PGame} : (-y).LF (-x) ↔ x.LF y

@[simp]

theorem SetTheory.PGame.neg_lt_neg_iff {x y : PGame} : -y < -x ↔ x < y

@[simp]

theorem SetTheory.PGame.neg_identical_neg {x y : PGame} : (-x).Identical (-y) ↔ x.Identical y

@[simp]

theorem SetTheory.PGame.neg_equiv_neg_iff {x y : PGame} : -x ≈ -y ↔ x ≈ y

@[simp]

theorem SetTheory.PGame.neg_fuzzy_neg_iff {x y : PGame} : (-x).Fuzzy (-y) ↔ x.Fuzzy y

theorem SetTheory.PGame.neg_le_iff {x y : PGame} : -y ≤ x ↔ -x ≤ y

theorem SetTheory.PGame.neg_lf_iff {x y : PGame} : (-y).LF x ↔ (-x).LF y

theorem SetTheory.PGame.neg_lt_iff {x y : PGame} : -y < x ↔ -x < y

theorem SetTheory.PGame.neg_equiv_iff {x y : PGame} : -x ≈ y ↔ x ≈ -y

theorem SetTheory.PGame.neg_fuzzy_iff {x y : PGame} : (-x).Fuzzy y ↔ x.Fuzzy (-y)

theorem SetTheory.PGame.le_neg_iff {x y : PGame} : y ≤ -x ↔ x ≤ -y

theorem SetTheory.PGame.lf_neg_iff {x y : PGame} : y.LF (-x) ↔ x.LF (-y)

theorem SetTheory.PGame.lt_neg_iff {x y : PGame} : y < -x ↔ x < -y

@[simp]

theorem SetTheory.PGame.neg_le_zero_iff {x : PGame} : -x ≤ 0 ↔ 0 ≤ x

@[simp]

theorem SetTheory.PGame.zero_le_neg_iff {x : PGame} : 0 ≤ -x ↔ x ≤ 0

@[simp]

theorem SetTheory.PGame.neg_lf_zero_iff {x : PGame} : (-x).LF 0 ↔ LF 0 x

@[simp]

theorem SetTheory.PGame.zero_lf_neg_iff {x : PGame} : LF 0 (-x) ↔ x.LF 0

@[simp]

theorem SetTheory.PGame.neg_lt_zero_iff {x : PGame} : -x < 0 ↔ 0 < x

@[simp]

theorem SetTheory.PGame.zero_lt_neg_iff {x : PGame} : 0 < -x ↔ x < 0

@[simp]

theorem SetTheory.PGame.neg_equiv_zero_iff {x : PGame} : -x ≈ 0 ↔ x ≈ 0

@[simp]

theorem SetTheory.PGame.neg_fuzzy_zero_iff {x : PGame} : (-x).Fuzzy 0 ↔ x.Fuzzy 0

@[simp]

theorem SetTheory.PGame.zero_equiv_neg_iff {x : PGame} : 0 ≈ -x ↔ 0 ≈ x

@[simp]

theorem SetTheory.PGame.zero_fuzzy_neg_iff {x : PGame} : Fuzzy 0 (-x) ↔ Fuzzy 0 x

Addition and subtraction

instance SetTheory.PGame.instAdd : Add PGame

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.

theorem SetTheory.PGame.mk_add_moveLeft {xl xr yl yr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} {yL : yl → PGame} {yR : yr → PGame} {i : (mk xl xr xL xR + mk yl yr yL yR).LeftMoves} : (mk xl xr xL xR + mk yl yr yL yR).moveLeft i = Sum.rec (fun (x : xl) => xL x + mk yl yr yL yR) (fun (x : yl) => mk xl xr xL xR + yL x) i

theorem SetTheory.PGame.mk_add_moveRight {xl xr yl yr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} {yL : yl → PGame} {yR : yr → PGame} {i : (mk xl xr xL xR + mk yl yr yL yR).RightMoves} : (mk xl xr xL xR + mk yl yr yL yR).moveRight i = Sum.rec (fun (x : xr) => xR x + mk yl yr yL yR) (fun (x : yr) => mk xl xr xL xR + yR x) i

instance SetTheory.PGame.instNatCast : NatCast PGame

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

Note that this is not the usual recursive definition n = {0, 1, … | }. For instance, 2 = 0 + 1 + 1 = {0 + 0 + 1, 0 + 1 + 0 | } does not contain any left option equivalent to 0. For an implementation of said definition, see Ordinal.toPGame. For the proof that these games are equivalent, see Ordinal.toPGame_natCast.

Equations

• SetTheory.PGame.instNatCast = { natCast := Nat.unaryCast }

@[simp]

theorem SetTheory.PGame.nat_succ (n : ℕ) : ↑(n + 1) = ↑n + 1

instance SetTheory.PGame.isEmpty_leftMoves_add (x y : PGame) [IsEmpty x.LeftMoves] [IsEmpty y.LeftMoves] : IsEmpty (x + y).LeftMoves

instance SetTheory.PGame.isEmpty_rightMoves_add (x y : PGame) [IsEmpty x.RightMoves] [IsEmpty y.RightMoves] : IsEmpty (x + y).RightMoves

@[irreducible]

def SetTheory.PGame.addZeroRelabelling (x : PGame) : (x + 0).Relabelling x

x + 0 has exactly the same moves as x.

Equations

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

theorem SetTheory.PGame.add_zero_equiv (x : PGame) : x + 0 ≈ x

x + 0 is equivalent to x.

def SetTheory.PGame.zeroAddRelabelling (x : PGame) : (0 + x).Relabelling x

0 + x has exactly the same moves as x.

Equations

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

theorem SetTheory.PGame.zero_add_equiv (x : PGame) : 0 + x ≈ x

0 + x is equivalent to x.

theorem SetTheory.PGame.leftMoves_add (x y : PGame) : (x + y).LeftMoves = (x.LeftMoves ⊕ y.LeftMoves)

Use toLeftMovesAdd to cast between these two types.

theorem SetTheory.PGame.rightMoves_add (x y : PGame) : (x + y).RightMoves = (x.RightMoves ⊕ y.RightMoves)

Use toRightMovesAdd to cast between these two types.

def SetTheory.PGame.toLeftMovesAdd {x y : 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

• SetTheory.PGame.toLeftMovesAdd = Equiv.cast ⋯

def SetTheory.PGame.toRightMovesAdd {x y : 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

• SetTheory.PGame.toRightMovesAdd = Equiv.cast ⋯

@[simp]

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

@[simp]

theorem SetTheory.PGame.add_moveLeft_inl {x : PGame} (y : PGame) (i : x.LeftMoves) : (x + y).moveLeft (toLeftMovesAdd (Sum.inl i)) = x.moveLeft i + y

@[simp]

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

@[simp]

theorem SetTheory.PGame.add_moveRight_inl {x : PGame} (y : PGame) (i : x.RightMoves) : (x + y).moveRight (toRightMovesAdd (Sum.inl i)) = x.moveRight i + y

@[simp]

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

@[simp]

theorem SetTheory.PGame.add_moveLeft_inr (x : PGame) {y : PGame} (i : y.LeftMoves) : (x + y).moveLeft (toLeftMovesAdd (Sum.inr i)) = x + y.moveLeft i

@[simp]

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

@[simp]

theorem SetTheory.PGame.add_moveRight_inr (x : PGame) {y : PGame} (i : y.RightMoves) : (x + y).moveRight (toRightMovesAdd (Sum.inr i)) = x + y.moveRight i

theorem SetTheory.PGame.leftMoves_add_cases {x y : PGame} (k : (x + y).LeftMoves) {P : (x + y).LeftMoves → Prop} (hl : ∀ (i : x.LeftMoves), P (toLeftMovesAdd (Sum.inl i))) (hr : ∀ (i : y.LeftMoves), P (toLeftMovesAdd (Sum.inr i))) : P k

Case on possible left moves of x + y.

theorem SetTheory.PGame.rightMoves_add_cases {x y : PGame} (k : (x + y).RightMoves) {P : (x + y).RightMoves → Prop} (hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))) (hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))) : P k

Case on possible right moves of x + y.

instance SetTheory.PGame.isEmpty_nat_rightMoves (n : ℕ) : IsEmpty (↑n).RightMoves

@[irreducible]

theorem SetTheory.PGame.add_comm (x y : PGame) : (x + y).Identical (y + x)

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

@[irreducible]

theorem SetTheory.PGame.add_assoc (x y z : PGame) : (x + y + z).Identical (x + (y + z))

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

theorem SetTheory.PGame.add_zero (x : PGame) : (x + 0).Identical x

x + 0 has exactly the same moves as x.

theorem SetTheory.PGame.zero_add (x : PGame) : (0 + x).Identical x

0 + x has exactly the same moves as x.

@[irreducible]

theorem SetTheory.PGame.neg_add (x y : PGame) : -(x + y) = -x + -y

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

theorem SetTheory.PGame.neg_add_rev (x y : PGame) : (-(x + y)).Identical (-y + -x)

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

theorem SetTheory.PGame.identical_zero_iff (x : PGame) : x.Identical 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves

theorem SetTheory.PGame.identical_zero (x : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] : x.Identical 0

Any game without left or right moves is identical to 0.

theorem SetTheory.PGame.add_eq_zero {x y : PGame} : (x + y).Identical 0 ↔ x.Identical 0 ∧ y.Identical 0

@[irreducible]

theorem SetTheory.PGame.Identical.add_right {x₁ x₂ y : PGame} : x₁.Identical x₂ → (x₁ + y).Identical (x₂ + y)

theorem SetTheory.PGame.Identical.add_left {x y₁ y₂ : PGame} (hy : y₁.Identical y₂) : (x + y₁).Identical (x + y₂)

theorem SetTheory.PGame.Identical.add {x₁ x₂ y₁ y₂ : PGame} (hx : x₁.Identical x₂) (hy : y₁.Identical y₂) : (x₁ + y₁).Identical (x₂ + y₂)

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.

theorem SetTheory.PGame.memₗ_add_iff {x y₁ y₂ : PGame} : x.memₗ (y₁ + y₂) ↔ (∃ (z : PGame), z.memₗ y₁ ∧ x.Identical (z + y₂)) ∨ ∃ (z : PGame), z.memₗ y₂ ∧ x.Identical (y₁ + z)

theorem SetTheory.PGame.memᵣ_add_iff {x y₁ y₂ : PGame} : x.memᵣ (y₁ + y₂) ↔ (∃ (z : PGame), z.memᵣ y₁ ∧ x.Identical (z + y₂)) ∨ ∃ (z : PGame), z.memᵣ y₂ ∧ x.Identical (y₁ + z)

@[irreducible]

def SetTheory.PGame.Relabelling.addCongr {w x y z : PGame} : w.Relabelling x → 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

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

instance SetTheory.PGame.instSub : Sub PGame

Equations

• SetTheory.PGame.instSub = { sub := fun (x y : SetTheory.PGame) => x + -y }

@[simp]

theorem SetTheory.PGame.sub_zero_eq_add_zero (x : PGame) : x - 0 = x + 0

theorem SetTheory.PGame.sub_zero (x : PGame) : (x - 0).Identical x

theorem SetTheory.PGame.neg_sub' (x y : PGame) : -(x - y) = -x - -y

This lemma is named to match neg_sub'.

theorem SetTheory.PGame.Identical.sub {x₁ x₂ y₁ y₂ : PGame} (hx : x₁.Identical x₂) (hy : y₁.Identical y₂) : (x₁ - y₁).Identical (x₂ - y₂)

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.

def SetTheory.PGame.Relabelling.subCongr {w x y z : 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

@[irreducible]

def SetTheory.PGame.negAddRelabelling (x y : 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.

theorem SetTheory.PGame.neg_add_le {x y : PGame} : -(x + y) ≤ -x + -y

@[irreducible]

def SetTheory.PGame.addCommRelabelling (x y : 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.

theorem SetTheory.PGame.add_comm_le {x y : PGame} : x + y ≤ y + x

theorem SetTheory.PGame.add_comm_equiv {x y : PGame} : x + y ≈ y + x

@[irreducible]

def SetTheory.PGame.addAssocRelabelling (x y z : 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.

theorem SetTheory.PGame.add_assoc_equiv {x y z : PGame} : x + y + z ≈ x + (y + z)

theorem SetTheory.PGame.neg_add_cancel_le_zero (x : PGame) : -x + x ≤ 0

theorem SetTheory.PGame.zero_le_neg_add_cancel (x : PGame) : 0 ≤ -x + x

theorem SetTheory.PGame.neg_add_cancel_equiv (x : PGame) : -x + x ≈ 0

theorem SetTheory.PGame.add_neg_cancel_le_zero (x : PGame) : x + -x ≤ 0

theorem SetTheory.PGame.zero_le_add_neg_cancel (x : PGame) : 0 ≤ x + -x

theorem SetTheory.PGame.add_neg_cancel_equiv (x : PGame) : x + -x ≈ 0

theorem SetTheory.PGame.sub_self_equiv (x : PGame) : x - x ≈ 0

instance SetTheory.PGame.addRightMono : AddRightMono PGame

instance SetTheory.PGame.addLeftMono : AddLeftMono PGame

theorem SetTheory.PGame.add_lf_add_right {y z : PGame} (h : y.LF z) (x : PGame) : (y + x).LF (z + x)

theorem SetTheory.PGame.add_lf_add_left {y z : PGame} (h : y.LF z) (x : PGame) : (x + y).LF (x + z)

instance SetTheory.PGame.addRightStrictMono : AddRightStrictMono PGame

instance SetTheory.PGame.addLeftStrictMono : AddLeftStrictMono PGame

theorem SetTheory.PGame.add_lf_add_of_lf_of_le {w x y z : PGame} (hwx : w.LF x) (hyz : y ≤ z) : (w + y).LF (x + z)

theorem SetTheory.PGame.add_lf_add_of_le_of_lf {w x y z : PGame} (hwx : w ≤ x) (hyz : y.LF z) : (w + y).LF (x + z)

theorem SetTheory.PGame.add_congr {w x y z : PGame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w + y ≈ x + z

theorem SetTheory.PGame.add_congr_left {x y z : PGame} (h : x ≈ y) : x + z ≈ y + z

theorem SetTheory.PGame.add_congr_right {x y z : PGame} : y ≈ z → x + y ≈ x + z

theorem SetTheory.PGame.sub_congr {w x y z : PGame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w - y ≈ x - z

theorem SetTheory.PGame.sub_congr_left {x y z : PGame} (h : x ≈ y) : x - z ≈ y - z

theorem SetTheory.PGame.sub_congr_right {x y z : PGame} : y ≈ z → x - y ≈ x - z

theorem SetTheory.PGame.le_iff_sub_nonneg {x y : PGame} : x ≤ y ↔ 0 ≤ y - x

theorem SetTheory.PGame.lf_iff_sub_zero_lf {x y : PGame} : x.LF y ↔ LF 0 (y - x)

theorem SetTheory.PGame.lt_iff_sub_pos {x y : PGame} : x < y ↔ 0 < y - x

Interaction of option insertion with negation

theorem SetTheory.PGame.neg_insertRight_neg (x x' : PGame) : (-x).insertRight (-x') = -x.insertLeft x'

theorem SetTheory.PGame.neg_insertLeft_neg (x x' : PGame) : (-x).insertLeft (-x') = -x.insertRight x'

Special pre-games

def SetTheory.PGame.star : PGame

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

Equations

• SetTheory.PGame.star = SetTheory.PGame.mk PUnit.{?u.1 + 1} PUnit.{?u.1 + 1} (fun (x : PUnit.{?u.1 + 1}) => 0) fun (x : PUnit.{?u.1 + 1}) => 0

@[simp]

theorem SetTheory.PGame.star_leftMoves : star.LeftMoves = PUnit.{u_1 + 1}

@[simp]

theorem SetTheory.PGame.star_rightMoves : star.RightMoves = PUnit.{u_1 + 1}

@[simp]

theorem SetTheory.PGame.star_moveLeft (x : star.LeftMoves) : star.moveLeft x = 0

@[simp]

theorem SetTheory.PGame.star_moveRight (x : star.RightMoves) : star.moveRight x = 0

instance SetTheory.PGame.uniqueStarLeftMoves : Unique star.LeftMoves

Equations

• SetTheory.PGame.uniqueStarLeftMoves = PUnit.instUnique

instance SetTheory.PGame.uniqueStarRightMoves : Unique star.RightMoves

Equations

• SetTheory.PGame.uniqueStarRightMoves = PUnit.instUnique

theorem SetTheory.PGame.zero_lf_star : LF 0 star

theorem SetTheory.PGame.star_lf_zero : star.LF 0

theorem SetTheory.PGame.star_fuzzy_zero : star.Fuzzy 0

@[simp]

theorem SetTheory.PGame.neg_star : -star = star

@[simp]

theorem SetTheory.PGame.zero_lt_one : 0 < 1

def SetTheory.PGame.up : PGame

The pre-game up

Equations

• SetTheory.PGame.up = SetTheory.PGame.mk PUnit.{?u.1 + 1} PUnit.{?u.1 + 1} (fun (x : PUnit.{?u.1 + 1}) => 0) fun (x : PUnit.{?u.1 + 1}) => SetTheory.PGame.star

@[simp]

theorem SetTheory.PGame.up_leftMoves : up.LeftMoves = PUnit.{u_1 + 1}

@[simp]

theorem SetTheory.PGame.up_rightMoves : up.RightMoves = PUnit.{u_1 + 1}

@[simp]

theorem SetTheory.PGame.up_moveLeft (x : up.LeftMoves) : up.moveLeft x = 0

@[simp]

theorem SetTheory.PGame.up_moveRight (x : up.RightMoves) : up.moveRight x = star

@[simp]

theorem SetTheory.PGame.up_neg : 0 < up

theorem SetTheory.PGame.star_fuzzy_up : star.Fuzzy up

def SetTheory.PGame.down : PGame

The pre-game down

Equations

• SetTheory.PGame.down = SetTheory.PGame.mk PUnit.{?u.1 + 1} PUnit.{?u.1 + 1} (fun (x : PUnit.{?u.1 + 1}) => SetTheory.PGame.star) fun (x : PUnit.{?u.1 + 1}) => 0

@[simp]

theorem SetTheory.PGame.down_leftMoves : down.LeftMoves = PUnit.{u_1 + 1}

@[simp]

theorem SetTheory.PGame.down_rightMoves : down.RightMoves = PUnit.{u_1 + 1}

@[simp]

theorem SetTheory.PGame.down_moveLeft (x : down.LeftMoves) : down.moveLeft x = star

@[simp]

theorem SetTheory.PGame.down_moveRight (x : down.RightMoves) : down.moveRight x = 0

@[simp]

theorem SetTheory.PGame.down_neg : down < 0

@[simp]

theorem SetTheory.PGame.neg_down : -down = up

@[simp]

theorem SetTheory.PGame.neg_up : -up = down

theorem SetTheory.PGame.star_fuzzy_down : star.Fuzzy down

instance SetTheory.PGame.instZeroLEOneClass : ZeroLEOneClass PGame

@[simp]

theorem SetTheory.PGame.zero_lf_one : LF 0 1