Documentation

CombinatorialGames.Surreal.Ordinal

Ordinals as surreals #

We define the canonical map NatOrdinal → Surreal in terms of the map NatOrdinal.toIGame.

source
@[irreducible]
instance IGame.Numeric.toIGame (o : NatOrdinal) :
(NatOrdinal.toIGame o).Numeric

Ordinal games are numeric.

source
def NatOrdinal.toSurreal :
NatOrdinal ↪o Surreal

Converts an ordinal into the corresponding surreal.

Equations
Instances For
    source
    @[simp]
    theorem Surreal.mk_natOrdinal_toIGame (o : NatOrdinal) :
    mk (NatOrdinal.toIGame o) = NatOrdinal.toSurreal o
    source
    @[simp]
    theorem Surreal.toGame_toSurreal (o : NatOrdinal) :
    toGame (NatOrdinal.toSurreal o) = NatOrdinal.toGame o
    source
    theorem NatOrdinal.toSurreal_def (o : NatOrdinal) :
    toSurreal o = Surreal.ofSets (⇑toSurreal '' Set.Iio o) ∅ ⋯
    source
    @[simp]
    theorem NatOrdinal.toSurreal_zero :
    toSurreal 0 = 0
    source
    @[simp]
    theorem NatOrdinal.toSurreal_one :
    toSurreal 1 = 1
    source
    @[simp]
    theorem NatOrdinal.toSurreal_nonneg (a : NatOrdinal) :
    0 ≤ toGame a
    source
    @[simp]
    theorem NatOrdinal.toSurreal_add (a b : NatOrdinal) :
    toSurreal (a + b) = toSurreal a + toSurreal b
    source
    @[simp]
    theorem NatOrdinal.toSurreal_mul (a b : NatOrdinal) :
    toSurreal (a * b) = toSurreal a * toSurreal b
    source
    def NatOrdinal.toSurrealRingHom :
    NatOrdinal →+*o Surreal

    NatOrdinal.toGame as an OrderRingHom.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem NatOrdinal.toSurrealRingHom_toFun (a : NatOrdinal) :
      toSurrealRingHom a = toSurreal a
      source
      @[simp]
      theorem NatOrdinal.toSurreal_natCast (n : ℕ) :
      toSurreal ↑n = ↑n