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
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
Main declarations #
Converts an ordinal into the corresponding pre-game.
Converts an ordinal less than
o into a move for the
pgame corresponding to
o, and vice
0.to_pgame has the same moves as
1.to_pgame has the same moves as
The order embedding version of
The sum of ordinals as games corresponds to natural addition of ordinals.