# mathlibdocumentation

set_theory.game.ordinal

# Ordinals as games #

We define the canonical map ordinalpgame, 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 #

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]
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
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]