Order properties of pregames

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

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

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

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

instance SetTheory.PGame.le : LE PGame

The less or equal relation on pre-games.

If 0 ≤ x, then Left can win x as the second player. x ≤ y means that 0 ≤ y - x. See PGame.le_iff_sub_nonneg.

Equations

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

def SetTheory.PGame.LF (x y : PGame) : Prop

The less or fuzzy relation on pre-games. x ⧏ y is defined as ¬ y ≤ x.

If 0 ⧏ x, then Left can win x as the first player. x ⧏ y means that 0 ⧏ y - x. See PGame.lf_iff_sub_zero_lf.

Equations

• x.LF y = ¬y ≤ x

def SetTheory.PGame.«term_⧏_» : Lean.TrailingParserDescr

The less or fuzzy relation on pre-games. x ⧏ y is defined as ¬ y ≤ x.

If 0 ⧏ x, then Left can win x as the first player. x ⧏ y means that 0 ⧏ y - x. See PGame.lf_iff_sub_zero_lf.

Equations

• SetTheory.PGame.«term_⧏_» = Lean.ParserDescr.trailingNode `SetTheory.PGame.«term_⧏_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⧏ ") (Lean.ParserDescr.cat `term 51))

@[simp]

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

@[simp]

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

theorem LE.le.not_gf {x y : SetTheory.PGame} : x ≤ y → ¬y.LF x

theorem SetTheory.PGame.LF.not_ge {x y : PGame} : x.LF y → ¬y ≤ x

theorem SetTheory.PGame.le_iff_forall_lf {x y : PGame} : x ≤ y ↔ (∀ (i : x.LeftMoves), (x.moveLeft i).LF y) ∧ ∀ (j : y.RightMoves), x.LF (y.moveRight j)

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

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

@[simp]

theorem SetTheory.PGame.mk_le_mk {xl xr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} {yl yr : Type u_1} {yL : yl → PGame} {yR : yr → PGame} : mk xl xr xL xR ≤ mk yl yr yL yR ↔ (∀ (i : xl), (xL i).LF (mk yl yr yL yR)) ∧ ∀ (j : yr), (mk xl xr xL xR).LF (yR j)

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

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

theorem SetTheory.PGame.lf_iff_exists_le {x y : PGame} : x.LF y ↔ (∃ (i : y.LeftMoves), x ≤ y.moveLeft i) ∨ ∃ (j : x.RightMoves), x.moveRight j ≤ y

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

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

@[simp]

theorem SetTheory.PGame.mk_lf_mk {xl xr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} {yl yr : Type u_1} {yL : yl → PGame} {yR : yr → PGame} : (mk xl xr xL xR).LF (mk yl yr yL yR) ↔ (∃ (i : yl), mk xl xr xL xR ≤ yL i) ∨ ∃ (j : xr), xR j ≤ mk yl yr yL yR

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

theorem SetTheory.PGame.le_or_gf (x y : PGame) : x ≤ y ∨ y.LF x

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

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

Alias of SetTheory.PGame.moveLeft_lf_of_le.

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

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

Alias of SetTheory.PGame.lf_moveRight_of_le.

theorem SetTheory.PGame.lf_of_moveRight_le {x y : PGame} {j : x.RightMoves} (h : x.moveRight j ≤ y) : x.LF y

theorem SetTheory.PGame.lf_of_le_moveLeft {x y : PGame} {i : y.LeftMoves} (h : x ≤ y.moveLeft i) : x.LF y

theorem SetTheory.PGame.lf_of_le_mk {xl xr : Type u_1} {xL : xl → PGame} {xR : xr → PGame} {y : PGame} : mk xl xr xL xR ≤ y → ∀ (i : xl), (xL i).LF y

theorem SetTheory.PGame.lf_of_mk_le {x : PGame} {yl yr : Type u_1} {yL : yl → PGame} {yR : yr → PGame} : x ≤ mk yl yr yL yR → ∀ (j : yr), x.LF (yR j)

theorem SetTheory.PGame.mk_lf_of_le {xl xr : Type u_1} {y : PGame} {j : xr} (xL : xl → PGame) {xR : xr → PGame} : xR j ≤ y → (mk xl xr xL xR).LF y

theorem SetTheory.PGame.lf_mk_of_le {x : PGame} {yl yr : Type u_1} {yL : yl → PGame} (yR : yr → PGame) {i : yl} : x ≤ yL i → x.LF (mk yl yr yL yR)

instance SetTheory.PGame.instPreorder : Preorder PGame

Equations

• SetTheory.PGame.instPreorder = Preorder.mk SetTheory.PGame.instPreorder.proof_1 SetTheory.PGame.instPreorder.proof_2 SetTheory.PGame.instPreorder.proof_3

theorem SetTheory.PGame.Identical.le {x y : PGame} : x.Identical y → x ≤ y

theorem SetTheory.PGame.Identical.ge {x y : PGame} (h : x.Identical y) : y ≤ x

theorem SetTheory.PGame.lt_iff_le_and_lf {x y : PGame} : x < y ↔ x ≤ y ∧ x.LF y

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

theorem SetTheory.PGame.lf_of_lt {x y : PGame} (h : x < y) : x.LF y

theorem LT.lt.lf {x y : SetTheory.PGame} (h : x < y) : x.LF y

Alias of SetTheory.PGame.lf_of_lt.

theorem SetTheory.PGame.lf_irrefl (x : PGame) : ¬x.LF x

instance SetTheory.PGame.instIsIrreflLF : IsIrrefl PGame fun (x1 x2 : PGame) => x1.LF x2

theorem SetTheory.PGame.not_lt {x y : PGame} : ¬x < y ↔ y.LF x ∨ y ≤ x

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

instance SetTheory.PGame.instTransLeLF : Trans (fun (x1 x2 : PGame) => x1 ≤ x2) (fun (x1 x2 : PGame) => x1.LF x2) fun (x1 x2 : PGame) => x1.LF x2

Equations

• SetTheory.PGame.instTransLeLF = { trans := ⋯ }

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

instance SetTheory.PGame.instTransLFLe : Trans (fun (x1 x2 : PGame) => x1.LF x2) (fun (x1 x2 : PGame) => x1 ≤ x2) fun (x1 x2 : PGame) => x1.LF x2

Equations

• SetTheory.PGame.instTransLFLe = { trans := ⋯ }

theorem LE.le.trans_lf {x y z : SetTheory.PGame} (h₁ : x ≤ y) (h₂ : y.LF z) : x.LF z

Alias of SetTheory.PGame.lf_of_le_of_lf.

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

Alias of SetTheory.PGame.lf_of_lf_of_le.

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

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

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

Alias of SetTheory.PGame.lf_of_lt_of_lf.

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

Alias of SetTheory.PGame.lf_of_lf_of_lt.

theorem SetTheory.PGame.moveLeft_lf {x : PGame} (i : x.LeftMoves) : (x.moveLeft i).LF x

theorem SetTheory.PGame.lf_moveRight {x : PGame} (j : x.RightMoves) : x.LF (x.moveRight j)

theorem SetTheory.PGame.lf_mk {xl xr : Type u_1} (xL : xl → PGame) (xR : xr → PGame) (i : xl) : (xL i).LF (mk xl xr xL xR)

theorem SetTheory.PGame.mk_lf {xl xr : Type u_1} (xL : xl → PGame) (xR : xr → PGame) (j : xr) : (mk xl xr xL xR).LF (xR j)

theorem SetTheory.PGame.le_of_forall_lt {x y : PGame} (h₁ : ∀ (i : x.LeftMoves), x.moveLeft i < y) (h₂ : ∀ (j : y.RightMoves), x < y.moveRight j) : x ≤ y

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

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

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

Note that it's often more convenient to use le_iff_forall_lf, which only unfolds the definition by one step.

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

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

Note that it's often more convenient to use lf_iff_exists_le, which only unfolds the definition by one step.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem SetTheory.PGame.zero_le_of_isEmpty_rightMoves (x : PGame) [IsEmpty x.RightMoves] : 0 ≤ x

@[simp]

theorem SetTheory.PGame.le_zero_of_isEmpty_leftMoves (x : PGame) [IsEmpty x.LeftMoves] : x ≤ 0

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

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

Equations

• SetTheory.PGame.rightResponse h i = Classical.choose ⋯

theorem SetTheory.PGame.rightResponse_spec {x : PGame} (h : x ≤ 0) (i : x.LeftMoves) : (x.moveLeft i).moveRight (rightResponse h i) ≤ 0

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

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

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

Equations

• SetTheory.PGame.leftResponse h j = Classical.choose ⋯

theorem SetTheory.PGame.leftResponse_spec {x : PGame} (h : 0 ≤ x) (j : x.RightMoves) : 0 ≤ (x.moveRight j).moveLeft (leftResponse h j)

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

theorem SetTheory.PGame.bddAbove_range_of_small {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → PGame) : BddAbove (Set.range f)

A small family of pre-games is bounded above.

theorem SetTheory.PGame.bddAbove_of_small (s : Set PGame) [Small.{u, u + 1} ↑s] : BddAbove s

A small set of pre-games is bounded above.

theorem SetTheory.PGame.bddBelow_range_of_small {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → PGame) : BddBelow (Set.range f)

A small family of pre-games is bounded below.

theorem SetTheory.PGame.bddBelow_of_small (s : Set PGame) [Small.{u, u + 1} ↑s] : BddBelow s

A small set of pre-games is bounded below.

def SetTheory.PGame.Equiv (x y : PGame) : Prop

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

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

Equations

• x.Equiv y = (x ≤ y ∧ y ≤ x)

instance SetTheory.PGame.instIsEquivEquiv : IsEquiv PGame Equiv

instance SetTheory.PGame.setoid : Setoid PGame

Equations

• SetTheory.PGame.setoid = { r := SetTheory.PGame.Equiv, iseqv := SetTheory.PGame.setoid.proof_1 }

theorem SetTheory.PGame.equiv_def {x y : PGame} : x ≈ y ↔ x ≤ y ∧ y ≤ x

theorem SetTheory.PGame.Equiv.le {x y : PGame} (h : x ≈ y) : x ≤ y

theorem SetTheory.PGame.Equiv.ge {x y : PGame} (h : x ≈ y) : y ≤ x

theorem SetTheory.PGame.equiv_rfl {x : PGame} : x ≈ x

theorem SetTheory.PGame.equiv_refl (x : PGame) : x ≈ x

theorem SetTheory.PGame.Equiv.symm {x y : PGame} : x ≈ y → y ≈ x

theorem SetTheory.PGame.Equiv.trans {x y z : PGame} : x ≈ y → y ≈ z → x ≈ z

theorem SetTheory.PGame.equiv_comm {x y : PGame} : x ≈ y ↔ y ≈ x

theorem SetTheory.PGame.equiv_of_eq {x y : PGame} (h : x = y) : x ≈ y

theorem SetTheory.PGame.Identical.equiv {x y : PGame} (h : x.Identical y) : x ≈ y

theorem SetTheory.PGame.le_of_le_of_equiv {x y z : PGame} (h₁ : x ≤ y) (h₂ : y ≈ z) : x ≤ z

instance SetTheory.PGame.instTransLeEquiv : Trans (fun (x1 x2 : PGame) => x1 ≤ x2) (fun (x1 x2 : PGame) => x1 ≈ x2) fun (x1 x2 : PGame) => x1 ≤ x2

Equations

• SetTheory.PGame.instTransLeEquiv = { trans := ⋯ }

theorem SetTheory.PGame.le_of_equiv_of_le {x y z : PGame} (h₁ : x ≈ y) : y ≤ z → x ≤ z

instance SetTheory.PGame.instTransEquivLe : Trans (fun (x1 x2 : PGame) => x1 ≈ x2) (fun (x1 x2 : PGame) => x1 ≤ x2) fun (x1 x2 : PGame) => x1 ≤ x2

Equations

• SetTheory.PGame.instTransEquivLe = { trans := ⋯ }

theorem SetTheory.PGame.LF.not_equiv {x y : PGame} (h : x.LF y) : ¬x ≈ y

theorem SetTheory.PGame.LF.not_equiv' {x y : PGame} (h : x.LF y) : ¬y ≈ x

theorem SetTheory.PGame.LF.not_gt {x y : PGame} (h : x.LF y) : ¬y < x

theorem SetTheory.PGame.le_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ ≤ y₁) : x₂ ≤ y₂

theorem SetTheory.PGame.le_congr {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ ≤ y₁ ↔ x₂ ≤ y₂

theorem SetTheory.PGame.le_congr_left {x₁ x₂ y : PGame} (hx : x₁ ≈ x₂) : x₁ ≤ y ↔ x₂ ≤ y

theorem SetTheory.PGame.le_congr_right {x y₁ y₂ : PGame} (hy : y₁ ≈ y₂) : x ≤ y₁ ↔ x ≤ y₂

theorem SetTheory.PGame.lf_congr {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁.LF y₁ ↔ x₂.LF y₂

theorem SetTheory.PGame.lf_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁.LF y₁ → x₂.LF y₂

theorem SetTheory.PGame.lf_congr_left {x₁ x₂ y : PGame} (hx : x₁ ≈ x₂) : x₁.LF y ↔ x₂.LF y

theorem SetTheory.PGame.lf_congr_right {x y₁ y₂ : PGame} (hy : y₁ ≈ y₂) : x.LF y₁ ↔ x.LF y₂

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

instance SetTheory.PGame.instTransLFEquiv : Trans (fun (x1 x2 : PGame) => x1.LF x2) (fun (x1 x2 : PGame) => x1 ≈ x2) fun (x1 x2 : PGame) => x1.LF x2

Equations

• SetTheory.PGame.instTransLFEquiv = { trans := ⋯ }

theorem SetTheory.PGame.lf_of_equiv_of_lf {x y z : PGame} (h₁ : x ≈ y) : y.LF z → x.LF z

instance SetTheory.PGame.instTransEquivLF : Trans (fun (x1 x2 : PGame) => x1 ≈ x2) (fun (x1 x2 : PGame) => x1.LF x2) fun (x1 x2 : PGame) => x1.LF x2

Equations

• SetTheory.PGame.instTransEquivLF = { trans := ⋯ }

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

instance SetTheory.PGame.instTransLtEquiv : Trans (fun (x1 x2 : PGame) => x1 < x2) (fun (x1 x2 : PGame) => x1 ≈ x2) fun (x1 x2 : PGame) => x1 < x2

Equations

• SetTheory.PGame.instTransLtEquiv = { trans := ⋯ }

theorem SetTheory.PGame.lt_of_equiv_of_lt {x y z : PGame} (h₁ : x ≈ y) : y < z → x < z

instance SetTheory.PGame.instTransEquivLt : Trans (fun (x1 x2 : PGame) => x1 ≈ x2) (fun (x1 x2 : PGame) => x1 < x2) fun (x1 x2 : PGame) => x1 < x2

Equations

• SetTheory.PGame.instTransEquivLt = { trans := ⋯ }

theorem SetTheory.PGame.lt_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ < y₁) : x₂ < y₂

theorem SetTheory.PGame.lt_congr {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ < y₁ ↔ x₂ < y₂

theorem SetTheory.PGame.lt_congr_left {x₁ x₂ y : PGame} (hx : x₁ ≈ x₂) : x₁ < y ↔ x₂ < y

theorem SetTheory.PGame.lt_congr_right {x y₁ y₂ : PGame} (hy : y₁ ≈ y₂) : x < y₁ ↔ x < y₂

theorem SetTheory.PGame.lt_or_equiv_of_le {x y : PGame} (h : x ≤ y) : x < y ∨ x ≈ y

theorem SetTheory.PGame.lf_or_equiv_or_gf (x y : PGame) : x.LF y ∨ x ≈ y ∨ y.LF x

theorem SetTheory.PGame.equiv_congr_left {y₁ y₂ : PGame} : y₁ ≈ y₂ ↔ ∀ (x₁ : PGame), x₁ ≈ y₁ ↔ x₁ ≈ y₂

theorem SetTheory.PGame.equiv_congr_right {x₁ x₂ : PGame} : x₁ ≈ x₂ ↔ ∀ (y₁ : PGame), x₁ ≈ y₁ ↔ x₂ ≈ y₁

theorem SetTheory.PGame.Equiv.of_exists {x y : PGame} (hl₁ : ∀ (i : x.LeftMoves), ∃ (j : y.LeftMoves), x.moveLeft i ≈ y.moveLeft j) (hr₁ : ∀ (i : x.RightMoves), ∃ (j : y.RightMoves), x.moveRight i ≈ y.moveRight j) (hl₂ : ∀ (j : y.LeftMoves), ∃ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft j) (hr₂ : ∀ (j : y.RightMoves), ∃ (i : x.RightMoves), x.moveRight i ≈ y.moveRight j) : x ≈ y

theorem SetTheory.PGame.Equiv.of_equiv {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves) (R : x.RightMoves ≃ y.RightMoves) (hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)) (hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)) : x ≈ y

@[deprecated SetTheory.PGame.Equiv.of_equiv (since := "2024-09-26")]

theorem SetTheory.PGame.equiv_of_mk_equiv {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves) (R : x.RightMoves ≃ y.RightMoves) (hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)) (hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)) : x ≈ y

Alias of SetTheory.PGame.Equiv.of_equiv.

def SetTheory.PGame.Fuzzy (x y : PGame) : Prop

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

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

Equations

• x.Fuzzy y = (x.LF y ∧ y.LF x)

def SetTheory.PGame.«term_‖_» : Lean.TrailingParserDescr

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

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

Equations

• SetTheory.PGame.«term_‖_» = Lean.ParserDescr.trailingNode `SetTheory.PGame.«term_‖_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ‖ ") (Lean.ParserDescr.cat `term 51))

theorem SetTheory.PGame.Fuzzy.swap {x y : PGame} : x.Fuzzy y → y.Fuzzy x

instance SetTheory.PGame.instIsSymmFuzzy : IsSymm PGame fun (x1 x2 : PGame) => x1.Fuzzy x2

theorem SetTheory.PGame.Fuzzy.swap_iff {x y : PGame} : x.Fuzzy y ↔ y.Fuzzy x

theorem SetTheory.PGame.fuzzy_irrefl (x : PGame) : ¬x.Fuzzy x

instance SetTheory.PGame.instIsIrreflFuzzy : IsIrrefl PGame fun (x1 x2 : PGame) => x1.Fuzzy x2

theorem SetTheory.PGame.lf_iff_lt_or_fuzzy {x y : PGame} : x.LF y ↔ x < y ∨ x.Fuzzy y

theorem SetTheory.PGame.lf_of_fuzzy {x y : PGame} (h : x.Fuzzy y) : x.LF y

theorem SetTheory.PGame.Fuzzy.lf {x y : PGame} (h : x.Fuzzy y) : x.LF y

Alias of SetTheory.PGame.lf_of_fuzzy.

theorem SetTheory.PGame.lt_or_fuzzy_of_lf {x y : PGame} : x.LF y → x < y ∨ x.Fuzzy y

theorem SetTheory.PGame.Fuzzy.not_equiv {x y : PGame} (h : x.Fuzzy y) : ¬x ≈ y

theorem SetTheory.PGame.Fuzzy.not_equiv' {x y : PGame} (h : x.Fuzzy y) : ¬y ≈ x

theorem SetTheory.PGame.not_fuzzy_of_le {x y : PGame} (h : x ≤ y) : ¬x.Fuzzy y

theorem SetTheory.PGame.not_fuzzy_of_ge {x y : PGame} (h : y ≤ x) : ¬x.Fuzzy y

theorem SetTheory.PGame.Equiv.not_fuzzy {x y : PGame} (h : x ≈ y) : ¬x.Fuzzy y

theorem SetTheory.PGame.Equiv.not_fuzzy' {x y : PGame} (h : x ≈ y) : ¬y.Fuzzy x

theorem SetTheory.PGame.fuzzy_congr {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁.Fuzzy y₁ ↔ x₂.Fuzzy y₂

theorem SetTheory.PGame.fuzzy_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁.Fuzzy y₁ → x₂.Fuzzy y₂

theorem SetTheory.PGame.fuzzy_congr_left {x₁ x₂ y : PGame} (hx : x₁ ≈ x₂) : x₁.Fuzzy y ↔ x₂.Fuzzy y

theorem SetTheory.PGame.fuzzy_congr_right {x y₁ y₂ : PGame} (hy : y₁ ≈ y₂) : x.Fuzzy y₁ ↔ x.Fuzzy y₂

theorem SetTheory.PGame.fuzzy_of_fuzzy_of_equiv {x y z : PGame} (h₁ : x.Fuzzy y) (h₂ : y ≈ z) : x.Fuzzy z

theorem SetTheory.PGame.fuzzy_of_equiv_of_fuzzy {x y z : PGame} (h₁ : x ≈ y) (h₂ : y.Fuzzy z) : x.Fuzzy z

theorem SetTheory.PGame.lt_or_equiv_or_gt_or_fuzzy (x y : PGame) : x < y ∨ x ≈ y ∨ y < x ∨ x.Fuzzy y

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

theorem SetTheory.PGame.lt_or_equiv_or_gf (x y : PGame) : x < y ∨ x ≈ y ∨ y.LF x

Interaction of relabelling with order

@[irreducible]

theorem SetTheory.PGame.Relabelling.le {x y : PGame} (r : x.Relabelling y) : x ≤ y

theorem SetTheory.PGame.Relabelling.ge {x y : PGame} (r : x.Relabelling y) : y ≤ x

theorem SetTheory.PGame.Relabelling.equiv {x y : PGame} (r : x.Relabelling y) : x ≈ y

A relabelling lets us prove equivalence of games.

theorem SetTheory.PGame.Equiv.isEmpty (x : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] : x ≈ 0

instance SetTheory.PGame.instCoeRelabellingEquiv {x y : PGame} : Coe (x.Relabelling y) (x ≈ y)

Equations

• SetTheory.PGame.instCoeRelabellingEquiv = { coe := ⋯ }

Interaction of option insertion with order

theorem SetTheory.PGame.le_insertLeft (x x' : PGame) : x ≤ x.insertLeft x'

A new left option cannot hurt Left.

theorem SetTheory.PGame.insertRight_le (x x' : PGame) : x.insertRight x' ≤ x

A new right option cannot hurt Right.

theorem SetTheory.PGame.insertLeft_equiv_of_lf {x x' : PGame} (h : x'.LF x) : x.insertLeft x' ≈ x

Adding a gift horse left option does not change the value of x. A gift horse left option is a game x' with x' ⧏ x. It is called "gift horse" because it seems like Left has gotten the "gift" of a new option, but actually the value of the game did not change.

theorem SetTheory.PGame.insertRight_equiv_of_lf {x x' : PGame} (h : x.LF x') : x.insertRight x' ≈ x

Adding a gift horse right option does not change the value of x. A gift horse right option is a game x' with x ⧏ x'. It is called "gift horse" because it seems like Right has gotten the "gift" of a new option, but actually the value of the game did not change.