Documentation

LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Birthday.Basic

Birthday of a surreal number #

TODO: write a better docstring

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_ofNat (n : ℕ) [n.AtLeastTwo] :
    (OfNat.ofNat n).birthday = ↑n
    source
    @[simp]
    theorem Surreal.birthday_one :
    birthday 1 = 1
    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_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_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.

    source
    instance Surreal.small_subtype_birthday_le (o : NatOrdinal) :
    Small.{u, u + 1} { x : Surreal // x.birthday ≤ o }

    A variant of small_setOf_birthday_le in simp-normal form

    source
    instance Surreal.small_subtype_birthday_lt (o : NatOrdinal) :
    Small.{u, u + 1} { x : Surreal // x.birthday < o }

    A variant of small_setOf_birthday_lt in simp-normal form