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
    @[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.birthday_le {x y : IGame} [x.Numeric] (h : x.Fits y) :
    (Game.mk y).birthday ≤ (Surreal.mk x).birthday
    source
    theorem IGame.Fits.birthday_lt {x y : IGame} [x.Numeric] (h : x.Fits y) (he : ¬x ≈ y) :
    (Game.mk y).birthday < (Surreal.mk x).birthday
    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
    theorem Surreal.birthday_toGame_le (x : Surreal) :
    (toGame x).birthday ≤ x.birthday

    The birthday of a surreal number is at least the birthday of the corresponding game.

    source
    instance Surreal.small_setOf_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_setOf_birthday_lt (o : NatOrdinal) :
    Small.{u, u + 1} ↑{x : Surreal | x.birthday < o}

    Surreals with a bounded birthday form a small set.