Documentation

CombinatorialGames.Surreal.Birthday.Cut

Birthday of cuts #

We introduce the birthday of a (surreal) cut as Cut.birthday, and relate it to the birthdays of games and surreal numbers.

This definition doesn't exist in the literature, but it's useful in proving results about the birthdays of games. In particular, it allows us to prove the equality birthday_toGame : x.toGame.birthday = x.birthday for surreal numbers x. See https://mathoverflow.net/a/497645/147705 for a "plaintext" version of this proof.

Birthday of cuts #

source
noncomputable def Surreal.Cut.birthday (x : Cut) :
WithTop NatOrdinal

The birthday of a cut x is defined as the infimum of ⨆ a ∈ s, a.birthday + 1 over all sets s of surreals where either the infimum of the left cuts or the supremum of right cuts of s equals x.

The birthday takes values in WithTop NatOrdinal. Cuts with birthday ⊤ are precisely those where the set s is not small.

This isn't a term in the literature, but it's useful for proving that birthdays of surreals equal those of their associated games.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Surreal.Cut.birthday_eq_sSup_birthday (x : Cut) :
    ∃ (s : Set Surreal), (sInf (⇑leftSurreal '' s) = x ∨ sSup (⇑rightSurreal '' s) = x) ∧ sSup ((fun (x : Surreal) => ↑x.birthday + 1) '' s) = x.birthday
    source
    theorem Surreal.Cut.birthday_sInf_leftSurreal_le (s : Set Surreal) :
    (sInf (⇑leftSurreal '' s)).birthday ≤ sSup ((fun (x : Surreal) => ↑x.birthday + 1) '' s)
    source
    theorem Surreal.Cut.birthday_sSup_rightSurreal_le (s : Set Surreal) :
    (sSup (⇑rightSurreal '' s)).birthday ≤ sSup ((fun (x : Surreal) => ↑x.birthday + 1) '' s)
    source
    theorem Surreal.Cut.birthday_iInf_leftSurreal_le {ι : Type u_1} (f : ι → Surreal) :
    (⨅ (i : ι), leftSurreal (f i)).birthday ≤ ⨆ (i : ι), ↑(f i).birthday + 1
    source
    theorem Surreal.Cut.birthday_iSup_rightSurreal_le {ι : Type u_1} (f : ι → Surreal) :
    (⨆ (i : ι), rightSurreal (f i)).birthday ≤ ⨆ (i : ι), ↑(f i).birthday + 1
    source
    theorem Surreal.Cut.birthday_sInf_leftSurreal_le' (s : Set Surreal) [Small.{u, u + 1} ↑s] :
    (sInf (⇑leftSurreal '' s)).birthday ≤ ↑(sSup ((fun (x : Surreal) => x.birthday + 1) '' s))
    source
    theorem Surreal.Cut.birthday_sSup_rightSurreal_le' (s : Set Surreal) [Small.{u, u + 1} ↑s] :
    (sSup (⇑rightSurreal '' s)).birthday ≤ ↑(sSup ((fun (x : Surreal) => x.birthday + 1) '' s))
    source
    theorem Surreal.Cut.birthday_iInf_leftSurreal_le' {ι : Type u_1} (f : ι → Surreal) [Small.{u, u_1} ι] :
    (⨅ (i : ι), leftSurreal (f i)).birthday ≤ ↑(⨆ (i : ι), (f i).birthday + 1)
    source
    theorem Surreal.Cut.birthday_iSup_rightSurreal_le' {ι : Type u_1} (f : ι → Surreal) [Small.{u, u_1} ι] :
    (⨆ (i : ι), rightSurreal (f i)).birthday ≤ ↑(⨆ (i : ι), (f i).birthday + 1)
    source
    theorem Surreal.Cut.birthday_lt_sSup_birthday {a : Surreal} {s : Set Surreal} (ha : a ∈ s) :
    ↑a.birthday < sSup ((fun (x : Surreal) => ↑x.birthday + 1) '' s)
    source
    theorem Surreal.Cut.sSup_birthday_lt_top_iff {s : Set Surreal} :
    sSup ((fun (x : Surreal) => ↑x.birthday + 1) '' s) < ⊤ ↔ Small.{u, u + 1} ↑s
    source
    theorem Surreal.Cut.sSup_birthday_eq_top_iff {s : Set Surreal} :
    sSup ((fun (x : Surreal) => ↑x.birthday + 1) '' s) = ⊤ ↔ ¬Small.{u, u + 1} ↑s
    source
    @[simp]
    theorem Surreal.Cut.birthday_bot :
    ⊥.birthday = 0
    source
    @[simp]
    theorem Surreal.Cut.birthday_top :
    ⊤.birthday = 0
    source
    @[simp]
    theorem Surreal.Cut.birthday_neg (x : Cut) :
    (-x).birthday = x.birthday
    source
    @[simp]
    theorem Surreal.Cut.birthday_leftSurreal (x : Surreal) :
    (leftSurreal x).birthday = ↑x.birthday + 1
    source
    @[simp]
    theorem Surreal.Cut.birthday_rightSurreal (x : Surreal) :
    (rightSurreal x).birthday = ↑x.birthday + 1
    source
    theorem Surreal.Cut.exists_birthday_lt_of_mem_Ioo {x y z : Cut} (h : y ∈ Set.Ioo x z) :
    ∃ (a : Surreal), ↑a.birthday < y.birthday ∧ Fits a x z
    source
    theorem Surreal.Cut.birthday_iInf_le {ι : Type u_1} (f : ι → Cut) :
    (⨅ (i : ι), f i).birthday ≤ ⨆ (i : ι), (f i).birthday
    source
    theorem Surreal.Cut.birthday_iSup_le {ι : Type u_1} (f : ι → Cut) :
    (⨆ (i : ι), f i).birthday ≤ ⨆ (i : ι), (f i).birthday
    source
    theorem Surreal.Cut.birthday_sInf_le (s : Set Cut) :
    (sInf s).birthday ≤ sSup (birthday '' s)
    source
    theorem Surreal.Cut.birthday_sSup_le (s : Set Cut) :
    (sSup s).birthday ≤ sSup (birthday '' s)
    source
    theorem Surreal.Cut.birthday_simplestBtwn_le {x y : Cut} (h : x < y) :
    ↑(simplestBtwn h).birthday ≤ max x.birthday y.birthday
    source
    theorem Surreal.Cut.birthday_supLeft_le (x : IGame) :
    (supLeft x).birthday ≤ ↑x.birthday
    source
    theorem Surreal.Cut.birthday_infRight_le (x : IGame) :
    (infRight x).birthday ≤ ↑x.birthday
    source
    theorem Surreal.Cut.birthday_leftGame_le (x : Game) :
    (leftGame x).birthday ≤ ↑x.birthday + 1
    source
    theorem Surreal.Cut.birthday_rightGame_le (x : Game) :
    (rightGame x).birthday ≤ ↑x.birthday + 1
    source
    @[simp]
    theorem Surreal.birthday_toGame (x : Surreal) :
    (toGame x).birthday = x.birthday

    The smallest birthday among numeric games equivalent to a surreal, is also the smallest birthday among all games in general.