set_theory.game.basic - mathlib3 docs

source

@[protected, instance]

def pgame.setoid :

setoid pgame

Equations

pgame.setoid = {r := pgame.equiv, iseqv := pgame.setoid._proof_1}

source

@[reducible]

def 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.

source

@[protected, instance]

def game.add_comm_group_with_one :

add_comm_group_with_one game

Equations

game.add_comm_group_with_one = {add := quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1, add_assoc := game.add_comm_group_with_one._proof_2, zero := ⟦0⟧, zero_add := game.add_comm_group_with_one._proof_3, add_zero := game.add_comm_group_with_one._proof_4, nsmul := add_comm_group.nsmul._default ⟦0⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6, nsmul_zero' := game.add_comm_group_with_one._proof_7, nsmul_succ' := game.add_comm_group_with_one._proof_8, neg := quot.lift (λ (x : pgame), ⟦-x⟧) game.add_comm_group_with_one._proof_9, sub := add_comm_group.sub._default (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_10 ⟦0⟧ game.add_comm_group_with_one._proof_11 game.add_comm_group_with_one._proof_12 (add_comm_group.nsmul._default ⟦0⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_13 game.add_comm_group_with_one._proof_14 (quot.lift (λ (x : pgame), ⟦-x⟧) game.add_comm_group_with_one._proof_9), sub_eq_add_neg := game.add_comm_group_with_one._proof_15, zsmul := add_comm_group.zsmul._default (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_16 ⟦0⟧ game.add_comm_group_with_one._proof_17 game.add_comm_group_with_one._proof_18 (add_comm_group.nsmul._default ⟦0⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_19 game.add_comm_group_with_one._proof_20 (quot.lift (λ (x : pgame), ⟦-x⟧) game.add_comm_group_with_one._proof_9), zsmul_zero' := game.add_comm_group_with_one._proof_21, zsmul_succ' := game.add_comm_group_with_one._proof_22, zsmul_neg' := game.add_comm_group_with_one._proof_23, add_left_neg := game.add_comm_group_with_one._proof_24, add_comm := game.add_comm_group_with_one._proof_25, int_cast := add_group_with_one.int_cast._default (add_group_with_one.nat_cast._default ⟦1⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_26 ⟦0⟧ game.add_comm_group_with_one._proof_27 game.add_comm_group_with_one._proof_28 (add_comm_group.nsmul._default ⟦0⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_29 game.add_comm_group_with_one._proof_30) (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_31 ⟦0⟧ game.add_comm_group_with_one._proof_32 game.add_comm_group_with_one._proof_33 (add_comm_group.nsmul._default ⟦0⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_34 game.add_comm_group_with_one._proof_35 ⟦1⟧ game.add_comm_group_with_one._proof_36 game.add_comm_group_with_one._proof_37 (quot.lift (λ (x : pgame), ⟦-x⟧) game.add_comm_group_with_one._proof_9) (add_comm_group.sub._default (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_10 ⟦0⟧ game.add_comm_group_with_one._proof_11 game.add_comm_group_with_one._proof_12 (add_comm_group.nsmul._default ⟦0⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_13 game.add_comm_group_with_one._proof_14 (quot.lift (λ (x : pgame), ⟦-x⟧) game.add_comm_group_with_one._proof_9)) game.add_comm_group_with_one._proof_38 (add_comm_group.zsmul._default (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_16 ⟦0⟧ game.add_comm_group_with_one._proof_17 game.add_comm_group_with_one._proof_18 (add_comm_group.nsmul._default ⟦0⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_19 game.add_comm_group_with_one._proof_20 (quot.lift (λ (x : pgame), ⟦-x⟧) game.add_comm_group_with_one._proof_9)) game.add_comm_group_with_one._proof_39 game.add_comm_group_with_one._proof_40 game.add_comm_group_with_one._proof_41 game.add_comm_group_with_one._proof_42, nat_cast := add_group_with_one.nat_cast._default ⟦1⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_26 ⟦0⟧ game.add_comm_group_with_one._proof_27 game.add_comm_group_with_one._proof_28 (add_comm_group.nsmul._default ⟦0⟧ (quotient.lift₂ (λ (x y : pgame), ⟦x + y⟧) game.add_comm_group_with_one._proof_1) game.add_comm_group_with_one._proof_5 game.add_comm_group_with_one._proof_6) game.add_comm_group_with_one._proof_29 game.add_comm_group_with_one._proof_30, one := ⟦1⟧, nat_cast_zero := game.add_comm_group_with_one._proof_43, nat_cast_succ := game.add_comm_group_with_one._proof_44, int_cast_of_nat := game.add_comm_group_with_one._proof_45, int_cast_neg_succ_of_nat := game.add_comm_group_with_one._proof_46}

source

@[protected, instance]

def game.inhabited :

inhabited game

Equations

game.inhabited = {default := 0}

source

@[protected, instance]

def game.partial_order :

partial_order game

Equations

game.partial_order = {le := quotient.lift₂ has_le.le game.partial_order._proof_1, lt := quotient.lift₂ has_lt.lt game.partial_order._proof_2, le_refl := game.partial_order._proof_3, le_trans := game.partial_order._proof_4, lt_iff_le_not_le := game.partial_order._proof_5, le_antisymm := game.partial_order._proof_6}

source

def game.lf :

game → 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

game.lf = quotient.lift₂ pgame.lf game.lf._proof_1

Instances for game.lf

game.lf.is_trichotomous

source

@[simp]

theorem game.not_le {x y : game} :

¬x ≤ y ↔ y.lf x

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

source

@[simp]

theorem game.not_lf {x y : game} :

¬x.lf y ↔ y ≤ x

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

source

@[protected, instance]

def game.lf.is_trichotomous :

is_trichotomous game game.lf

source

theorem pgame.le_iff_game_le {x y : pgame} :

x ≤ y ↔ ⟦x⟧ ≤ ⟦y⟧

source

theorem pgame.lf_iff_game_lf {x y : pgame} :

x.lf y ↔ game.lf ⟦x⟧ ⟦y⟧

source

theorem pgame.lt_iff_game_lt {x y : pgame} :

x < y ↔ ⟦x⟧ < ⟦y⟧

source

theorem pgame.equiv_iff_game_eq {x y : pgame} :

x.equiv y ↔ ⟦x⟧ = ⟦y⟧

source

def game.fuzzy :

game → game → Prop

The fuzzy, confused, or incomparable relation on games.

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

Equations

game.fuzzy = quotient.lift₂ pgame.fuzzy game.fuzzy._proof_1

source

theorem pgame.fuzzy_iff_game_fuzzy {x y : pgame} :

x.fuzzy y ↔ game.fuzzy ⟦x⟧ ⟦y⟧

source

@[protected, instance]

def game.covariant_class_add_le :

covariant_class game game has_add.add has_le.le

source

@[protected, instance]

def game.covariant_class_swap_add_le :

covariant_class game game (function.swap has_add.add) has_le.le

source

@[protected, instance]

def game.covariant_class_add_lt :

covariant_class game game has_add.add has_lt.lt

source

@[protected, instance]

def game.covariant_class_swap_add_lt :

covariant_class game game (function.swap has_add.add) has_lt.lt

source

theorem game.add_lf_add_right {b c : game} (h : b.lf c) (a : game) :

(b + a).lf (c + a)

source

theorem game.add_lf_add_left {b c : game} (h : b.lf c) (a : game) :

(a + b).lf (a + c)

source

@[protected, instance]

def game.ordered_add_comm_group :

ordered_add_comm_group game

Equations

game.ordered_add_comm_group = {add := add_comm_group_with_one.add game.add_comm_group_with_one, add_assoc := _, zero := add_comm_group_with_one.zero game.add_comm_group_with_one, zero_add := _, add_zero := _, nsmul := add_comm_group_with_one.nsmul game.add_comm_group_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group_with_one.neg game.add_comm_group_with_one, sub := add_comm_group_with_one.sub game.add_comm_group_with_one, sub_eq_add_neg := _, zsmul := add_comm_group_with_one.zsmul game.add_comm_group_with_one, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le game.partial_order, lt := partial_order.lt game.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := game.ordered_add_comm_group._proof_1}

source

theorem game.bdd_above_of_small (s : set game) [small ↥s] :

bdd_above s

A small set s of games is bounded above.

source

theorem game.bdd_below_of_small (s : set game) [small ↥s] :

bdd_below s

A small set s of games is bounded below.

source

@[simp]

theorem pgame.quot_neg (a : pgame) :

⟦-a⟧ = -⟦a⟧

source

@[simp]

theorem pgame.quot_add (a b : pgame) :

⟦a + b⟧ = ⟦a⟧ + ⟦b⟧

source

@[simp]

theorem pgame.quot_sub (a b : pgame) :

⟦a - b⟧ = ⟦a⟧ - ⟦b⟧

source

theorem pgame.quot_eq_of_mk_quot_eq {x y : pgame} (L : x.left_moves ≃ y.left_moves) (R : x.right_moves ≃ y.right_moves) (hl : ∀ (i : x.left_moves), ⟦x.move_left i⟧ = ⟦y.move_left (⇑L i)⟧) (hr : ∀ (j : x.right_moves), ⟦x.move_right j⟧ = ⟦y.move_right (⇑R j)⟧) :

⟦x⟧ = ⟦y⟧

source

@[protected, instance]

def pgame.has_mul :

has_mul 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

pgame.has_mul = {mul := λ (x y : pgame), pgame.rec (λ (xl xr : Type u) (xL : xl → pgame) (xR : xr → pgame) (IHxl : Π (ᾰ : xl), (λ (x : pgame), pgame → pgame) (xL ᾰ)) (IHxr : Π (ᾰ : xr), (λ (x : pgame), pgame → pgame) (xR ᾰ)) (y : pgame), pgame.rec (λ (yl yr : Type u) (yL : yl → pgame) (yR : yr → pgame) (IHyl : Π (ᾰ : yl), (λ (y : pgame), pgame) (yL ᾰ)) (IHyr : Π (ᾰ : yr), (λ (y : pgame), pgame) (yR ᾰ)), pgame.mk (xl × yl ⊕ xr × yr) (xl × yr ⊕ xr × yl) (λ (ᾰ : xl × yl ⊕ xr × yr), ᾰ.cases_on (λ (ᾰ : xl × yl), ᾰ.cases_on (λ (i : xl) (j : yl), IHxl i (pgame.mk yl yr yL yR) + IHyl j - IHxl i (yL j))) (λ (ᾰ : xr × yr), ᾰ.cases_on (λ (i : xr) (j : yr), IHxr i (pgame.mk yl yr yL yR) + IHyr j - IHxr i (yR j)))) (λ (ᾰ : xl × yr ⊕ xr × yl), ᾰ.cases_on (λ (ᾰ : xl × yr), ᾰ.cases_on (λ (i : xl) (j : yr), IHxl i (pgame.mk yl yr yL yR) + IHyr j - IHxl i (yR j))) (λ (ᾰ : xr × yl), ᾰ.cases_on (λ (i : xr) (j : yl), IHxr i (pgame.mk yl yr yL yR) + IHyl j - IHxr i (yL j))))) y) x y}

source

theorem pgame.left_moves_mul (x y : pgame) :

(x * y).left_moves = (x.left_moves × y.left_moves ⊕ x.right_moves × y.right_moves)

source

theorem pgame.right_moves_mul (x y : pgame) :

(x * y).right_moves = (x.left_moves × y.right_moves ⊕ x.right_moves × y.left_moves)

source

def pgame.to_left_moves_mul {x y : pgame} :

x.left_moves × y.left_moves ⊕ x.right_moves × y.right_moves ≃ (x * y).left_moves

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

pgame.to_left_moves_mul = equiv.cast pgame.to_left_moves_mul._proof_1

source

def pgame.to_right_moves_mul {x y : pgame} :

x.left_moves × y.right_moves ⊕ x.right_moves × y.left_moves ≃ (x * y).right_moves

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

pgame.to_right_moves_mul = equiv.cast pgame.to_right_moves_mul._proof_1

source

@[simp]

theorem pgame.mk_mul_move_left_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} {j : yl} :

(pgame.mk xl xr xL xR * pgame.mk yl yr yL yR).move_left (sum.inl (i, j)) = xL i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yL j - xL i * yL j

source

@[simp]

theorem pgame.mul_move_left_inl {x y : pgame} {i : x.left_moves} {j : y.left_moves} :

(x * y).move_left (⇑pgame.to_left_moves_mul (sum.inl (i, j))) = x.move_left i * y + x * y.move_left j - x.move_left i * y.move_left j

source

@[simp]

theorem pgame.mk_mul_move_left_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} {j : yr} :

(pgame.mk xl xr xL xR * pgame.mk yl yr yL yR).move_left (sum.inr (i, j)) = xR i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yR j - xR i * yR j

source

@[simp]

theorem pgame.mul_move_left_inr {x y : pgame} {i : x.right_moves} {j : y.right_moves} :

(x * y).move_left (⇑pgame.to_left_moves_mul (sum.inr (i, j))) = x.move_right i * y + x * y.move_right j - x.move_right i * y.move_right j

source

@[simp]

theorem pgame.mk_mul_move_right_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} {j : yr} :

(pgame.mk xl xr xL xR * pgame.mk yl yr yL yR).move_right (sum.inl (i, j)) = xL i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yR j - xL i * yR j

source

@[simp]

theorem pgame.mul_move_right_inl {x y : pgame} {i : x.left_moves} {j : y.right_moves} :

(x * y).move_right (⇑pgame.to_right_moves_mul (sum.inl (i, j))) = x.move_left i * y + x * y.move_right j - x.move_left i * y.move_right j

source

@[simp]

theorem pgame.mk_mul_move_right_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} {j : yl} :

(pgame.mk xl xr xL xR * pgame.mk yl yr yL yR).move_right (sum.inr (i, j)) = xR i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yL j - xR i * yL j

source

@[simp]

theorem pgame.mul_move_right_inr {x y : pgame} {i : x.right_moves} {j : y.left_moves} :

(x * y).move_right (⇑pgame.to_right_moves_mul (sum.inr (i, j))) = x.move_right i * y + x * y.move_left j - x.move_right i * y.move_left j

source

@[simp]

theorem pgame.neg_mk_mul_move_left_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} {j : yr} :

(-(pgame.mk xl xr xL xR * pgame.mk yl yr yL yR)).move_left (sum.inl (i, j)) = -(xL i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yR j - xL i * yR j)

source

@[simp]

theorem pgame.neg_mk_mul_move_left_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} {j : yl} :

(-(pgame.mk xl xr xL xR * pgame.mk yl yr yL yR)).move_left (sum.inr (i, j)) = -(xR i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yL j - xR i * yL j)

source

@[simp]

theorem pgame.neg_mk_mul_move_right_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} {j : yl} :

(-(pgame.mk xl xr xL xR * pgame.mk yl yr yL yR)).move_right (sum.inl (i, j)) = -(xL i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yL j - xL i * yL j)

source

@[simp]

theorem pgame.neg_mk_mul_move_right_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} {j : yr} :

(-(pgame.mk xl xr xL xR * pgame.mk yl yr yL yR)).move_right (sum.inr (i, j)) = -(xR i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yR j - xR i * yR j)

source

theorem pgame.left_moves_mul_cases {x y : pgame} (k : (x * y).left_moves) {P : (x * y).left_moves → Prop} (hl : ∀ (ix : x.left_moves) (iy : y.left_moves), P (⇑pgame.to_left_moves_mul (sum.inl (ix, iy)))) (hr : ∀ (jx : x.right_moves) (jy : y.right_moves), P (⇑pgame.to_left_moves_mul (sum.inr (jx, jy)))) :

P k

source

theorem pgame.right_moves_mul_cases {x y : pgame} (k : (x * y).right_moves) {P : (x * y).right_moves → Prop} (hl : ∀ (ix : x.left_moves) (jy : y.right_moves), P (⇑pgame.to_right_moves_mul (sum.inl (ix, jy)))) (hr : ∀ (jx : x.right_moves) (iy : y.left_moves), P (⇑pgame.to_right_moves_mul (sum.inr (jx, iy)))) :

P k

source

def pgame.mul_comm_relabelling (x y : pgame) :

(x * y).relabelling (y * x)

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

Equations

(pgame.mk xl xr xL xR).mul_comm_relabelling (pgame.mk yl yr yL yR) = pgame.relabelling.mk ((equiv.prod_comm xl yl).sum_congr (equiv.prod_comm xr yr)) ((equiv.sum_comm (xl × yr) (xr × yl)).trans ((equiv.prod_comm xr yl).sum_congr (equiv.prod_comm xl yr))) (λ (i : (pgame.mk xl xr xL xR * pgame.mk yl yr yL yR).left_moves), sum.cases_on i (λ (i : xl × yl), i.cases_on (λ (i : xl) (j : yl), id ((((xL i * pgame.mk yl yr yL yR).add_comm_relabelling (pgame.mk xl xr xL xR * yL j)).trans (((pgame.mk xl xr xL xR).mul_comm_relabelling (yL j)).add_congr ((xL i).mul_comm_relabelling (pgame.mk yl yr yL yR)))).sub_congr ((xL i).mul_comm_relabelling (yL j))))) (λ (i : xr × yr), i.cases_on (λ (i : xr) (j : yr), id ((((xR i * pgame.mk yl yr yL yR).add_comm_relabelling (pgame.mk xl xr xL xR * yR j)).trans (((pgame.mk xl xr xL xR).mul_comm_relabelling (yR j)).add_congr ((xR i).mul_comm_relabelling (pgame.mk yl yr yL yR)))).sub_congr ((xR i).mul_comm_relabelling (yR j)))))) (λ (j : (pgame.mk xl xr xL xR * pgame.mk yl yr yL yR).right_moves), sum.cases_on j (λ (j : xl × yr), j.cases_on (λ (i : xl) (j : yr), id ((((xL i * pgame.mk yl yr yL yR).add_comm_relabelling (pgame.mk xl xr xL xR * yR j)).trans (((pgame.mk xl xr xL xR).mul_comm_relabelling (yR j)).add_congr ((xL i).mul_comm_relabelling (pgame.mk yl yr yL yR)))).sub_congr ((xL i).mul_comm_relabelling (yR j))))) (λ (j : xr × yl), j.cases_on (λ (i : xr) (j : yl), id ((((xR i * pgame.mk yl yr yL yR).add_comm_relabelling (pgame.mk xl xr xL xR * yL j)).trans (((pgame.mk xl xr xL xR).mul_comm_relabelling (yL j)).add_congr ((xR i).mul_comm_relabelling (pgame.mk yl yr yL yR)))).sub_congr ((xR i).mul_comm_relabelling (yL j))))))

source

theorem pgame.quot_mul_comm (x y : pgame) :

⟦x * y⟧ = ⟦y * x⟧

source

theorem pgame.mul_comm_equiv (x y : pgame) :

(x * y).equiv (y * x)

x * y is equivalent to y * x.

source

@[protected, instance]

def pgame.is_empty_mul_zero_left_moves (x : pgame) :

is_empty (x * 0).left_moves

source

@[protected, instance]

def pgame.is_empty_mul_zero_right_moves (x : pgame) :

is_empty (x * 0).right_moves

source

@[protected, instance]

def pgame.is_empty_zero_mul_left_moves (x : pgame) :

is_empty (0 * x).left_moves

source

@[protected, instance]

def pgame.is_empty_zero_mul_right_moves (x : pgame) :

is_empty (0 * x).right_moves

source

def pgame.mul_zero_relabelling (x : pgame) :

(x * 0).relabelling 0

x * 0 has exactly the same moves as 0.

Equations

x.mul_zero_relabelling = pgame.relabelling.is_empty (x * 0)

source

theorem pgame.mul_zero_equiv (x : pgame) :

(x * 0).equiv 0

x * 0 is equivalent to 0.

source

@[simp]

theorem pgame.quot_mul_zero (x : pgame) :

⟦x * 0⟧ = ⟦0⟧

source

def pgame.zero_mul_relabelling (x : pgame) :

(0 * x).relabelling 0

0 * x has exactly the same moves as 0.

Equations

x.zero_mul_relabelling = pgame.relabelling.is_empty (0 * x)

source

theorem pgame.zero_mul_equiv (x : pgame) :

(0 * x).equiv 0

0 * x is equivalent to 0.

source

@[simp]

theorem pgame.quot_zero_mul (x : pgame) :

⟦0 * x⟧ = ⟦0⟧

source

def pgame.neg_mul_relabelling (x y : pgame) :

(-x * y).relabelling (-(x * y))

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

Equations

(pgame.mk xl xr xL xR).neg_mul_relabelling (pgame.mk yl yr yL yR) = pgame.relabelling.mk (equiv.sum_comm (xr × yl) (xl × yr)) (equiv.sum_comm (xr × yr) (xl × yl)) (λ (i : (-pgame.mk xl xr xL xR * pgame.mk yl yr yL yR).left_moves), sum.cases_on i (λ (i : xr × yl), i.cases_on (λ (i : xr) (j : yl), id (((xR i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yL j).neg_add_relabelling (-(xR i * yL j))).trans ((((xR i * pgame.mk yl yr yL yR).neg_add_relabelling (pgame.mk xl xr xL xR * yL j)).trans (((xR i).neg_mul_relabelling (pgame.mk yl yr yL yR)).symm.add_congr ((pgame.mk xl xr xL xR).neg_mul_relabelling (yL j)).symm)).sub_congr ((xR i).neg_mul_relabelling (yL j)).symm)).symm)) (λ (i : xl × yr), i.cases_on (λ (i : xl) (j : yr), id (((xL i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yR j).neg_add_relabelling (-(xL i * yR j))).trans ((((xL i * pgame.mk yl yr yL yR).neg_add_relabelling (pgame.mk xl xr xL xR * yR j)).trans (((xL i).neg_mul_relabelling (pgame.mk yl yr yL yR)).symm.add_congr ((pgame.mk xl xr xL xR).neg_mul_relabelling (yR j)).symm)).sub_congr ((xL i).neg_mul_relabelling (yR j)).symm)).symm))) (λ (j : (-pgame.mk xl xr xL xR * pgame.mk yl yr yL yR).right_moves), sum.cases_on j (λ (j : xr × yr), j.cases_on (λ (i : xr) (j : yr), id (((xR i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yR j).neg_add_relabelling (-(xR i * yR j))).trans ((((xR i * pgame.mk yl yr yL yR).neg_add_relabelling (pgame.mk xl xr xL xR * yR j)).trans (((xR i).neg_mul_relabelling (pgame.mk yl yr yL yR)).symm.add_congr ((pgame.mk xl xr xL xR).neg_mul_relabelling (yR j)).symm)).sub_congr ((xR i).neg_mul_relabelling (yR j)).symm)).symm)) (λ (j : xl × yl), j.cases_on (λ (i : xl) (j : yl), id (((xL i * pgame.mk yl yr yL yR + pgame.mk xl xr xL xR * yL j).neg_add_relabelling (-(xL i * yL j))).trans ((((xL i * pgame.mk yl yr yL yR).neg_add_relabelling (pgame.mk xl xr xL xR * yL j)).trans (((xL i).neg_mul_relabelling (pgame.mk yl yr yL yR)).symm.add_congr ((pgame.mk xl xr xL xR).neg_mul_relabelling (yL j)).symm)).sub_congr ((xL i).neg_mul_relabelling (yL j)).symm)).symm)))

source

@[simp]

theorem pgame.quot_neg_mul (x y : pgame) :

⟦-x * y⟧ = -⟦x * y⟧

source

def pgame.mul_neg_relabelling (x y : pgame) :

(x * -y).relabelling (-(x * y))

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

Equations

x.mul_neg_relabelling y = (x.mul_comm_relabelling (-y)).trans ((y.neg_mul_relabelling x).trans (y.mul_comm_relabelling x).neg_congr)

source

@[simp]

theorem pgame.quot_mul_neg (x y : pgame) :

⟦x * -y⟧ = -⟦x * y⟧

source

@[simp]

theorem pgame.quot_left_distrib (x y z : pgame) :

⟦x * (y + z)⟧ = ⟦x * y⟧ + ⟦x * z⟧

source

theorem pgame.left_distrib_equiv (x y z : pgame) :

(x * (y + z)).equiv (x * y + x * z)

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

source

@[simp]

theorem pgame.quot_left_distrib_sub (x y z : pgame) :

⟦x * (y - z)⟧ = ⟦x * y⟧ - ⟦x * z⟧

source

@[simp]

theorem pgame.quot_right_distrib (x y z : pgame) :

⟦(x + y) * z⟧ = ⟦x * z⟧ + ⟦y * z⟧

source

theorem pgame.right_distrib_equiv (x y z : pgame) :

((x + y) * z).equiv (x * z + y * z)

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

source

@[simp]

theorem pgame.quot_right_distrib_sub (x y z : pgame) :

⟦(y - z) * x⟧ = ⟦y * x⟧ - ⟦z * x⟧

source

def pgame.mul_one_relabelling (x : pgame) :

(x * 1).relabelling x

x * 1 has the same moves as x.

Equations

(pgame.mk xl xr xL xR).mul_one_relabelling = _.mpr (pgame.relabelling.mk ((equiv.sum_empty (xl × punit) (xr × pempty)).trans (equiv.prod_punit xl)) ((equiv.empty_sum (xl × pempty) (xr × punit)).trans (equiv.prod_punit xr)) (λ (i : (pgame.mk xl xr xL xR * pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim).left_moves), sum.cases_on i (λ (i : xl × punit), i.cases_on (λ (i : xl) (i_snd : punit), i_snd.cases_on (id (((pgame.relabelling.refl (xL i * pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim + pgame.mk xl xr xL xR * 0)).sub_congr (xL i).mul_zero_relabelling).trans (_.mpr ((xL i * pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim + pgame.mk xl xr xL xR * 0).add_zero_relabelling.trans (((xL i).mul_one_relabelling.add_congr (pgame.mk xl xr xL xR).mul_zero_relabelling).trans (xL i).add_zero_relabelling))))))) (λ (i : xr × pempty), i.cases_on (λ (i : xr) (i_snd : pempty), pempty.cases_on (λ (i_snd : pempty), ((pgame.mk xl xr xL xR * pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim).move_left (sum.inr (i, i_snd))).relabelling ((pgame.mk xl xr xL xR).move_left (⇑((equiv.sum_empty (xl × punit) (xr × pempty)).trans (equiv.prod_punit xl)) (sum.inr (i, i_snd))))) i_snd))) (λ (j : (pgame.mk xl xr xL xR * pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim).right_moves), sum.cases_on j (λ (j : xl × pempty), j.cases_on (λ (i : xl) (j_snd : pempty), pempty.cases_on (λ (j_snd : pempty), ((pgame.mk xl xr xL xR * pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim).move_right (sum.inl (i, j_snd))).relabelling ((pgame.mk xl xr xL xR).move_right (⇑((equiv.empty_sum (xl × pempty) (xr × punit)).trans (equiv.prod_punit xr)) (sum.inl (i, j_snd))))) j_snd)) (λ (j : xr × punit), j.cases_on (λ (i : xr) (j_snd : punit), j_snd.cases_on (id (((pgame.relabelling.refl (xR i * pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim + pgame.mk xl xr xL xR * 0)).sub_congr (xR i).mul_zero_relabelling).trans (_.mpr ((xR i * pgame.mk punit pempty (λ (_x : punit), 0) pempty.elim + pgame.mk xl xr xL xR * 0).add_zero_relabelling.trans (((xR i).mul_one_relabelling.add_congr (pgame.mk xl xr xL xR).mul_zero_relabelling).trans (xR i).add_zero_relabelling)))))))))

source

@[simp]

theorem pgame.quot_mul_one (x : pgame) :

⟦x * 1⟧ = ⟦x⟧

source

theorem pgame.mul_one_equiv (x : pgame) :

(x * 1).equiv x

x * 1 is equivalent to x.

source

def pgame.one_mul_relabelling (x : pgame) :

(1 * x).relabelling x

1 * x has the same moves as x.

Equations

x.one_mul_relabelling = (1.mul_comm_relabelling x).trans x.mul_one_relabelling

source

@[simp]

theorem pgame.quot_one_mul (x : pgame) :

⟦1 * x⟧ = ⟦x⟧

source

theorem pgame.one_mul_equiv (x : pgame) :

(1 * x).equiv x

1 * x is equivalent to x.

source

theorem pgame.quot_mul_assoc (x y z : pgame) :

⟦x * y * z⟧ = ⟦x * (y * z)⟧

source

theorem pgame.mul_assoc_equiv (x y z : pgame) :

(x * y * z).equiv (x * (y * z))

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

source

inductive pgame.inv_ty (l r : Type u) :

bool → Type u

zero : Π {l r : Type u}, pgame.inv_ty l r bool.ff
left₁ : Π {l r : Type u}, r → pgame.inv_ty l r bool.ff → pgame.inv_ty l r bool.ff
left₂ : Π {l r : Type u}, l → pgame.inv_ty l r bool.tt → pgame.inv_ty l r bool.ff
right₁ : Π {l r : Type u}, l → pgame.inv_ty l r bool.ff → pgame.inv_ty l r bool.tt
right₂ : Π {l r : Type u}, r → pgame.inv_ty l r bool.tt → pgame.inv_ty l r bool.tt

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 inv_val is the function part.

Instances for pgame.inv_ty

source

@[protected, instance]

def pgame.inv_ty.is_empty (l r : Type u) [is_empty l] [is_empty r] :

is_empty (pgame.inv_ty l r bool.tt)

source

@[protected, instance]

def pgame.inv_ty.inhabited (l r : Type u) :

inhabited (pgame.inv_ty l r bool.ff)

Equations

pgame.inv_ty.inhabited l r = {default := pgame.inv_ty.zero r}

source

@[protected, instance]

def pgame.unique_inv_ty (l r : Type u) [is_empty l] [is_empty r] :

unique (pgame.inv_ty l r bool.ff)

Equations

pgame.unique_inv_ty l r = {to_inhabited := {default := inhabited.default (pgame.inv_ty.inhabited l r)}, uniq := _}

source

def pgame.inv_val {l r : Type u_1} (L : l → pgame) (R : r → pgame) (IHl : l → pgame) (IHr : r → pgame) {b : bool} :

pgame.inv_ty l r b → 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 inv_ty.

Equations

pgame.inv_val L R IHl IHr (pgame.inv_ty.right₂ i j) = (1 + (R i - pgame.mk l r L R) * pgame.inv_val L R IHl IHr j) * IHr i
pgame.inv_val L R IHl IHr (pgame.inv_ty.right₁ i j) = (1 + (L i - pgame.mk l r L R) * pgame.inv_val L R IHl IHr j) * IHl i
pgame.inv_val L R IHl IHr (pgame.inv_ty.left₂ i j) = (1 + (L i - pgame.mk l r L R) * pgame.inv_val L R IHl IHr j) * IHl i
pgame.inv_val L R IHl IHr (pgame.inv_ty.left₁ i j) = (1 + (R i - pgame.mk l r L R) * pgame.inv_val L R IHl IHr j) * IHr i
pgame.inv_val L R IHl IHr pgame.inv_ty.zero = 0

source

@[simp]

theorem pgame.inv_val_is_empty {l r : Type u} {b : bool} (L : l → pgame) (R : r → pgame) (IHl : l → pgame) (IHr : r → pgame) (i : pgame.inv_ty l r b) [is_empty l] [is_empty r] :

pgame.inv_val L R IHl IHr i = 0

source

def pgame.inv' :

pgame → 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

(pgame.mk l r L R).inv' = let l' : Type u_1 := {i // 0 < L i}, L' : l' → pgame := λ (i : l'), L i.val, IHl' : l' → pgame := λ (i : l'), (L i.val).inv', IHr : r → pgame := λ (i : r), (R i).inv' in pgame.mk (pgame.inv_ty l' r bool.ff) (pgame.inv_ty l' r bool.tt) (pgame.inv_val L' R IHl' IHr) (pgame.inv_val L' R IHl' IHr)