# mathlibdocumentation

set_theory.game.ordinal

# Ordinals as games #

We define the canonical map ordinal → 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.to_surreal.

# Main declarations #

• ordinal.to_pgame: The canonical map between ordinals and pre-games.
• ordinal.to_pgame_embedding: The order embedding version of the previous map.

Converts an ordinal into the corresponding pre-game.

Equations
@[simp]
@[protected, instance]
@[protected, instance]

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

Equations
@[simp]
noncomputable def ordinal.zero_to_pgame_relabelling  :

0.to_pgame has the same moves as 0.

Equations
@[protected, instance]
Equations
@[simp]
noncomputable def ordinal.one_to_pgame_relabelling  :

1.to_pgame has the same moves as 1.

Equations
theorem ordinal.to_pgame_lf {a b : ordinal} (h : a < b) :
theorem ordinal.to_pgame_le {a b : ordinal} (h : a b) :
theorem ordinal.to_pgame_lt {a b : ordinal} (h : a < b) :
@[simp]
theorem ordinal.to_pgame_lf_iff {a b : ordinal} :
@[simp]
theorem ordinal.to_pgame_le_iff {a b : ordinal} :
a b
@[simp]
theorem ordinal.to_pgame_lt_iff {a b : ordinal} :
a < b
@[simp]
theorem ordinal.to_pgame_equiv_iff {a b : ordinal} :
a = b
@[simp]
theorem ordinal.to_pgame_eq_iff {a b : ordinal} :
a = b
@[simp]
noncomputable def ordinal.to_pgame_embedding  :

The order embedding version of to_pgame.

Equations

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

@[simp]