# Ordinals as games #

We define the canonical map Ordinal → SetTheory.PGame, where every ordinal is mapped to the game whose left set consists of all previous ordinals.

The map to surreals is defined in Ordinal.toSurreal.

# Main declarations #

• Ordinal.toPGame: The canonical map between ordinals and pre-games.
• Ordinal.toPGameEmbedding: The order embedding version of the previous map.
noncomputable def Ordinal.toPGame :

Converts an ordinal into the corresponding pre-game.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ordinal.toPGame_def (o : Ordinal.{u_1}) :
let_fun this := ; o.toPGame = SetTheory.PGame.mk () PEmpty.{u_1 + 1} (fun (x : ()) => (Ordinal.typein (fun (x x_1 : ()) => x < x_1) x).toPGame) PEmpty.elim
@[simp]
theorem Ordinal.toPGame_leftMoves (o : Ordinal.{u_1}) :
o.toPGame.LeftMoves = ()
@[simp]
theorem Ordinal.toPGame_rightMoves (o : Ordinal.{u_1}) :
o.toPGame.RightMoves = PEmpty.{u_1 + 1}
instance Ordinal.isEmpty_toPGame_rightMoves (o : Ordinal.{u_1}) :
IsEmpty o.toPGame.RightMoves
Equations
• =
noncomputable def Ordinal.toLeftMovesToPGame {o : Ordinal.{u_1}} :
() o.toPGame.LeftMoves

Converts an ordinal less than o into a move for the PGame corresponding to o, and vice versa.

Equations
• Ordinal.toLeftMovesToPGame = o.enumIsoOut.trans ()
Instances For
@[simp]
theorem Ordinal.toLeftMovesToPGame_symm_lt {o : Ordinal.{u_1}} (i : o.toPGame.LeftMoves) :
(Ordinal.toLeftMovesToPGame.symm i) < o
theorem Ordinal.toPGame_moveLeft_hEq {o : Ordinal.{u_1}} :
let_fun this := ; HEq o.toPGame.moveLeft fun (x : ()) => (Ordinal.typein (fun (x x_1 : ()) => x < x_1) x).toPGame
@[simp]
theorem Ordinal.toPGame_moveLeft' {o : Ordinal.{u_1}} (i : o.toPGame.LeftMoves) :
o.toPGame.moveLeft i = ((Ordinal.toLeftMovesToPGame.symm i)).toPGame
theorem Ordinal.toPGame_moveLeft {o : Ordinal.{u_1}} (i : ()) :
o.toPGame.moveLeft (Ordinal.toLeftMovesToPGame i) = (i).toPGame
noncomputable def Ordinal.zeroToPGameRelabelling :
().Relabelling 0

0.toPGame has the same moves as 0.

Equations
Instances For
noncomputable instance Ordinal.uniqueOneToPGameLeftMoves :
Unique ().LeftMoves
Equations
@[simp]
theorem Ordinal.one_toPGame_leftMoves_default_eq :
default = Ordinal.toLeftMovesToPGame 0,
@[simp]
theorem Ordinal.to_leftMoves_one_toPGame_symm (i : ().LeftMoves) :
Ordinal.toLeftMovesToPGame.symm i = 0,
theorem Ordinal.one_toPGame_moveLeft (x : ().LeftMoves) :
().moveLeft x =
noncomputable def Ordinal.oneToPGameRelabelling :
().Relabelling 1

1.toPGame has the same moves as 1.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ordinal.toPGame_lf {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) :
a.toPGame.LF b.toPGame
theorem Ordinal.toPGame_le {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a b) :
a.toPGame b.toPGame
theorem Ordinal.toPGame_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) :
a.toPGame < b.toPGame
@[simp]
theorem Ordinal.toPGame_lf_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
a.toPGame.LF b.toPGame a < b
@[simp]
theorem Ordinal.toPGame_le_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
a.toPGame b.toPGame a b
@[simp]
theorem Ordinal.toPGame_lt_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
a.toPGame < b.toPGame a < b
@[simp]
theorem Ordinal.toPGame_equiv_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
a.toPGame b.toPGame a = b
@[simp]
theorem Ordinal.toPGame_eq_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
a.toPGame = b.toPGame a = b
@[simp]
theorem Ordinal.toPGameEmbedding_apply :
∀ (a : Ordinal.{u}), Ordinal.toPGameEmbedding a = a.toPGame
noncomputable def Ordinal.toPGameEmbedding :

The order embedding version of toPGame.

Equations
Instances For
theorem Ordinal.toPGame_add (a : Ordinal.{u}) (b : Ordinal.{u}) :
a.toPGame + b.toPGame (a.nadd b).toPGame

The sum of ordinals as games corresponds to natural addition of ordinals.

@[simp]
theorem Ordinal.toPGame_add_mk' (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) :
a.toPGame + b.toPGame = (a.nadd b).toPGame