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 #

@[irreducible]

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 := ; o.toPGame = SetTheory.PGame.mk (Quotient.out o) PEmpty.{u_1 + 1} (fun (x : (Quotient.out o)) => (Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) x).toPGame) PEmpty.elim
    @[simp]
    theorem Ordinal.toPGame_leftMoves (o : Ordinal.{u_1}) :
    o.toPGame.LeftMoves = (Quotient.out o)
    @[simp]
    theorem Ordinal.toPGame_rightMoves (o : Ordinal.{u_1}) :
    o.toPGame.RightMoves = PEmpty.{u_1 + 1}
    instance Ordinal.isEmpty_toPGame_rightMoves (o : Ordinal.{u_1}) :
    IsEmpty o.toPGame.RightMoves
    Equations
    • =
    noncomputable def Ordinal.toLeftMovesToPGame {o : Ordinal.{u_1}} :
    (Set.Iio o) o.toPGame.LeftMoves

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

    Equations
    • Ordinal.toLeftMovesToPGame = o.enumIsoOut.trans (Equiv.cast )
    Instances For
      @[simp]
      theorem Ordinal.toLeftMovesToPGame_symm_lt {o : Ordinal.{u_1}} (i : o.toPGame.LeftMoves) :
      (Ordinal.toLeftMovesToPGame.symm i) < o
      theorem Ordinal.toPGame_moveLeft_hEq {o : Ordinal.{u_1}} :
      let_fun this := ; HEq o.toPGame.moveLeft fun (x : (Quotient.out o)) => (Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) x).toPGame
      @[simp]
      theorem Ordinal.toPGame_moveLeft' {o : Ordinal.{u_1}} (i : o.toPGame.LeftMoves) :
      o.toPGame.moveLeft i = ((Ordinal.toLeftMovesToPGame.symm i)).toPGame
      theorem Ordinal.toPGame_moveLeft {o : Ordinal.{u_1}} (i : (Set.Iio o)) :
      o.toPGame.moveLeft (Ordinal.toLeftMovesToPGame i) = (i).toPGame
      noncomputable def Ordinal.zeroToPGameRelabelling :
      (Ordinal.toPGame 0).Relabelling 0

      0.toPGame has the same moves as 0.

      Equations
      Instances For
        @[simp]
        theorem Ordinal.one_toPGame_leftMoves_default_eq :
        default = Ordinal.toLeftMovesToPGame 0,
        @[simp]
        theorem Ordinal.to_leftMoves_one_toPGame_symm (i : (Ordinal.toPGame 1).LeftMoves) :
        Ordinal.toLeftMovesToPGame.symm i = 0,
        noncomputable def Ordinal.oneToPGameRelabelling :
        (Ordinal.toPGame 1).Relabelling 1

        1.toPGame has the same moves as 1.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Ordinal.toPGame_lf {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) :
          a.toPGame.LF b.toPGame
          theorem Ordinal.toPGame_le {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a b) :
          a.toPGame b.toPGame
          theorem Ordinal.toPGame_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) :
          a.toPGame < b.toPGame
          @[simp]
          theorem Ordinal.toPGame_lf_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame.LF b.toPGame a < b
          @[simp]
          theorem Ordinal.toPGame_le_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame b.toPGame a b
          @[simp]
          theorem Ordinal.toPGame_lt_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame < b.toPGame a < b
          @[simp]
          theorem Ordinal.toPGame_equiv_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame b.toPGame a = b
          @[simp]
          theorem Ordinal.toPGame_eq_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame = b.toPGame a = b
          @[simp]
          theorem Ordinal.toPGameEmbedding_apply :
          ∀ (a : Ordinal.{u}), Ordinal.toPGameEmbedding a = a.toPGame

          The order embedding version of toPGame.

          Equations
          Instances For
            @[irreducible]
            theorem Ordinal.toPGame_add (a : Ordinal.{u}) (b : Ordinal.{u}) :
            a.toPGame + b.toPGame (a.nadd b).toPGame

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

            @[simp]
            theorem Ordinal.toPGame_add_mk' (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) :
            a.toPGame + b.toPGame = (a.nadd b).toPGame