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
    @[deprecated]
    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
        theorem Ordinal.toPGame_zero :
        Ordinal.toPGame 0 ≈ 0
        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_one :
          Ordinal.toPGame 1 ≈ 1
          source
          theorem Ordinal.toPGame_lf {a b : Ordinal.{u_1}} (h : a < b) :
          a.toPGame.LF b.toPGame
          source
          theorem Ordinal.toPGame_le {a b : Ordinal.{u_1}} (h : a ≤ b) :
          a.toPGame ≤ b.toPGame
          source
          theorem Ordinal.toPGame_lt {a 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 b : Ordinal.{u_1}} :
          a.toPGame.LF b.toPGame ↔ a < b
          source
          @[simp]
          theorem Ordinal.toPGame_le_iff {a b : Ordinal.{u_1}} :
          a.toPGame ≤ b.toPGame ↔ a ≤ b
          source
          @[simp]
          theorem Ordinal.toPGame_lt_iff {a b : Ordinal.{u_1}} :
          a.toPGame < b.toPGame ↔ a < b
          source
          @[simp]
          theorem Ordinal.toPGame_equiv_iff {a 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 b : Ordinal.{u_1}} :
          a.toPGame = b.toPGame ↔ a = b
          source
          noncomputable def Ordinal.toPGameEmbedding :
          Ordinal.{u} ↪o SetTheory.PGame

          The order embedding version of toPGame.

          Equations
          Instances For
            source
            @[simp]
            theorem Ordinal.toPGameEmbedding_apply (o : Ordinal.{u}) :
            Ordinal.toPGameEmbedding o = o.toPGame
            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
              noncomputable def Ordinal.toGameEmbedding :
              Ordinal.{u} ↪o SetTheory.Game

              The order embedding version of toGame.

              Equations
              Instances For
                source
                @[simp]
                theorem Ordinal.toGameEmbedding_apply (o : Ordinal.{u}) :
                Ordinal.toGameEmbedding o = o.toGame
                source
                @[simp]
                theorem Ordinal.toGame_zero :
                Ordinal.toGame 0 = 0
                source
                @[simp]
                theorem Ordinal.toGame_one :
                Ordinal.toGame 1 = 1
                source
                theorem Ordinal.toGame_injective :
                Function.Injective Ordinal.toGame
                source
                @[simp]
                theorem Ordinal.toGame_lf_iff {a b : Ordinal.{u_1}} :
                a.toGame.LF b.toGame ↔ a < b
                source
                @[simp]
                theorem Ordinal.toGame_le_iff {a b : Ordinal.{u_1}} :
                a.toGame ≤ b.toGame ↔ a ≤ b
                source
                @[simp]
                theorem Ordinal.toGame_lt_iff {a b : Ordinal.{u_1}} :
                a.toGame < b.toGame ↔ a < b
                source
                theorem Ordinal.toGame_eq_iff {a b : Ordinal.{u_1}} :
                a.toGame = b.toGame ↔ a = b
                source
                @[irreducible]
                theorem Ordinal.toPGame_nadd (a b : Ordinal.{u_1}) :
                (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 b : Ordinal.{u_1}) :
                (a.nadd b).toGame = a.toGame + b.toGame
                source
                @[irreducible]
                theorem Ordinal.toPGame_nmul (a b : Ordinal.{u_1}) :
                (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 b : Ordinal.{u_1}) :
                (a.nmul b).toGame = ⟦a.toPGame * b.toPGame⟧
                source
                @[simp]
                theorem Ordinal.toGame_natCast (n : ℕ) :
                (↑n).toGame = ↑n
                source
                theorem Ordinal.toPGame_natCast (n : ℕ) :
                (↑n).toPGame ≈ ↑n