mathlib3 documentation

set_theory.game.birthday

Birthdays of games #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 pgame.birthday  :
pgame → ordinal

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
source
theorem pgame.birthday_def (x : pgame) :
x.birthday = linear_order.max (ordinal.lsub (λ (i : x.left_moves), (x.move_left i).birthday)) (ordinal.lsub (λ (i : x.right_moves), (x.move_right i).birthday))
source
theorem pgame.birthday_move_left_lt {x : pgame} (i : x.left_moves) :
(x.move_left i).birthday < x.birthday
source
theorem pgame.birthday_move_right_lt {x : pgame} (i : x.right_moves) :
(x.move_right i).birthday < x.birthday
source
theorem pgame.lt_birthday_iff {x : pgame} {o : ordinal} :
o < x.birthday ↔ (∃ (i : x.left_moves), o ≤ (x.move_left i).birthday) ∨ ∃ (i : x.right_moves), o ≤ (x.move_right i).birthday
source
theorem pgame.relabelling.birthday_congr {x y : pgame} :
x.relabelling y → x.birthday = y.birthday
source
@[simp]
theorem pgame.birthday_eq_zero {x : pgame} :
x.birthday = 0 ↔ is_empty x.left_moves ∧ is_empty x.right_moves
source
@[simp]
theorem pgame.birthday_zero  :
0.birthday = 0
source
@[simp]
theorem pgame.birthday_one  :
1.birthday = 1
source
@[simp]
theorem pgame.birthday_star  :
pgame.star.birthday = 1
source
@[simp]
theorem pgame.neg_birthday (x : pgame) :
(-x).birthday = x.birthday
source
@[simp]
theorem pgame.to_pgame_birthday (o : ordinal) :
o.to_pgame.birthday = o
source
theorem pgame.le_birthday (x : pgame) :
x ≤ x.birthday.to_pgame
source
theorem pgame.neg_birthday_le (x : pgame) :
-x.birthday.to_pgame ≤ x
source
@[simp]
theorem pgame.birthday_add (x y : pgame) :
(x + y).birthday = x.birthday.nadd y.birthday
source
theorem pgame.birthday_add_zero (a : pgame) :
(a + 0).birthday = a.birthday
source
theorem pgame.birthday_zero_add (a : pgame) :
(0 + a).birthday = a.birthday
source
theorem pgame.birthday_add_one (a : pgame) :
(a + 1).birthday = order.succ a.birthday
source
theorem pgame.birthday_one_add (a : pgame) :
(1 + a).birthday = order.succ a.birthday
source
@[simp]
theorem pgame.birthday_nat_cast (n : ℕ) :
↑n.birthday = ↑n
source
theorem pgame.birthday_add_nat (a : pgame) (n : ℕ) :
(a + ↑n).birthday = a.birthday + ↑n
source
theorem pgame.birthday_nat_add (a : pgame) (n : ℕ) :
(↑n + a).birthday = a.birthday + ↑n