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
noncomputable def Ordinal.toPGame :
Ordinal.{u} → SetTheory.PGame

Converts an ordinal into the corresponding pre-game.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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
    source
    @[simp]
    theorem Ordinal.toPGame_leftMoves (o : Ordinal.{u_1}) :
    o.toPGame.LeftMoves = (Quotient.out o).α
    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.enumIsoOut.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}} :
      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
      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 :
          ∀ (a : Ordinal.{u}), Ordinal.toPGameEmbedding a = a.toPGame
          source
          noncomputable def Ordinal.toPGameEmbedding :
          Ordinal.{u} ↪o SetTheory.PGame

          The order embedding version of toPGame.

          Equations
          Instances For
            source
            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.

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