Documentation

Mathlib.SetTheory.Game.Ordinal

Ordinals as games #

We define the canonical map OrdinalSetTheory.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.toSurreal.

Main declarations #

Converts an ordinal into the corresponding pre-game.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Ordinal.toPGame_def (o : Ordinal.{u_1}) :
    let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1); Ordinal.toPGame o = SetTheory.PGame.mk (Quotient.out o).α PEmpty.{u_1 + 1} (fun x => Ordinal.toPGame (Ordinal.typein (fun x x_1 => x < x_1) x)) PEmpty.elim

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

    Instances For
      @[simp]
      theorem Ordinal.toLeftMovesToPGame_symm_lt {o : Ordinal.{u_1}} (i : SetTheory.PGame.LeftMoves (Ordinal.toPGame o)) :
      ↑(Ordinal.toLeftMovesToPGame.symm i) < o
      theorem Ordinal.toPGame_moveLeft_hEq {o : Ordinal.{u_1}} :
      let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1); HEq (SetTheory.PGame.moveLeft (Ordinal.toPGame o)) fun x => Ordinal.toPGame (Ordinal.typein (fun x x_1 => x < x_1) x)
      theorem Ordinal.toPGame_moveLeft {o : Ordinal.{u_1}} (i : ↑(Set.Iio o)) :
      SetTheory.PGame.moveLeft (Ordinal.toPGame o) (Ordinal.toLeftMovesToPGame i) = Ordinal.toPGame i

      0.to_pgame has the same moves as 0.

      Instances For
        @[simp]
        theorem Ordinal.one_toPGame_leftMoves_default_eq :
        default = Ordinal.toLeftMovesToPGame { val := 0, property := (_ : 0 Set.Iio 1) }
        @[simp]
        theorem Ordinal.to_leftMoves_one_toPGame_symm (i : SetTheory.PGame.LeftMoves (Ordinal.toPGame 1)) :
        Ordinal.toLeftMovesToPGame.symm i = { val := 0, property := (_ : 0 Set.Iio 1) }

        1.to_pgame has the same moves as 1.

        Instances For

          The order embedding version of toPGame.

          Instances For

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