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 #
pgame.birthday
: The birthday of a pre-game.
Todo #
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
- (pgame.mk xl xr xL xR).birthday = linear_order.max (ordinal.lsub (λ (i : xl), (xL i).birthday)) (ordinal.lsub (λ (i : xr), (xR i).birthday))
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))
theorem
pgame.birthday_move_right_lt
{x : pgame}
(i : x.right_moves) :
(x.move_right i).birthday < x.birthday
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
@[simp]
theorem
pgame.birthday_eq_zero
(x : pgame) :
x.birthday = 0 ↔ is_empty x.left_moves ∧ is_empty x.right_moves