Documentation

CombinatorialGames.Surreal.Birthday.Basic

Birthdays of surreals #

We define the birthday of a surreal number as the smallest birthday of all numeric pre-games equivalent to it.

The numeric condition can be removed to yield an equivalent definition, but that is proved in CombinatorialGames.Surreal.Birthday.Cut.

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

The birthday of a surreal number is defined as the least birthday among all numeric pre-games that define it.

The numeric condition can be removed, see Surreal.birthday_toGame.

Equations
Instances For
    source
    theorem Surreal.birthday_eq_iGameBirthday (x : Surreal) :
    ∃ (y : IGame) (x_1 : y.Numeric), mk y = x ∧ y.birthday = x.birthday
    source
    theorem Surreal.birthday_mk_le (x : IGame) [x.Numeric] :
    (mk x).birthday ≤ x.birthday
    source
    theorem Surreal.birthday_toGame_le (x : Surreal) :
    (toGame x).birthday ≤ x.birthday

    See Surreal.birthday_toGame for the equality.

    source
    @[simp]
    theorem Surreal.birthday_zero :
    birthday 0 = 0
    source
    @[simp]
    theorem Surreal.birthday_eq_zero {x : Surreal} :
    x.birthday = 0 ↔ x = 0
    source
    @[simp]
    theorem Surreal.birthday_neg (x : Surreal) :
    (-x).birthday = x.birthday
    source
    theorem Surreal.le_toSurreal_birthday (x : Surreal) :
    x ≤ NatOrdinal.toSurreal x.birthday
    source
    theorem Surreal.neg_toSurreal_birthday_le (x : Surreal) :
    -NatOrdinal.toSurreal x.birthday ≤ x
    source
    @[simp]
    theorem Surreal.birthday_toSurreal (o : NatOrdinal) :
    (NatOrdinal.toSurreal o).birthday = o
    source
    @[simp]
    theorem Surreal.birthday_natCast (n : ℕ) :
    (↑n).birthday = ↑n
    source
    @[simp]
    theorem Surreal.birthday_intCast (n : ℤ) :
    (↑n).birthday = ↑n.natAbs
    source
    @[simp]
    theorem Surreal.birthday_ofNat (n : ℕ) [n.AtLeastTwo] :
    (OfNat.ofNat n).birthday = ↑n
    source
    @[simp]
    theorem Surreal.birthday_one :
    birthday 1 = 1
    source
    theorem IGame.Fits.gameBirthday_le {x y : IGame} [x.Numeric] (h : x.Fits y) :
    (Game.mk y).birthday ≤ (Surreal.mk x).birthday
    source
    theorem IGame.Fits.gameBirthday_lt {x y : IGame} [x.Numeric] (h : x.Fits y) (he : ¬x ≈ y) :
    (Game.mk y).birthday < (Surreal.mk x).birthday
    source
    theorem IGame.Fits.surrealBirthday_le {x y : IGame} [x.Numeric] [y.Numeric] (h : x.Fits y) :
    (Surreal.mk y).birthday ≤ (Surreal.mk x).birthday
    source
    theorem IGame.Fits.surrealBirthday_lt {x y : IGame} [x.Numeric] [y.Numeric] (h : x.Fits y) (he : ¬x ≈ y) :
    (Surreal.mk y).birthday < (Surreal.mk x).birthday
    source
    theorem Surreal.birthday_ofSets_le_of_btwn {s t : Set Surreal} {z : Surreal} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} (hL : ∀ x ∈ s, x < z) (hR : ∀ y ∈ t, z < y) :
    !{s | t}.birthday ≤ z.birthday
    source
    theorem Surreal.birthday_ofSets_lt_of_btwn {s t : Set Surreal} {z : Surreal} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} (hL : ∀ x ∈ s, x < z) (hR : ∀ y ∈ t, z < y) (h : !{s | t} ≠ z) :
    !{s | t}.birthday < z.birthday
    source
    theorem Surreal.ofSets_eq_of_forall_birthday_le {s t : Set Surreal} {z : Surreal} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} (hL : ∀ x ∈ s, x < z) (hR : ∀ y ∈ t, z < y) (h : ∀ (w : Surreal), (∀ x ∈ s, x < w) → (∀ y ∈ t, w < y) → z.birthday ≤ w.birthday) :
    !{s | t} = z
    source
    theorem Surreal.birthday_ofSets_le {s t : Set Surreal} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} :
    !{s | t}.birthday ≤ max (sSup (Order.succ ∘ birthday '' s)) (sSup (Order.succ ∘ birthday '' t))
    source
    theorem Surreal.birthday_ofSets_singleton_lt_of_birthday_eq {o : NatOrdinal} {x y : Surreal} (hx : x.birthday = o) (hy : y.birthday = o) (hxy : x < y) :
    !{{x} | {y}}.birthday < o
    source
    theorem Surreal.birthday_add_le (x y : Surreal) :
    (x + y).birthday ≤ x.birthday + y.birthday
    source
    theorem Surreal.birthday_sub_le (x y : Surreal) :
    (x - y).birthday ≤ x.birthday + y.birthday
    source
    theorem Surreal.birthday_eq_one {x : Surreal} :
    x.birthday = 1 ↔ x = 1 ∨ x = -1
    source
    theorem Surreal.birthday_le_one {x : Surreal} :
    x.birthday ≤ 1 ↔ x = 0 ∨ x = 1 ∨ x = -1
    source
    instance Surreal.small_setOfPred_birthday_le (o : NatOrdinal) :
    Small.{u, u + 1} ↑{x : Surreal | x.birthday ≤ o}

    Surreals with a bounded birthday form a small set.

    source
    instance Surreal.small_setOfPred_birthday_lt (o : NatOrdinal) :
    Small.{u, u + 1} ↑{x : Surreal | x.birthday < o}

    Surreals with a bounded birthday form a small set.