Game addition relation

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} {rα : α → α → Prop} {rβ : β → β → Prop} {a₁ a₂ : α} {b : β} : rα a₁ a₂ → GameAdd rα rβ (a₁, b) (a₂, b)
• snd {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b₁ b₂ : β} : rβ b₁ b₂ → GameAdd rα rβ (a, b₁) (a, b₂)

theorem Prod.gameAdd_iff {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {x y : α × β} : GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ 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₂ : β} : GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂

@[simp]

theorem Prod.gameAdd_swap_swap {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) (a b : α × β) : GameAdd rβ rα a.swap b.swap ↔ GameAdd rα rβ a b

theorem Prod.gameAdd_swap_swap_mk {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) (a₁ a₂ : α) (b₁ b₂ : β) : GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ GameAdd rβ rα (b₁, a₁) (b₂, a₂)

theorem Prod.gameAdd_le_lex {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) : GameAdd rα rβ ≤ Prod.Lex rα rβ

Prod.GameAdd is a subrelation of Prod.Lex.

theorem Prod.rprod_le_transGen_gameAdd {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) : RProd rα rβ ≤ Relation.TransGen (GameAdd rα rβ)

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 rα a) (hb : Acc rβ b) : Acc (Prod.GameAdd rα rβ) (a, 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α : WellFounded rα) (hβ : WellFounded rβ) : WellFounded (Prod.GameAdd rα rβ)

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α : WellFounded rα) (hβ : WellFounded rβ) (IH : (a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → GameAdd rα rβ (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.

theorem Prod.GameAdd.fix_eq {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {C : α → β → Sort u_3} (hα : WellFounded rα) (hβ : WellFounded rβ) (IH : (a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a : α) (b : β) : fix hα hβ IH a b = IH a b fun (a' : α) (b' : β) (x : GameAdd rα rβ (a', b') (a, b)) => fix hα hβ IH a' b'

theorem Prod.GameAdd.induction {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {C : α → β → Prop} : WellFounded rα → WellFounded rβ → (∀ (a₁ : α) (b₁ : β), (∀ (a₂ : α) (b₂ : β), GameAdd rα rβ (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.GameAdd rα = Sym2.lift₂ ⟨fun (a₁ b₁ a₂ b₂ : α) => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩

theorem Sym2.gameAdd_iff {α : Type u_1} {rα : α → α → Prop} {x y : α × α} : GameAdd rα (Sym2.mk x) (Sym2.mk y) ↔ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y

theorem Sym2.gameAdd_mk'_iff {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b₁ b₂ : α} : GameAdd rα s(a₁, b₁) s(a₂, b₂) ↔ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)

theorem Prod.GameAdd.to_sym2 {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b₁ b₂ : α} (h : GameAdd rα rα (a₁, b₁) (a₂, b₂)) : Sym2.GameAdd rα s(a₁, b₁) s(a₂, b₂)

theorem Sym2.GameAdd.fst {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α} (h : rα a₁ a₂) : GameAdd rα s(a₁, b) s(a₂, b)

theorem Sym2.GameAdd.snd {α : Type u_1} {rα : α → α → Prop} {a b₁ b₂ : α} (h : rα b₁ b₂) : GameAdd rα s(a, b₁) s(a, b₂)

theorem Sym2.GameAdd.fst_snd {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α} (h : rα a₁ a₂) : GameAdd rα s(a₁, b) s(b, a₂)

theorem Sym2.GameAdd.snd_fst {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α} (h : rα a₁ a₂) : GameAdd rα s(b, a₁) s(a₂, b)

theorem Acc.sym2_gameAdd {α : Type u_1} {rα : α → α → Prop} {a b : α} (ha : Acc rα a) (hb : Acc rα b) : Acc (Sym2.GameAdd rα) s(a, b)

theorem WellFounded.sym2_gameAdd {α : Type u_1} {rα : α → α → Prop} (h : WellFounded rα) : WellFounded (Sym2.GameAdd rα)

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 : WellFounded rα) (IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα 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.

theorem Sym2.GameAdd.fix_eq {α : Type u_1} {rα : α → α → Prop} {C : α → α → Sort u_3} (hr : WellFounded rα) (IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a b : α) : fix hr IH a b = IH a b fun (a' b' : α) (x : GameAdd rα s(a', b') s(a, b)) => fix hr IH a' b'

theorem Sym2.GameAdd.induction {α : Type u_1} {rα C : α → α → Prop} : WellFounded rα → (∀ (a₁ b₁ : α), (∀ (a₂ b₂ : α), GameAdd rα 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.