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.

source

noncomputable def Ordinal.toPGame :

Ordinal.{u} → SetTheory.PGame

Converts an ordinal into the corresponding pre-game.

Equations

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

Instances For

source

theorem Ordinal.toPGame_def (o : Ordinal.{u_1}) :

let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1); Ordinal.toPGame o = SetTheory.PGame.mk (Quotient.out o).α PEmpty.{u_1 + 1} (fun x => Ordinal.toPGame (Ordinal.typein (fun x x_1 => x < x_1) x)) PEmpty.elim

source

@[simp]

theorem Ordinal.toPGame_leftMoves (o : Ordinal.{u_1}) :

SetTheory.PGame.LeftMoves (Ordinal.toPGame o) = (Quotient.out o).α

source

@[simp]

theorem Ordinal.toPGame_rightMoves (o : Ordinal.{u_1}) :

SetTheory.PGame.RightMoves (Ordinal.toPGame o) = PEmpty.{u_1 + 1}

source

instance Ordinal.isEmpty_zero_toPGame_leftMoves :

IsEmpty (SetTheory.PGame.LeftMoves (Ordinal.toPGame 0))

source

instance Ordinal.isEmpty_toPGame_rightMoves (o : Ordinal.{u_1}) :

IsEmpty (SetTheory.PGame.RightMoves (Ordinal.toPGame o))

source

noncomputable def Ordinal.toLeftMovesToPGame {o : Ordinal.{u_1}} :

↑(Set.Iio o) ≃ SetTheory.PGame.LeftMoves (Ordinal.toPGame o)

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

Instances For

source

@[simp]

theorem Ordinal.toLeftMovesToPGame_symm_lt {o : Ordinal.{u_1}} (i : SetTheory.PGame.LeftMoves (Ordinal.toPGame o)) :

↑(↑Ordinal.toLeftMovesToPGame.symm i) < o

source

theorem Ordinal.toPGame_moveLeft_hEq {o : Ordinal.{u_1}} :

let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1); HEq (SetTheory.PGame.moveLeft (Ordinal.toPGame o)) fun x => Ordinal.toPGame (Ordinal.typein (fun x x_1 => x < x_1) x)

source

@[simp]

theorem Ordinal.toPGame_moveLeft' {o : Ordinal.{u_1}} (i : SetTheory.PGame.LeftMoves (Ordinal.toPGame o)) :

SetTheory.PGame.moveLeft (Ordinal.toPGame o) i = Ordinal.toPGame ↑(↑Ordinal.toLeftMovesToPGame.symm i)

source

theorem Ordinal.toPGame_moveLeft {o : Ordinal.{u_1}} (i : ↑(Set.Iio o)) :

SetTheory.PGame.moveLeft (Ordinal.toPGame o) (↑Ordinal.toLeftMovesToPGame i) = Ordinal.toPGame ↑i

source

noncomputable def Ordinal.zeroToPgameRelabelling :

SetTheory.PGame.Relabelling (Ordinal.toPGame 0) 0

0.to_pgame has the same moves as 0.

Instances For

source

noncomputable instance Ordinal.uniqueOneToPgameLeftMoves :

Unique (SetTheory.PGame.LeftMoves (Ordinal.toPGame 1))

source

@[simp]

theorem Ordinal.one_toPGame_leftMoves_default_eq :

default = ↑Ordinal.toLeftMovesToPGame { val := 0, property := (_ : 0 ∈ Set.Iio 1) }

source

@[simp]

theorem Ordinal.to_leftMoves_one_toPGame_symm (i : SetTheory.PGame.LeftMoves (Ordinal.toPGame 1)) :

↑Ordinal.toLeftMovesToPGame.symm i = { val := 0, property := (_ : 0 ∈ Set.Iio 1) }

source

theorem Ordinal.one_toPGame_moveLeft (x : SetTheory.PGame.LeftMoves (Ordinal.toPGame 1)) :

SetTheory.PGame.moveLeft (Ordinal.toPGame 1) x = Ordinal.toPGame 0

source

noncomputable def Ordinal.oneToPGameRelabelling :

SetTheory.PGame.Relabelling (Ordinal.toPGame 1) 1

1.to_pgame has the same moves as 1.

Instances For

source

theorem Ordinal.toPGame_lf {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) :

SetTheory.PGame.LF (Ordinal.toPGame a) (Ordinal.toPGame b)

source

theorem Ordinal.toPGame_le {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a ≤ b) :

Ordinal.toPGame a ≤ Ordinal.toPGame b

source

theorem Ordinal.toPGame_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) :

Ordinal.toPGame a < Ordinal.toPGame b

source

theorem Ordinal.toPGame_nonneg (a : Ordinal.{u_1}) :

0 ≤ Ordinal.toPGame a

source

@[simp]

theorem Ordinal.toPGame_lf_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :

SetTheory.PGame.LF (Ordinal.toPGame a) (Ordinal.toPGame b) ↔ a < b

source

@[simp]

theorem Ordinal.toPGame_le_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :

Ordinal.toPGame a ≤ Ordinal.toPGame b ↔ a ≤ b

source

@[simp]

theorem Ordinal.toPGame_lt_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :

Ordinal.toPGame a < Ordinal.toPGame b ↔ a < b

source

@[simp]

theorem Ordinal.toPGame_equiv_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :

Ordinal.toPGame a ≈ Ordinal.toPGame b ↔ a = b

source

theorem Ordinal.toPGame_injective :

Function.Injective Ordinal.toPGame

source

@[simp]

theorem Ordinal.toPGame_eq_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :

Ordinal.toPGame a = Ordinal.toPGame b ↔ a = b

source

@[simp]

theorem Ordinal.toPGameEmbedding_apply :

∀ (a : Ordinal.{u}), ↑Ordinal.toPGameEmbedding a = Ordinal.toPGame a

source

noncomputable def Ordinal.toPGameEmbedding :

Ordinal.{u} ↪o SetTheory.PGame

The order embedding version of toPGame.

Instances For

source

theorem Ordinal.toPGame_add (a : Ordinal.{u}) (b : Ordinal.{u}) :

Ordinal.toPGame a + Ordinal.toPGame b ≈ Ordinal.toPGame (Ordinal.nadd a b)

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

source

@[simp]

theorem Ordinal.toPGame_add_mk' (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) :

Quotient.mk SetTheory.PGame.setoid (Ordinal.toPGame a) + Quotient.mk SetTheory.PGame.setoid (Ordinal.toPGame b) = Quotient.mk SetTheory.PGame.setoid (Ordinal.toPGame (Ordinal.nadd a b))