Documentation

Mathlib.Order.GameAdd

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 and ). 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 #

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 and .

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 : α × β) :
    Prod.GameAdd a.swap b.swap Prod.GameAdd a b
    theorem Prod.gameAdd_swap_swap_mk {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
    Prod.GameAdd (a₁, b₁) (a₂, b₂) Prod.GameAdd (b₁, a₁) (b₂, a₂)
    theorem Prod.gameAdd_le_lex {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) :
    Prod.GameAdd Prod.Lex

    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) :
    Acc (Prod.GameAdd ) (a, b)

    If a is accessible under and b is accessible under , 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 ) (hβ : WellFounded ) :

    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 ) (hβ : WellFounded ) (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α : WellFounded ) (hβ : WellFounded ) (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} :
      WellFounded WellFounded (∀ (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 .

      See Prod.GameAdd for the ordered pair analog.

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

        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 ) (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 : WellFounded ) (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} :
          WellFounded (∀ (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.