Documentation

Mathlib.SetTheory.Game.Ordinal

Ordinals as games #

We define the canonical map Ordinal → SetTheory.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 #

source
@[irreducible]
noncomputable def Ordinal.toPGame (o : Ordinal.{u}) :
SetTheory.PGame

Converts an ordinal into the corresponding pre-game.

Equations
Instances For
    source
    theorem Ordinal.toPGame_def (o : Ordinal.{u_1}) :
    o.toPGame = SetTheory.PGame.mk o.toType PEmpty.{u_1 + 1} (fun (x : o.toType) => (↑(o.enumIsoToType.symm x)).toPGame) PEmpty.elim
    source
    @[simp]
    theorem Ordinal.toPGame_leftMoves (o : Ordinal.{u_1}) :
    o.toPGame.LeftMoves = o.toType
    source
    @[simp]
    theorem Ordinal.toPGame_rightMoves (o : Ordinal.{u_1}) :
    o.toPGame.RightMoves = PEmpty.{u_1 + 1}
    source
    instance Ordinal.isEmpty_zero_toPGame_leftMoves :
    IsEmpty (Ordinal.toPGame 0).LeftMoves
    Equations
    source
    instance Ordinal.isEmpty_toPGame_rightMoves (o : Ordinal.{u_1}) :
    IsEmpty o.toPGame.RightMoves
    Equations
    • ⋯ = ⋯
    source
    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.enumIsoToType.trans (Equiv.cast ⋯)
    Instances For
      source
      @[simp]
      theorem Ordinal.toLeftMovesToPGame_symm_lt {o : Ordinal.{u_1}} (i : o.toPGame.LeftMoves) :
      ↑(Ordinal.toLeftMovesToPGame.symm i) < o
      source
      theorem Ordinal.toPGame_moveLeft_hEq {o : Ordinal.{u_1}} :
      HEq o.toPGame.moveLeft fun (x : o.toType) => (↑(o.enumIsoToType.symm x)).toPGame
      source
      @[simp]
      theorem Ordinal.toPGame_moveLeft' {o : Ordinal.{u_1}} (i : o.toPGame.LeftMoves) :
      o.toPGame.moveLeft i = (↑(Ordinal.toLeftMovesToPGame.symm i)).toPGame
      source
      theorem Ordinal.toPGame_moveLeft {o : Ordinal.{u_1}} (i : ↑(Set.Iio o)) :
      o.toPGame.moveLeft (Ordinal.toLeftMovesToPGame i) = (↑i).toPGame
      source
      noncomputable def Ordinal.zeroToPGameRelabelling :
      (Ordinal.toPGame 0).Relabelling 0

      0.toPGame has the same moves as 0.

      Equations
      Instances For
        source
        noncomputable instance Ordinal.uniqueOneToPGameLeftMoves :
        Unique (Ordinal.toPGame 1).LeftMoves
        Equations
        source
        @[simp]
        theorem Ordinal.one_toPGame_leftMoves_default_eq :
        default = Ordinal.toLeftMovesToPGame ⟨0, ⋯⟩
        source
        @[simp]
        theorem Ordinal.to_leftMoves_one_toPGame_symm (i : (Ordinal.toPGame 1).LeftMoves) :
        Ordinal.toLeftMovesToPGame.symm i = ⟨0, ⋯⟩
        source
        theorem Ordinal.one_toPGame_moveLeft (x : (Ordinal.toPGame 1).LeftMoves) :
        (Ordinal.toPGame 1).moveLeft x = Ordinal.toPGame 0
        source
        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
          source
          theorem Ordinal.toPGame_lf {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) :
          a.toPGame.LF b.toPGame
          source
          theorem Ordinal.toPGame_le {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a ≤ b) :
          a.toPGame ≤ b.toPGame
          source
          theorem Ordinal.toPGame_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) :
          a.toPGame < b.toPGame
          source
          theorem Ordinal.toPGame_nonneg (a : Ordinal.{u_1}) :
          0 ≤ a.toPGame
          source
          @[simp]
          theorem Ordinal.toPGame_lf_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame.LF b.toPGame ↔ a < b
          source
          @[simp]
          theorem Ordinal.toPGame_le_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame ≤ b.toPGame ↔ a ≤ b
          source
          @[simp]
          theorem Ordinal.toPGame_lt_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame < b.toPGame ↔ a < b
          source
          @[simp]
          theorem Ordinal.toPGame_equiv_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame ≈ b.toPGame ↔ a = b
          source
          theorem Ordinal.toPGame_injective :
          Function.Injective Ordinal.toPGame
          source
          @[simp]
          theorem Ordinal.toPGame_eq_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
          a.toPGame = b.toPGame ↔ a = b
          source
          @[simp]
          theorem Ordinal.toPGameEmbedding_apply (o : Ordinal.{u}) :
          Ordinal.toPGameEmbedding o = o.toPGame
          source
          noncomputable def Ordinal.toPGameEmbedding :
          Ordinal.{u} ↪o SetTheory.PGame

          The order embedding version of toPGame.

          Equations
          Instances For
            source
            @[reducible, inline]
            noncomputable abbrev Ordinal.toGame (o : Ordinal.{u_1}) :
            SetTheory.Game

            Converts an ordinal into the corresponding game.

            Equations
            • o.toGame = ⟦o.toPGame⟧
            Instances For
              source
              @[irreducible]
              theorem Ordinal.toPGame_nadd (a : Ordinal.{u}) (b : Ordinal.{u}) :
              (a.nadd b).toPGame ≈ a.toPGame + b.toPGame

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

              source
              theorem Ordinal.toGame_nadd (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) :
              (a.nadd b).toGame = a.toGame + b.toGame
              source
              @[irreducible]
              theorem Ordinal.toPGame_nmul (a : Ordinal.{u}) (b : Ordinal.{u}) :
              (a.nmul b).toPGame ≈ a.toPGame * b.toPGame

              The natural multiplication of ordinals corresponds to their product as pre-games.

              source
              theorem Ordinal.toGame_nmul (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) :
              (a.nmul b).toGame = ⟦a.toPGame * b.toPGame⟧