Surreal cuts

A surreal cut is defined as consisting of two sets of surreals with the following properties:

• They are complementary sets.
• Every surreal in the first set is less than every surreal in the second set.

This construction resembles the construction of the surreals themselves, but yields a "bigger" structure, which can embed the surreals, but is also a complete linear order.

Note that surreal cuts are not the same as the Dedekind completion of the surreals. Whereas the Dedekind completion maps every element of the original order to a unique Dedekind cut, every surreal number x actually corresponds to two cuts (Iio x, Ici x) and (Iic x, Ioi x), which we call the left and right cut, respectively.

The theory of concept lattices gives us a very simple definition of surreal cuts as Concept Surreal Surreal (⬝ < ⬝). However, we've attempted to provide a thin wrapper for all concept terminology.

@[reducible, inline]

abbrev Surreal.Cut : Type (u_1 + 1)

A surreal cut, sometimes called a section, consists of two complementary sets of surreals, where every surreal in the former is less than every surreal in the latter.

Equations

• Surreal.Cut = Concept Surreal Surreal fun (x1 x2 : Surreal) => x1 < x2

Basic definitions

def Surreal.Cut.left (x : Cut) : Set Surreal

The left set in a cut. This is an alias for Concept.extent.

Equations

• x.left = x.extent

def Surreal.Cut.right (x : Cut) : Set Surreal

The right set in a cut. This is an alias for Concept.intent.

Equations

• x.right = x.intent

theorem Surreal.Cut.left_lt_right {x : Cut} {y z : Surreal} (hy : y ∈ x.left) (hz : z ∈ x.right) : y < z

theorem Surreal.Cut.disjoint_left_right (x : Cut) : Disjoint x.left x.right

theorem Surreal.Cut.codisjoint_left_right (x : Cut) : Codisjoint x.left x.right

theorem Surreal.Cut.isCompl_left_right (x : Cut) : IsCompl x.left x.right

theorem Surreal.Cut.isLowerSet_left (c : Cut) : IsLowerSet c.left

theorem Surreal.Cut.isUpperSet_right (c : Cut) : IsUpperSet c.right

theorem Surreal.Cut.ext {c d : Cut} (h : c.left = d.left) : c = d

theorem Surreal.Cut.ext_iff {c d : Cut} : c = d ↔ c.left = d.left

theorem Surreal.Cut.ext' {c d : Cut} (h : c.right = d.right) : c = d

theorem Surreal.Cut.left_injective : Function.Injective left

theorem Surreal.Cut.right_injective : Function.Injective right

@[simp]

theorem Surreal.Cut.left_inj {c d : Cut} : c.left = d.left ↔ c = d

@[simp]

theorem Surreal.Cut.right_inj {c d : Cut} : c.right = d.right ↔ c = d

@[simp]

theorem Surreal.Cut.left_subset_left_iff {c d : Cut} : c.left ⊆ d.left ↔ c ≤ d

@[simp]

theorem Surreal.Cut.left_ssubset_left_iff {c d : Cut} : c.left ⊂ d.left ↔ c < d

@[simp]

theorem Surreal.Cut.right_subset_right_iff {c d : Cut} : c.right ⊆ d.right ↔ d ≤ c

@[simp]

theorem Surreal.Cut.right_ssubset_right_iff {c d : Cut} : c.right ⊂ d.right ↔ d < c

@[simp]

theorem Surreal.Cut.compl_left (x : Cut) : x.leftᶜ = x.right

@[simp]

theorem Surreal.Cut.compl_right (x : Cut) : x.rightᶜ = x.left

@[simp]

theorem Surreal.Cut.notMem_left_iff {x : Cut} {y : Surreal} : y ∉ x.left ↔ y ∈ x.right

@[simp]

theorem Surreal.Cut.notMem_right_iff {x : Cut} {y : Surreal} : y ∉ x.right ↔ y ∈ x.left

@[simp]

theorem Surreal.Cut.right_bot : ⊥.right = Set.univ

@[simp]

theorem Surreal.Cut.left_bot : ⊥.left = ∅

@[simp]

theorem Surreal.Cut.left_top : ⊤.left = Set.univ

@[simp]

theorem Surreal.Cut.right_top : ⊤.right = ∅

instance Surreal.Cut.instTotalLe : Std.Total fun (x1 x2 : Cut) => x1 ≤ x2

@[instance_reducible]

noncomputable instance Surreal.Cut.instLinearOrder : LinearOrder Cut

Equations

• Surreal.Cut.instLinearOrder = Lattice.toLinearOrder Surreal.Cut

@[instance_reducible]

noncomputable instance Surreal.Cut.instCompleteLinearOrder : CompleteLinearOrder Cut

Equations

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

@[simp]

theorem Surreal.Cut.left_min (x y : Cut) : (min x y).left = x.left ∩ y.left

@[simp]

theorem Surreal.Cut.right_min (x y : Cut) : (min x y).right = x.right ∪ y.right

@[simp]

theorem Surreal.Cut.right_max (x y : Cut) : (max x y).right = x.right ∩ y.right

@[simp]

theorem Surreal.Cut.left_max (x y : Cut) : (max x y).left = x.left ∪ y.left

@[simp]

theorem Surreal.Cut.left_sInf (s : Set Cut) : (sInf s).left = ⋂ x ∈ s, x.left

@[simp]

theorem Surreal.Cut.right_sInf (s : Set Cut) : (sInf s).right = ⋃ x ∈ s, x.right

@[simp]

theorem Surreal.Cut.right_sSup (s : Set Cut) : (sSup s).right = ⋂ x ∈ s, x.right

@[simp]

theorem Surreal.Cut.left_sSup (s : Set Cut) : (sSup s).left = ⋃ x ∈ s, x.left

@[simp]

theorem Surreal.Cut.left_iInf {ι : Sort u_1} (f : ι → Cut) : (⨅ (i : ι), f i).left = ⋂ (i : ι), (f i).left

@[simp]

theorem Surreal.Cut.right_iInf {ι : Sort u_1} (f : ι → Cut) : (⨅ (i : ι), f i).right = ⋃ (i : ι), (f i).right

@[simp]

theorem Surreal.Cut.right_iSup {ι : Sort u_1} (f : ι → Cut) : (⨆ (i : ι), f i).right = ⋂ (i : ι), (f i).right

@[simp]

theorem Surreal.Cut.left_iSup {ι : Sort u_1} (f : ι → Cut) : (⨆ (i : ι), f i).left = ⋃ (i : ι), (f i).left

instance Surreal.Cut.instNontrivial : Nontrivial Cut

theorem Surreal.Cut.lt_iff_nonempty_inter {x y : Cut} : x < y ↔ (x.right ∩ y.left).Nonempty

@[instance_reducible]

noncomputable instance Surreal.Cut.instNeg : Neg Cut

Equations

• Surreal.Cut.instNeg = { neg := fun (x : Surreal.Cut) => { extent := -x.intent, intent := -x.extent, upperPolar_extent := ⋯, lowerPolar_intent := ⋯ } }

@[simp]

theorem Surreal.Cut.left_neg (x : Cut) : (-x).left = -x.right

@[simp]

theorem Surreal.Cut.right_neg (x : Cut) : (-x).right = -x.left

@[instance_reducible]

noncomputable instance Surreal.Cut.instInvolutiveNeg : InvolutiveNeg Cut

Equations

• Surreal.Cut.instInvolutiveNeg = { toNeg := Surreal.Cut.instNeg, neg_neg := ⋯ }

@[simp]

theorem Surreal.Cut.neg_bot : -⊥ = ⊤

@[simp]

theorem Surreal.Cut.neg_top : -⊤ = ⊥

@[simp]

theorem Surreal.Cut.neg_min (x y : Cut) : -min x y = max (-x) (-y)

@[simp]

theorem Surreal.Cut.neg_max (x y : Cut) : -max x y = min (-x) (-y)

@[simp]

theorem Surreal.Cut.neg_sInf (s : Set Cut) : -sInf s = sSup (-s)

@[simp]

theorem Surreal.Cut.neg_sSup (s : Set Cut) : -sSup s = sInf (-s)

@[simp]

theorem Surreal.Cut.neg_iInf {ι : Sort u_1} (f : ι → Cut) : -⨅ (i : ι), f i = ⨆ (i : ι), -f i

@[simp]

theorem Surreal.Cut.neg_iSup {ι : Sort u_1} (f : ι → Cut) : -⨆ (i : ι), f i = ⨅ (i : ι), -f i

@[simp]

theorem Surreal.Cut.neg_le_neg_iff {x y : Cut} : -x ≤ -y ↔ y ≤ x

theorem Surreal.Cut.neg_le {x y : Cut} : -x ≤ y ↔ -y ≤ x

theorem Surreal.Cut.le_neg {x y : Cut} : x ≤ -y ↔ y ≤ -x

@[simp]

theorem Surreal.Cut.neg_lt_neg_iff {x y : Cut} : -x < -y ↔ y < x

theorem Surreal.Cut.neg_lt {x y : Cut} : -x < y ↔ -y < x

theorem Surreal.Cut.lt_neg {x y : Cut} : x < -y ↔ y < -x

Cuts from games

def Surreal.Cut.leftGame : Game →o Cut

The left stop $L(x)$ of a game x is such that its right set consists of surreals equal or larger to it.

Equations

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

def Surreal.Cut.rightGame : Game →o Cut

The right stop $R(x)$ of a game x is such that its left set consists of surreals equal or lesser to it.

Equations

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

def Surreal.Cut.leftSurreal : Surreal ↪o Cut

The cut just to the left of a surreal number.

Equations

• Surreal.Cut.leftSurreal = { toFun := fun (x : Surreal) => Concept.copy (Surreal.Cut.leftGame (Surreal.toGame x)) (Set.Iio x) (Set.Ici x) ⋯ ⋯, inj' := ⋯, map_rel_iff' := ⋯ }

def Surreal.Cut.rightSurreal : Surreal ↪o Cut

The cut just to the right of a surreal number.

Equations

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

@[simp]

theorem Surreal.Cut.left_leftGame (x : Game) : (leftGame x).left = {y : Surreal | ¬x ≤ toGame y}

@[simp]

theorem Surreal.Cut.right_leftGame (x : Game) : (leftGame x).right = {y : Surreal | x ≤ toGame y}

@[simp]

theorem Surreal.Cut.left_rightGame (x : Game) : (rightGame x).left = {y : Surreal | toGame y ≤ x}

@[simp]

theorem Surreal.Cut.right_rightGame (x : Game) : (rightGame x).right = {y : Surreal | ¬toGame y ≤ x}

@[simp]

theorem Surreal.Cut.left_leftSurreal (x : Surreal) : (leftSurreal x).left = Set.Iio x

@[simp]

theorem Surreal.Cut.right_leftSurreal (x : Surreal) : (leftSurreal x).right = Set.Ici x

@[simp]

theorem Surreal.Cut.left_rightSurreal (x : Surreal) : (rightSurreal x).left = Set.Iic x

@[simp]

theorem Surreal.Cut.right_rightSurreal (x : Surreal) : (rightSurreal x).right = Set.Ioi x

theorem Surreal.Cut.mem_left_leftGame {x : Game} {y : Surreal} : y ∈ (leftGame x).left ↔ ¬x ≤ toGame y

theorem Surreal.Cut.mem_right_leftGame {x : Game} {y : Surreal} : y ∈ (leftGame x).right ↔ x ≤ toGame y

theorem Surreal.Cut.mem_left_rightGame {x : Game} {y : Surreal} : y ∈ (rightGame x).left ↔ toGame y ≤ x

theorem Surreal.Cut.mem_right_rightGame {x : Game} {y : Surreal} : y ∈ (rightGame x).right ↔ ¬toGame y ≤ x

theorem Surreal.Cut.mem_left_leftSurreal {x y : Surreal} : y ∈ (leftSurreal x).left ↔ y < x

theorem Surreal.Cut.mem_right_leftSurreal {x y : Surreal} : y ∈ (leftSurreal x).right ↔ x ≤ y

theorem Surreal.Cut.mem_left_rightSurreal {x y : Surreal} : y ∈ (rightSurreal x).left ↔ y ≤ x

theorem Surreal.Cut.mem_right_rightSurreal {x y : Surreal} : y ∈ (rightSurreal x).right ↔ x < y

@[simp]

theorem Surreal.Cut.leftGame_toGame (x : Surreal) : leftGame (toGame x) = leftSurreal x

@[simp]

theorem Surreal.Cut.rightGame_toGame (x : Surreal) : rightGame (toGame x) = rightSurreal x

@[simp]

theorem Surreal.Cut.leftGame_neg (x : Game) : leftGame (-x) = -rightGame x

@[simp]

theorem Surreal.Cut.rightGame_neg (x : Game) : rightGame (-x) = -leftGame x

@[simp]

theorem Surreal.Cut.neg_leftGame_image (s : Set Game) : -⇑leftGame '' s = ⇑rightGame '' (-s)

@[simp]

theorem Surreal.Cut.neg_rightGame_image (s : Set Game) : -⇑rightGame '' s = ⇑leftGame '' (-s)

@[simp]

theorem Surreal.Cut.neg_leftSurreal (x : Surreal) : -leftSurreal x = rightSurreal (-x)

@[simp]

theorem Surreal.Cut.neg_rightSurreal (x : Surreal) : -rightSurreal x = leftSurreal (-x)

@[simp]

theorem Surreal.Cut.neg_leftSurreal_image (s : Set Surreal) : -⇑leftSurreal '' s = ⇑rightSurreal '' (-s)

@[simp]

theorem Surreal.Cut.neg_rightSurreal_image (s : Set Surreal) : -⇑rightSurreal '' s = ⇑leftSurreal '' (-s)

@[simp]

theorem Surreal.Cut.le_leftSurreal_iff {x : Cut} {y : Surreal} : x ≤ leftSurreal y ↔ y ∈ x.right

@[simp]

theorem Surreal.Cut.leftSurreal_lt_iff {x : Surreal} {y : Cut} : leftSurreal x < y ↔ x ∈ y.left

@[simp]

theorem Surreal.Cut.rightSurreal_le_iff {x : Surreal} {y : Cut} : rightSurreal x ≤ y ↔ x ∈ y.left

@[simp]

theorem Surreal.Cut.lt_rightSurreal_iff {x : Cut} {y : Surreal} : x < rightSurreal y ↔ y ∈ x.right

theorem Surreal.Cut.leftSurreal_lt_rightSurreal (x : Surreal) : leftSurreal x < rightSurreal x

@[simp]

theorem Surreal.Cut.leftSurreal_le_rightSurreal (x : Surreal) : leftSurreal x ≤ rightSurreal x

theorem Surreal.Cut.leftSurreal_lt_rightSurreal_iff {x y : Surreal} : leftSurreal x < rightSurreal y ↔ x ≤ y

@[simp]

theorem Surreal.Cut.rightSurreal_lt_leftSurreal_iff {x y : Surreal} : rightSurreal x < leftSurreal y ↔ x < y

theorem Surreal.Cut.leftSurreal_strictMono : StrictMono ⇑leftSurreal

theorem Surreal.Cut.rightSurreal_strictMono : StrictMono ⇑rightSurreal

theorem Surreal.Cut.leftSurreal_lt_leftSurreal_iff {x y : Surreal} : leftSurreal x < leftSurreal y ↔ x < y

theorem Surreal.Cut.rightSurreal_lt_rightSurreal_iff {x y : Surreal} : leftSurreal x < leftSurreal y ↔ x < y

theorem Surreal.Cut.leftSurreal_covBy_rightSurreal (x : Surreal) : leftSurreal x ⋖ rightSurreal x

@[simp]

theorem Surreal.Cut.leftSurreal_ne_rightSurreal (x y : Surreal) : leftSurreal x ≠ rightSurreal y

@[simp]

theorem Surreal.Cut.rightSurreal_ne_leftSurreal (x y : Surreal) : rightSurreal x ≠ leftSurreal y

theorem Surreal.Cut.leftGame_lt_rightGame_iff {x : Game} : leftGame x < rightGame x ↔ x ∈ Set.range ⇑toGame

@[simp]

theorem Surreal.Cut.leftGame_ne_bot (x : Game) : leftGame x ≠ ⊥

@[simp]

theorem Surreal.Cut.leftGame_ne_top (x : Game) : leftGame x ≠ ⊤

@[simp]

theorem Surreal.Cut.rightGame_ne_bot (x : Game) : rightGame x ≠ ⊥

@[simp]

theorem Surreal.Cut.rightGame_ne_top (x : Game) : rightGame x ≠ ⊤

@[simp]

theorem Surreal.Cut.leftSurreal_ne_bot (x : Surreal) : leftSurreal x ≠ ⊥

@[simp]

theorem Surreal.Cut.leftSurreal_ne_top (x : Surreal) : leftSurreal x ≠ ⊤

@[simp]

theorem Surreal.Cut.rightSurreal_ne_bot (x : Surreal) : rightSurreal x ≠ ⊥

@[simp]

theorem Surreal.Cut.rightSurreal_ne_top (x : Surreal) : rightSurreal x ≠ ⊤

theorem Surreal.Cut.sInf_leftSurreal_right (x : Cut) : sInf (⇑leftSurreal '' x.right) = x

theorem Surreal.Cut.sSup_rightSurreal_left (x : Cut) : sSup (⇑rightSurreal '' x.left) = x

theorem Surreal.Cut.leftSurreal_mem_of_sInf_eq {s : Set Cut} {x : Surreal} (hs : sInf s = leftSurreal x) : leftSurreal x ∈ s

theorem Surreal.Cut.rightSurreal_mem_of_sInf_eq {s : Set Cut} {x : Surreal} [Small.{u, u + 1} ↑s] (hs : sInf s = rightSurreal x) : rightSurreal x ∈ s

theorem Surreal.Cut.rightSurreal_mem_of_sSup_eq {s : Set Cut} {x : Surreal} : sSup s = rightSurreal x → rightSurreal x ∈ s

theorem Surreal.Cut.leftSurreal_mem_of_sSup_eq {s : Set Cut} {x : Surreal} [Small.{u, u + 1} ↑s] : sSup s = leftSurreal x → leftSurreal x ∈ s

Group action by translation

@[instance_reducible]

noncomputable instance Surreal.Cut.instVAdd : VAdd Surreal Cut

Equations

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

@[simp]

theorem Surreal.Cut.left_vadd' (a : Surreal) (x : Cut) : (a +ᵥ x).left = (fun (x : Surreal) => x - a) ⁻¹' x.left

theorem Surreal.Cut.left_vadd (a : Surreal) (x : Cut) : (a +ᵥ x).left = (fun (x : Surreal) => x + a) '' x.left

@[simp]

theorem Surreal.Cut.right_vadd' (a : Surreal) (x : Cut) : (a +ᵥ x).right = (fun (x : Surreal) => x - a) ⁻¹' x.right

theorem Surreal.Cut.right_vadd (a : Surreal) (x : Cut) : (a +ᵥ x).right = (fun (x : Surreal) => x + a) '' x.right

@[instance_reducible]

noncomputable instance Surreal.Cut.instAddAction : AddAction Surreal Cut

Equations

• Surreal.Cut.instAddAction = { toVAdd := Surreal.Cut.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }

@[simp]

theorem Surreal.Cut.vadd_bot (a : Surreal) : a +ᵥ ⊥ = ⊥

@[simp]

theorem Surreal.Cut.vadd_top (a : Surreal) : a +ᵥ ⊤ = ⊤

@[simp]

theorem Surreal.Cut.vadd_leftGame (a : Surreal) (x : Game) : a +ᵥ leftGame x = leftGame (toGame a + x)

@[simp]

theorem Surreal.Cut.vadd_rightGame (a : Surreal) (x : Game) : a +ᵥ rightGame x = rightGame (toGame a + x)

@[simp]

theorem Surreal.Cut.vadd_leftSurreal (a x : Surreal) : a +ᵥ leftSurreal x = leftSurreal (a + x)

@[simp]

theorem Surreal.Cut.vadd_rightSurreal (a x : Surreal) : a +ᵥ rightSurreal x = rightSurreal (a + x)

theorem Surreal.Cut.neg_vadd (a : Surreal) (x : Cut) : -(a +ᵥ x) = -a +ᵥ -x

Calculating cuts

def Surreal.Cut.supLeft (x : IGame) : Cut

The supremum $L'(x)$ of all right cuts of left options of x.

If infRight x ≤ supLeft x then leftGame x = supLeft x and rightGame x = infRight x; otherwise, x is equivalent to the simplest surreal between supLeft x and infRight x.

Equations

• Surreal.Cut.supLeft x = ⨆ i ∈ IGame.moves Player.left x, Surreal.Cut.rightGame (Game.mk i)

theorem Surreal.Cut.left_supLeft (x : IGame) : (supLeft x).left = ⋃ i ∈ IGame.moves Player.left x, {y : Surreal | toGame y ≤ Game.mk i}

theorem Surreal.Cut.right_supLeft (x : IGame) : (supLeft x).right = ⋂ i ∈ IGame.moves Player.left x, {y : Surreal | ¬toGame y ≤ Game.mk i}

theorem Surreal.Cut.supLeft_mem_of_short {x : IGame} [x.Short] (hx : (IGame.moves Player.left x).Nonempty) : ∃ y ∈ IGame.moves Player.left x, rightGame (Game.mk y) = supLeft x

def Surreal.Cut.infRight (x : IGame) : Cut

The infimum $R'(x)$ of all left cuts of right options of x.

If infRight x ≤ supLeft x then leftGame x = supLeft x and rightGame x = infRight x; otherwise, x is equivalent to the simplest surreal between supLeft x and infRight x.

Equations

• Surreal.Cut.infRight x = ⨅ i ∈ IGame.moves Player.right x, Surreal.Cut.leftGame (Game.mk i)

theorem Surreal.Cut.left_infRight (x : IGame) : (infRight x).left = ⋂ i ∈ IGame.moves Player.right x, {y : Surreal | ¬Game.mk i ≤ toGame y}

theorem Surreal.Cut.right_infRight (x : IGame) : (infRight x).right = ⋃ i ∈ IGame.moves Player.right x, {y : Surreal | Game.mk i ≤ toGame y}

theorem Surreal.Cut.infRight_mem_of_short {x : IGame} [x.Short] (hx : (IGame.moves Player.right x).Nonempty) : ∃ y ∈ IGame.moves Player.right x, leftGame (Game.mk y) = infRight x

@[simp]

theorem Surreal.Cut.infRight_neg (x : IGame) : infRight (-x) = -supLeft x

@[simp]

theorem Surreal.Cut.supLeft_neg (x : IGame) : supLeft (-x) = -infRight x

theorem Surreal.Cut.leftGame_eq_supLeft_of_le {x : IGame} (h : infRight x ≤ supLeft x) : leftGame (Game.mk x) = supLeft x

theorem Surreal.Cut.rightGame_eq_infRight_of_le {x : IGame} : infRight x ≤ supLeft x → rightGame (Game.mk x) = infRight x

def Surreal.Cut.Fits (x : Surreal) (y z : Cut) : Prop

A surreal x fits between two cuts y and z when x ∈ y.right ∩ z.left.

Equations

• Surreal.Cut.Fits x y z = (x ∈ y.right ∩ z.left)

theorem Surreal.Cut.Fits.lt {x : Surreal} {y z : Cut} (h : Fits x y z) : y < z

@[simp]

theorem Surreal.Cut.fits_leftSurreal_rightSurreal {x y : Surreal} : Fits x (leftSurreal y) (rightSurreal y) ↔ x = y

theorem Surreal.Cut.Fits.le_leftSurreal {x : Surreal} {y z : Cut} (h : Fits x y z) : y ≤ leftSurreal x

theorem Surreal.Cut.Fits.rightSurreal_le {x : Surreal} {y z : Cut} (h : Fits x y z) : rightSurreal x ≤ z

theorem Surreal.Cut.not_fits_iff {x : Surreal} {y z : Cut} : ¬Fits x y z ↔ x ∈ y.left ∪ z.right

noncomputable def Surreal.Cut.simplestBtwn {x y : Cut} (h : x < y) : Surreal

The simplest surreal number (in terms of birthday) that fits between two cuts.

Equations

• Surreal.Cut.simplestBtwn h = Classical.choose ⋯

theorem Surreal.Cut.fits_simplestBtwn {x y : Cut} (h : x < y) : Fits (simplestBtwn h) x y

theorem Surreal.Cut.birthday_simplestBtwn_le_of_fits {x y : Cut} {z : Surreal} (hz : Fits z x y) : (simplestBtwn ⋯).birthday ≤ z.birthday

theorem Surreal.Cut.fits_supLeft_infRight {x y : IGame} [x.Numeric] : Fits (mk x) (supLeft y) (infRight y) ↔ x.Fits y

theorem Surreal.Cut.simplestBtwn_leftGame_rightGame {x : Game} (h : leftGame x < rightGame x) : toGame (simplestBtwn h) = x

@[simp]

theorem Surreal.Cut.simplestBtwn_leftSurreal_rightSurreal (x : Surreal) : simplestBtwn ⋯ = x

theorem Surreal.Cut.simplestBtwn_supLeft_infRight {x : IGame} (h : supLeft x < infRight x) : toGame (simplestBtwn h) = Game.mk x

If x is a game with supLeft x < infRight x, then the simplest number between those two cuts is equal to x.

theorem Surreal.Cut.supLeft_lt_infRight_of_equiv_numeric {x y : IGame} [y.Numeric] (h : x ≈ y) : supLeft x < infRight x

theorem Surreal.Cut.supLeft_lt_infRight_of_numeric (x : IGame) [x.Numeric] : supLeft x < infRight x

Numeric cuts

class inductive Surreal.Cut.Numeric : Cut → Prop

We say that a cut is numeric when it's either a left or right cut from a surreal.

• leftSurreal (y : Surreal) : (leftSurreal y).Numeric
• rightSurreal (y : Surreal) : (rightSurreal y).Numeric

theorem Surreal.Cut.numeric_def' (a✝ : Cut) : a✝.Numeric ↔ (∃ (y : Surreal), a✝ = leftSurreal y) ∨ ∃ (y : Surreal), a✝ = rightSurreal y

theorem Surreal.Cut.numeric_def {x : Cut} : x.Numeric ↔ x ∈ Set.range ⇑leftSurreal ∪ Set.range ⇑rightSurreal

@[simp]

theorem Surreal.Cut.Numeric.ne_bot (x : Cut) [hx : x.Numeric] : x ≠ ⊥

@[simp]

theorem Surreal.Cut.Numeric.ne_top (x : Cut) [hx : x.Numeric] : x ≠ ⊤

noncomputable def Surreal.Cut.Numeric.recOn' {motive : (x : Cut) → [x.Numeric] → Sort u_1} (x : Cut) [h : x.Numeric] (leftSurreal : (y : Surreal) → motive (leftSurreal y)) (rightSurreal : (y : Surreal) → motive (rightSurreal y)) : motive x

A version of the recursor which eliminates into Sort.

Equations

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

@[simp]

theorem Surreal.Cut.Numeric.recOn'_leftSurreal {motive : (x : Cut) → [x.Numeric] → Sort u_1} (y : Surreal) (leftSurreal : (y : Surreal) → motive (leftSurreal y)) (rightSurreal : (y : Surreal) → motive (rightSurreal y)) : recOn' (Cut.leftSurreal y) leftSurreal rightSurreal = leftSurreal y

@[simp]

theorem Surreal.Cut.Numeric.recOn'_rightSurreal {motive : (x : Cut) → [x.Numeric] → Sort u_1} (y : Surreal) (leftSurreal : (y : Surreal) → motive (leftSurreal y)) (rightSurreal : (y : Surreal) → motive (rightSurreal y)) : recOn' (Cut.rightSurreal y) leftSurreal rightSurreal = rightSurreal y

instance Surreal.Cut.Numeric.leftGame (x : IGame) [x.Short] : (leftGame (Game.mk x)).Numeric

instance Surreal.Cut.Numeric.rightGame (x : IGame) [x.Short] : (rightGame (Game.mk x)).Numeric

theorem Surreal.Cut.Numeric.supLeft {x : IGame} [x.Short] (hx : (IGame.moves Player.left x).Nonempty) : (supLeft x).Numeric

theorem Surreal.Cut.Numeric.infRight {x : IGame} [x.Short] (hx : (IGame.moves Player.right x).Nonempty) : (infRight x).Numeric

noncomputable def Surreal.Cut.toSurreal (x : Cut) [x.Numeric] : Surreal

Returns the surreal defining the cut.

Equations

• x.toSurreal = Surreal.Cut.Numeric.recOn' x (fun (y : Surreal) => y) fun (y : Surreal) => y

@[simp]

theorem Surreal.Cut.toSurreal_leftSurreal (x : Surreal) : (leftSurreal x).toSurreal = x

@[simp]

theorem Surreal.Cut.toSurreal_rightSurreal (x : Surreal) : (rightSurreal x).toSurreal = x