Documentation

Mathlib.SetTheory.Game.Birthday

Birthdays of games #

The birthday of a game is an ordinal that represents at which "step" the game was constructed. We define it recursively as the least ordinal larger than the birthdays of its left and right games. We prove the basic properties about these.

Main declarations #

Todo #

source
noncomputable def SetTheory.PGame.birthday :
SetTheory.PGame → Ordinal.{u}

The birthday of a pre-game is inductively defined as the least strict upper bound of the birthdays of its left and right games. It may be thought as the "step" in which a certain game is constructed.

Equations
Instances For
    source
    theorem SetTheory.PGame.birthday_def (x : SetTheory.PGame) :
    x.birthday = max (Ordinal.lsub fun (i : x.LeftMoves) => (x.moveLeft i).birthday) (Ordinal.lsub fun (i : x.RightMoves) => (x.moveRight i).birthday)
    source
    theorem SetTheory.PGame.birthday_moveLeft_lt {x : SetTheory.PGame} (i : x.LeftMoves) :
    (x.moveLeft i).birthday < x.birthday
    source
    theorem SetTheory.PGame.birthday_moveRight_lt {x : SetTheory.PGame} (i : x.RightMoves) :
    (x.moveRight i).birthday < x.birthday
    source
    theorem SetTheory.PGame.lt_birthday_iff {x : SetTheory.PGame} {o : Ordinal.{u_1}} :
    o < x.birthday ↔ (∃ (i : x.LeftMoves), o ≤ (x.moveLeft i).birthday) ∨ ∃ (i : x.RightMoves), o ≤ (x.moveRight i).birthday
    source
    @[irreducible]
    theorem SetTheory.PGame.Relabelling.birthday_congr {x : SetTheory.PGame} {y : SetTheory.PGame} :
    x.Relabelling y → x.birthday = y.birthday
    source
    @[simp]
    theorem SetTheory.PGame.birthday_eq_zero {x : SetTheory.PGame} :
    x.birthday = 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves
    source
    @[simp]
    theorem SetTheory.PGame.birthday_zero :
    SetTheory.PGame.birthday 0 = 0
    source
    @[simp]
    theorem SetTheory.PGame.birthday_one :
    SetTheory.PGame.birthday 1 = 1
    source
    @[simp]
    theorem SetTheory.PGame.birthday_star :
    SetTheory.PGame.star.birthday = 1
    source
    @[simp]
    theorem SetTheory.PGame.neg_birthday (x : SetTheory.PGame) :
    (-x).birthday = x.birthday
    source
    @[simp]
    theorem SetTheory.PGame.toPGame_birthday (o : Ordinal.{u_1}) :
    o.toPGame.birthday = o
    source
    theorem SetTheory.PGame.le_birthday (x : SetTheory.PGame) :
    x ≤ x.birthday.toPGame
    source
    theorem SetTheory.PGame.neg_birthday_le (x : SetTheory.PGame) :
    -x.birthday.toPGame ≤ x
    source
    @[simp, irreducible]
    theorem SetTheory.PGame.birthday_add (x : SetTheory.PGame) (y : SetTheory.PGame) :
    (x + y).birthday = x.birthday.nadd y.birthday
    source
    theorem SetTheory.PGame.birthday_add_zero (a : SetTheory.PGame) :
    (a + 0).birthday = a.birthday
    source
    theorem SetTheory.PGame.birthday_zero_add (a : SetTheory.PGame) :
    (0 + a).birthday = a.birthday
    source
    theorem SetTheory.PGame.birthday_add_one (a : SetTheory.PGame) :
    (a + 1).birthday = Order.succ a.birthday
    source
    theorem SetTheory.PGame.birthday_one_add (a : SetTheory.PGame) :
    (1 + a).birthday = Order.succ a.birthday
    source
    @[simp]
    theorem SetTheory.PGame.birthday_natCast (n : ℕ) :
    (↑n).birthday = ↑n
    source
    @[deprecated SetTheory.PGame.birthday_natCast]
    theorem SetTheory.PGame.birthday_nat_cast (n : ℕ) :
    (↑n).birthday = ↑n

    Alias of SetTheory.PGame.birthday_natCast.

    source
    theorem SetTheory.PGame.birthday_add_nat (a : SetTheory.PGame) (n : ℕ) :
    (a + ↑n).birthday = a.birthday + ↑n
    source
    theorem SetTheory.PGame.birthday_nat_add (a : SetTheory.PGame) (n : ℕ) :
    (↑n + a).birthday = a.birthday + ↑n