mathlib documentation

order.game_add

Game addition relation #

This file defines, given relations rα : α → α → Prop and rβ : β → β → Prop, a relation prod.game_add on pairs, such that game_add rα rβ x y iff x can be reached from y by decreasing either entry (with respect to rα and rβ). It is so called since it models the subsequency relation on the addition of combinatorial games.

Main definitions and results #

Todo #

source
inductive prod.game_add {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) :
α × β → α × β → Prop
  • fst : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a' a : α} {b : β}, rα a' a → prod.game_add rα rβ (a', b) (a, b)
  • snd : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b' b : β}, rβ b' b → prod.game_add rα rβ (a, b') (a, b)

The "addition of games" relation in combinatorial game theory, on the product type: if rα a' a means that a ⟶ a' is a valid move in game α, and rβ b' b means that b ⟶ b' is a valid move in game β, then game_add rα rβ specifies the valid moves in the juxtaposition of α and β: the player is free to choose one of the games and make a move in it, while leaving the other game unchanged.

source
theorem prod.game_add_le_lex {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) :
prod.game_add rα rβ ≤ prod.lex rα rβ

game_add is a subrelation of prod.lex.

source
theorem prod.rprod_le_trans_gen_game_add {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) :
prod.rprod rα rβ ≤ relation.trans_gen (prod.game_add rα rβ)

prod.rprod is a subrelation of the transitive closure of game_add.

source
theorem acc.prod_game_add {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b : β} (ha : acc rα a) (hb : acc rβ b) :
acc (prod.game_add rα rβ) (a, b)

If a is accessible under rα and b is accessible under rβ, then (a, b) is accessible under prod.game_add rα rβ. Notice that prod.lex_accessible requires the stronger condition ∀ b, acc rβ b.

source
theorem well_founded.prod_game_add {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} (hα : well_founded rα) (hβ : well_founded rβ) :
well_founded (prod.game_add rα rβ)

The sum of two well-founded games is well-founded.