mathlib documentation

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

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

Equations
@[protected, instance]
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]
@[simp]
theorem ordinal.to_pgame_lt_iff {a b : ordinal} :
@[simp]
@[simp]
theorem ordinal.to_pgame_eq_iff {a b : ordinal} :

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