Documentation

CombinatorialGames.Surreal.Ordinal

Ordinals as surreals #

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

@[irreducible]

instance IGame.Numeric.toIGame (o : NatOrdinal) :

(NatOrdinal.toIGame o).Numeric

Ordinal games are numeric.

def NatOrdinal.toSurreal :

NatOrdinal ↪o Surreal

Converts an ordinal into the corresponding surreal.

Equations

NatOrdinal.toSurreal = OrderEmbedding.ofStrictMono (fun (o : NatOrdinal) => Surreal.mk (NatOrdinal.toIGame o)) NatOrdinal.toSurreal._proof_1

Instances For

instance NatOrdinal.instCoeSurreal :

Coe NatOrdinal Surreal

Equations

NatOrdinal.instCoeSurreal = { coe := fun (x : NatOrdinal) => NatOrdinal.toSurreal x }

@[simp]

theorem Surreal.mk_natOrdinal_toIGame (o : NatOrdinal) :

mk (NatOrdinal.toIGame o) = NatOrdinal.toSurreal o

@[simp]

theorem Surreal.toGame_toSurreal (o : NatOrdinal) :

toGame (NatOrdinal.toSurreal o) = NatOrdinal.toGame o

theorem NatOrdinal.toSurreal_def (o : NatOrdinal) :

toSurreal o = !{⇑toSurreal '' Set.Iio o | ∅}

@[simp]

theorem NatOrdinal.toSurreal_zero :

toSurreal 0 = 0

@[simp]

theorem NatOrdinal.toSurreal_one :

toSurreal 1 = 1

theorem NatOrdinal.toSurreal_nonneg (a : NatOrdinal) :

@[simp]

theorem NatOrdinal.toSurreal_add (a b : NatOrdinal) :

toSurreal (a + b) = toSurreal a + toSurreal b

@[simp]

theorem NatOrdinal.toSurreal_mul (a b : NatOrdinal) :

toSurreal (a * b) = toSurreal a * toSurreal b

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

@[simp]

theorem NatOrdinal.toSurrealRingHom_toFun (a : NatOrdinal) :

toSurrealRingHom a = toSurreal a

@[simp]

theorem NatOrdinal.toSurreal_natCast (n : ℕ) :

toSurreal ↑n = ↑n