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 "No deprecation message was provided." (since := "2024-09-22")]

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 (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) :

↑(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 = (↑(toLeftMovesToPGame.symm i)).toPGame

source

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

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

source

noncomputable def Ordinal.zeroToPGameRelabelling :

(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 :

toPGame 0 ≈ 0

source

noncomputable instance Ordinal.uniqueOneToPGameLeftMoves :

Unique (toPGame 1).LeftMoves

Equations

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

source

@[simp]

theorem Ordinal.one_toPGame_leftMoves_default_eq :

default = toLeftMovesToPGame ⟨0, ⋯⟩

source

@[simp]

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

toLeftMovesToPGame.symm i = ⟨0, ⋯⟩

source

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

(toPGame 1).moveLeft x = toPGame 0

source

noncomputable def Ordinal.oneToPGameRelabelling :

(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 :

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 toPGame

source

@[simp]

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

a.toPGame = b.toPGame ↔ a = b

source

@[deprecated Ordinal.toPGame_inj (since := "2024-12-29")]

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

a.toPGame = b.toPGame ↔ a = b

Alias of Ordinal.toPGame_inj.

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}) :

toPGameEmbedding o = o.toPGame

source

noncomputable def Ordinal.toGame :

Ordinal.{u} ↪o SetTheory.Game

Converts an ordinal into the corresponding game.

Equations

Ordinal.toGame = { toFun := fun (o : Ordinal.{?u.10}) => ⟦o.toPGame⟧, inj' := Ordinal.toGame.proof_1, map_rel_iff' := ⋯ }

Instances For

source

@[simp]

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

⟦o.toPGame⟧ = toGame o

source

@[deprecated Ordinal.toGame (since := "2024-11-23")]

def Ordinal.toGameEmbedding :

Ordinal.{u} ↪o SetTheory.Game

Alias of Ordinal.toGame.

Converts an ordinal into the corresponding game.

Equations

Ordinal.toGameEmbedding = Ordinal.toGame

Instances For

source

@[simp]

theorem Ordinal.toGame_zero :

toGame 0 = 0

source

@[simp]

theorem Ordinal.toGame_one :

toGame 1 = 1

source

theorem Ordinal.toGame_injective :

Function.Injective ⇑toGame

source

@[simp]

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

(toGame a).LF (toGame b) ↔ a < b

source

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

toGame a ≤ toGame b ↔ a ≤ b

source

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

toGame a < toGame b ↔ a < b

source

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

toGame a = toGame b ↔ a = b

source

@[deprecated Ordinal.toGame_inj (since := "2024-12-29")]

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

toGame a = toGame b ↔ a = b

Alias of Ordinal.toGame_inj.

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}) :

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

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}) :

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

source

@[simp]

theorem Ordinal.toGame_natCast (n : ℕ) :

toGame ↑n = ↑n

source

theorem Ordinal.toPGame_natCast (n : ℕ) :

(↑n).toPGame ≈ ↑n

Documentation

Mathlib.SetTheory.Game.Ordinal

Ordinals as games #

Main declarations #