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

@[irreducible]

noncomputable def Ordinal.toPGame (o : Ordinal.{u}) :

SetTheory.PGame

Converts an ordinal into the corresponding pre-game.

Equations

o.toPGame = SetTheory.PGame.mk o.toType PEmpty.{?u.2 + 1} (fun (x : o.toType) => (↑(o.enumIsoToType.symm x)).toPGame) PEmpty.elim

Instances For

source

@[deprecated]

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

o.toPGame = SetTheory.PGame.mk o.toType PEmpty.{u_1 + 1} (fun (x : o.toType) => (↑(o.enumIsoToType.symm x)).toPGame) PEmpty.elim

source

@[simp]

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

o.toPGame.LeftMoves = o.toType

source

@[simp]

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

o.toPGame.RightMoves = PEmpty.{u_1 + 1}

source

instance Ordinal.isEmpty_zero_toPGame_leftMoves :

IsEmpty (Ordinal.toPGame 0).LeftMoves

source

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

IsEmpty o.toPGame.RightMoves

source

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

↑(Set.Iio o) ≃ 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.enumIsoToType.trans (Equiv.cast ⋯)

Instances For

source

@[simp]

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

↑(Ordinal.toLeftMovesToPGame.symm i) < o

source

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

HEq o.toPGame.moveLeft fun (x : o.toType) => (↑(o.enumIsoToType.symm x)).toPGame

source

@[simp]

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

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

source

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

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

source

noncomputable def Ordinal.zeroToPGameRelabelling :

(Ordinal.toPGame 0).Relabelling 0

0.toPGame has the same moves as 0.

Equations

Ordinal.zeroToPGameRelabelling = SetTheory.PGame.Relabelling.isEmpty (Ordinal.toPGame 0)

Instances For

source

theorem Ordinal.toPGame_zero :

Ordinal.toPGame 0 ≈ 0

source

noncomputable instance Ordinal.uniqueOneToPGameLeftMoves :

Unique (Ordinal.toPGame 1).LeftMoves

Equations

Ordinal.uniqueOneToPGameLeftMoves = (Equiv.cast Ordinal.uniqueOneToPGameLeftMoves.proof_1).unique

source

@[simp]

theorem Ordinal.one_toPGame_leftMoves_default_eq :

default = Ordinal.toLeftMovesToPGame ⟨0, ⋯⟩

source

@[simp]

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

Ordinal.toLeftMovesToPGame.symm i = ⟨0, ⋯⟩

source

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

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

source

noncomputable def Ordinal.oneToPGameRelabelling :

(Ordinal.toPGame 1).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

source

theorem Ordinal.toPGame_one :

Ordinal.toPGame 1 ≈ 1

source

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

a.toPGame.LF b.toPGame

source

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

a.toPGame ≤ b.toPGame

source

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

a.toPGame < b.toPGame

source

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

0 ≤ a.toPGame

source

@[simp]

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

a.toPGame.LF b.toPGame ↔ a < b

source

@[simp]

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

a.toPGame ≤ b.toPGame ↔ a ≤ b

source

@[simp]

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

a.toPGame < b.toPGame ↔ a < b

source

@[simp]

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

a.toPGame ≈ b.toPGame ↔ a = b

source

theorem Ordinal.toPGame_injective :

Function.Injective Ordinal.toPGame

source

@[simp]

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

a.toPGame = b.toPGame ↔ a = b

source

noncomputable def Ordinal.toPGameEmbedding :

Ordinal.{u} ↪o SetTheory.PGame

The order embedding version of toPGame.

Equations

Ordinal.toPGameEmbedding = { toFun := Ordinal.toPGame, inj' := Ordinal.toPGame_injective, map_rel_iff' := @Ordinal.toPGame_le_iff }

Instances For

source

@[simp]

theorem Ordinal.toPGameEmbedding_apply (o : Ordinal.{u}) :

Ordinal.toPGameEmbedding o = o.toPGame

source

@[reducible, inline]

noncomputable abbrev Ordinal.toGame (o : Ordinal.{u_1}) :

SetTheory.Game

Converts an ordinal into the corresponding game.

Equations

o.toGame = ⟦o.toPGame⟧

Instances For

source

noncomputable def Ordinal.toGameEmbedding :

Ordinal.{u} ↪o SetTheory.Game

The order embedding version of toGame.

Equations

Ordinal.toGameEmbedding = { toFun := Ordinal.toGame, inj' := Ordinal.toGameEmbedding.proof_1, map_rel_iff' := ⋯ }

Instances For

source

@[simp]

theorem Ordinal.toGameEmbedding_apply (o : Ordinal.{u}) :

Ordinal.toGameEmbedding o = o.toGame

source

@[simp]

theorem Ordinal.toGame_zero :

Ordinal.toGame 0 = 0

source

@[simp]

theorem Ordinal.toGame_one :

Ordinal.toGame 1 = 1

source

theorem Ordinal.toGame_injective :

Function.Injective Ordinal.toGame

source

@[simp]

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

a.toGame.LF b.toGame ↔ a < b

source

@[simp]

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

a.toGame ≤ b.toGame ↔ a ≤ b

source

@[simp]

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

a.toGame < b.toGame ↔ a < b

source

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

a.toGame = b.toGame ↔ a = b

source

@[irreducible]

theorem Ordinal.toPGame_nadd (a b : Ordinal.{u_1}) :

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

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

source

theorem Ordinal.toGame_nadd (a b : Ordinal.{u_1}) :

(a.nadd b).toGame = a.toGame + b.toGame

source

@[irreducible]

theorem Ordinal.toPGame_nmul (a b : Ordinal.{u_1}) :

(a.nmul b).toPGame ≈ a.toPGame * b.toPGame

The natural multiplication of ordinals corresponds to their product as pre-games.

source

theorem Ordinal.toGame_nmul (a b : Ordinal.{u_1}) :

(a.nmul b).toGame = ⟦a.toPGame * b.toPGame⟧

source

@[simp]

theorem Ordinal.toGame_natCast (n : ℕ) :

(↑n).toGame = ↑n

source

theorem Ordinal.toPGame_natCast (n : ℕ) :

(↑n).toPGame ≈ ↑n

Documentation

Mathlib.SetTheory.Game.Ordinal

Ordinals as games #

Main declarations #