Documentation

Mathlib.SetTheory.PGame.Algebra

Algebraic structure on pregames #

This file defines the operations necessary to make games into an additive commutative group. Addition is defined for $x = {x L | x R}$ and $y = {y L | y R}$ by $x + y = {x L + y, x + y L | x R + y, x + y R}$ . Negation is defined by ${x L | x R} = {- x R | - x L}$ .

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 :

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 :

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 :

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] :

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 :

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 :

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 :

theorem SetTheory.PGame.star_lf_zero :

theorem SetTheory.PGame.star_fuzzy_zero :

@[simp]

theorem SetTheory.PGame.neg_star :

@[simp]

theorem SetTheory.PGame.zero_lt_one :

0 < 1

def SetTheory.PGame.up :

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 :

def SetTheory.PGame.down :

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 :

@[simp]

theorem SetTheory.PGame.neg_down :

@[simp]

theorem SetTheory.PGame.neg_up :

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