mathlib3 documentation

set_theory.game.ordinal

Ordinals as games #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.