Documentation

This file defines, given relations rα : α → α → Prop and rβ : β → β → Prop, a relation Prod.GameAdd on pairs, such that GameAdd 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.

We also define Sym2.GameAdd, which is the unordered pair analog of Prod.GameAdd.

Main definitions and results #

• Prod.GameAdd: the game addition relation on ordered pairs.

• WellFounded.prod_gameAdd: formalizes induction on ordered pairs, where exactly one entry decreases at a time.

• Sym2.GameAdd: the game addition relation on unordered pairs.

• WellFounded.sym2_gameAdd: formalizes induction on unordered pairs, where exactly one entry decreases at a time.

Prod.GameAdd#

inductive Prod.GameAdd {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) :
α × βα × βProp

Prod.GameAdd rα rβ x y means that x can be reached from y by decreasing either entry with respect to the relations rα and rβ.

It is so called, as it models game addition within combinatorial game theory. 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 GameAdd 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.

See Sym2.GameAdd for the unordered pair analog.

• fst: ∀ {α : Type u_1} {β : Type u_2} { : ααProp} { : ββProp} {a₁ a₂ : α} {b : β}, a₁ a₂Prod.GameAdd (a₁, b) (a₂, b)
• snd: ∀ {α : Type u_1} {β : Type u_2} { : ααProp} { : ββProp} {a : α} {b₁ b₂ : β}, b₁ b₂Prod.GameAdd (a, b₁) (a, b₂)
Instances For
theorem Prod.gameAdd_iff {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} {x : α × β} {y : α × β} :
Prod.GameAdd x y x.1 y.1 x.2 = y.2 x.2 y.2 x.1 = y.1
theorem Prod.gameAdd_mk_iff {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} :
Prod.GameAdd (a₁, b₁) (a₂, b₂) a₁ a₂ b₁ = b₂ b₁ b₂ a₁ = a₂
@[simp]
theorem Prod.gameAdd_swap_swap {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) (a : α × β) (b : α × β) :
theorem Prod.gameAdd_swap_swap_mk {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
theorem Prod.gameAdd_le_lex {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) :

Prod.GameAdd is a subrelation of Prod.Lex.

theorem Prod.rprod_le_transGen_gameAdd {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) :

Prod.RProd is a subrelation of the transitive closure of Prod.GameAdd.

theorem Acc.prod_gameAdd {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} {a : α} {b : β} (ha : Acc a) (hb : Acc b) :

If a is accessible under rα and b is accessible under rβ, then (a, b) is accessible under Prod.GameAdd rα rβ. Notice that Prod.lexAccessible requires the stronger condition ∀ b, Acc rβ b.

theorem WellFounded.prod_gameAdd {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} (hα : ) (hβ : ) :

The Prod.GameAdd relation on well-founded inputs is well-founded.

In particular, the sum of two well-founded games is well-founded.

def Prod.GameAdd.fix {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} {C : αβSort u_3} (hα : ) (hβ : ) (IH : (a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → Prod.GameAdd (a₂, b₂) (a₁, b₁)C a₂ b₂)C a₁ b₁) (a : α) (b : β) :
C a b

Recursion on the well-founded Prod.GameAdd relation. Note that it's strictly more general to recurse on the lexicographic order instead.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Prod.GameAdd.fix_eq {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} {C : αβSort u_3} (hα : ) (hβ : ) (IH : (a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → Prod.GameAdd (a₂, b₂) (a₁, b₁)C a₂ b₂)C a₁ b₁) (a : α) (b : β) :
Prod.GameAdd.fix IH a b = IH a b fun (a' : α) (b' : β) (x : Prod.GameAdd (a', b') (a, b)) => Prod.GameAdd.fix IH a' b'
theorem Prod.GameAdd.induction {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} {C : αβProp} :
(∀ (a₁ : α) (b₁ : β), (∀ (a₂ : α) (b₂ : β), Prod.GameAdd (a₂, b₂) (a₁, b₁)C a₂ b₂)C a₁ b₁)∀ (a : α) (b : β), C a b

Induction on the well-founded Prod.GameAdd relation. Note that it's strictly more general to induct on the lexicographic order instead.

Sym2.GameAdd#

def Sym2.GameAdd {α : Type u_1} (rα : ααProp) :
Sym2 αSym2 αProp

Sym2.GameAdd rα x y means that x can be reached from y by decreasing either entry with respect to the relation rα.

See Prod.GameAdd for the ordered pair analog.

Equations
• = Sym2.lift₂ fun (a₁ b₁ a₂ b₂ : α) => Prod.GameAdd (a₁, b₁) (a₂, b₂) Prod.GameAdd (b₁, a₁) (a₂, b₂),
Instances For
theorem Sym2.gameAdd_iff {α : Type u_1} {rα : ααProp} {x : α × α} {y : α × α} :
theorem Sym2.gameAdd_mk'_iff {α : Type u_1} {rα : ααProp} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
theorem Prod.GameAdd.to_sym2 {α : Type u_1} {rα : ααProp} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h : Prod.GameAdd (a₁, b₁) (a₂, b₂)) :
theorem Sym2.GameAdd.fst {α : Type u_1} {rα : ααProp} {a₁ : α} {a₂ : α} {b : α} (h : a₁ a₂) :
theorem Sym2.GameAdd.snd {α : Type u_1} {rα : ααProp} {a : α} {b₁ : α} {b₂ : α} (h : b₁ b₂) :
theorem Sym2.GameAdd.fst_snd {α : Type u_1} {rα : ααProp} {a₁ : α} {a₂ : α} {b : α} (h : a₁ a₂) :
theorem Sym2.GameAdd.snd_fst {α : Type u_1} {rα : ααProp} {a₁ : α} {a₂ : α} {b : α} (h : a₁ a₂) :
theorem Acc.sym2_gameAdd {α : Type u_1} {rα : ααProp} {a : α} {b : α} (ha : Acc a) (hb : Acc b) :
Acc () s(a, b)
theorem WellFounded.sym2_gameAdd {α : Type u_1} {rα : ααProp} (h : ) :

The Sym2.GameAdd relation on well-founded inputs is well-founded.

def Sym2.GameAdd.fix {α : Type u_1} {rα : ααProp} {C : ααSort u_3} (hr : ) (IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → Sym2.GameAdd s(a₂, b₂) s(a₁, b₁)C a₂ b₂)C a₁ b₁) (a : α) (b : α) :
C a b

Recursion on the well-founded Sym2.GameAdd relation.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Sym2.GameAdd.fix_eq {α : Type u_1} {rα : ααProp} {C : ααSort u_3} (hr : ) (IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → Sym2.GameAdd s(a₂, b₂) s(a₁, b₁)C a₂ b₂)C a₁ b₁) (a : α) (b : α) :
Sym2.GameAdd.fix hr IH a b = IH a b fun (a' b' : α) (x : Sym2.GameAdd s(a', b') s(a, b)) => Sym2.GameAdd.fix hr IH a' b'
theorem Sym2.GameAdd.induction {α : Type u_1} {rα : ααProp} {C : ααProp} :
(∀ (a₁ b₁ : α), (∀ (a₂ b₂ : α), Sym2.GameAdd s(a₂, b₂) s(a₁, b₁)C a₂ b₂)C a₁ b₁)∀ (a b : α), C a b

Induction on the well-founded Sym2.GameAdd relation.