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.

noncomputable 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

@[implicit_reducible]

noncomputable 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) : 0 ≤ toGame a

@[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

noncomputable def NatOrdinal.toSurrealRingHom : NatOrdinal →+*o Surreal

NatOrdinal.toGame as an OrderRingHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NatOrdinal.toSurrealRingHom_toFun (a : NatOrdinal) : toSurrealRingHom a = toSurreal a

@[simp]

theorem NatOrdinal.toSurreal_natCast (n : ℕ) : toSurreal ↑n = ↑n