Prod.GameAdd.induction
theorem Prod.GameAdd.induction :
∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {C : α → β → Prop},
WellFounded rα →
WellFounded rβ →
(∀ (a₁ : α) (b₁ : β), (∀ (a₂ : α) (b₂ : β), Prod.GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) →
∀ (a : α) (b : β), C a b
This theorem states that for any types `α` and `β` and any relations `rα` and `rβ` on `α` and `β` respectively, if these relations are well-founded and there's a predicate `C` on `α` and `β` such that for any pairs `(a1, b1)` and `(a2, b2)`, if the `Prod.GameAdd` of `(a2, b2)` and `(a1, b1)` holds under `rα` and `rβ`, then `C a2 b2` implies `C a1 b1`, then `C a b` holds for all `a` in `α` and `b` in `β`. This is essentially a form of induction on the well-founded relation `Prod.GameAdd`. The theorem also notes that it would be more general to induce on the lexicographic order instead.
More concisely: If relations `rα` and `rβ` on types `α` and `β` are well-founded, and there is a predicate `C` such that `C a2 b2` implies `C a1 b1` whenever `(a1, b1)` and `(a2, b2)` satisfy `Prod.GameAdd` under `rα` and `rβ`, then `C a b` holds for all `a` in `α` and `b` in `β`.
|
WellFounded.sym2_gameAdd
theorem WellFounded.sym2_gameAdd :
∀ {α : Type u_1} {rα : α → α → Prop}, WellFounded rα → WellFounded (Sym2.GameAdd rα)
The theorem `WellFounded.sym2_gameAdd` states that for any type `α` and any binary relation `rα` on `α`, if `rα` is well-founded, then the `Sym2.GameAdd` relation is also well-founded. In other words, if there are no infinite descending chains in `rα`, then there are also no infinite descending chains when playing the `Sym2.GameAdd` game, which involves reaching one symmetric pair from another by decreasing either entry with respect to the relation `rα`.
More concisely: If `rα` is a well-founded relation on type `α`, then the `Sym2.GameAdd` relation induced by `rα` is also well-founded.
|
Acc.prod_gameAdd
theorem Acc.prod_gameAdd :
∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b : β},
Acc rα a → Acc rβ b → Acc (Prod.GameAdd rα rβ) (a, b)
This theorem states that for any two types `α` and `β`, and relations `rα` on `α` and `rβ` on `β`, if an element `a` of type `α` is accessible under `rα` and an element `b` of type `β` is accessible under `rβ`, then the pair `(a, b)` is accessible under the `Prod.GameAdd` of `rα` and `rβ`. Notably, this differs from `Prod.lexAccessible` which requires a stronger condition that every element of `β` be accessible under `rβ`.
More concisely: For any types `α` and `β` and relations `rα` on `α` and `rβ` on `β`, if every element of `α` accessible under `rα` has an accessible mate under `rβ`, then the pair of an accessible element in `α` and an accessible element in `β` is accessible under the product relation `Prod.GameAdd` of `rα` and `rβ`.
|
Sym2.GameAdd.induction
theorem Sym2.GameAdd.induction :
∀ {α : Type u_1} {rα C : α → α → Prop},
WellFounded rα →
(∀ (a₁ b₁ : α), (∀ (a₂ b₂ : α), Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) →
∀ (a b : α), C a b
The theorem `Sym2.GameAdd.induction` is a principle of induction for the well-founded relation `Sym2.GameAdd`. Given a type `α` and two relations `rα` and `C` on `α`, if `rα` is well-founded, then for every pair `(a₁, b₁)` of `α`, if for every pair `(a₂, b₂)` of `α` such that `(a₂, b₂)` can be reached from `(a₁, b₁)` by decreasing either entry with respect to `rα` (i.e., `Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁)`), the property `C` holds for `(a₂, b₂)`, then the property `C` must also hold for `(a₁, b₁)`. The theorem then concludes that the property `C` holds for every pair `(a, b)` in `α`.
More concisely: If `rα` is a well-founded relation on `α` and for all `(a₁, b₁)` in `α`, if `C` holds for all `(a₂, b₂)` reachable from `(a₁, b₁)` by decreasing an entry with respect to `rα`, then `C` holds for all `(a, b)` in `α`.
|
WellFounded.prod_gameAdd
theorem WellFounded.prod_gameAdd :
∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop},
WellFounded rα → WellFounded rβ → WellFounded (Prod.GameAdd rα rβ)
This theorem asserts that the `Prod.GameAdd` relation is well-founded when applied to well-founded inputs. Specifically, if you have two well-founded games represented by the relations `rα` and `rβ` over types `α` and `β` respectively, then the sum of these two games, represented by the `Prod.GameAdd` relation, is also well-founded. In other words, the theorem guarantees that game addition operation preserves the well-foundedness property.
More concisely: If `rα` and `rβ` are well-founded relations over types `α` and `β` respectively, then the relation `Prod.GameAdd (rα) (rβ)` is also well-founded.
|
Prod.rprod_le_transGen_gameAdd
theorem Prod.rprod_le_transGen_gameAdd :
∀ {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop),
Prod.RProd rα rβ ≤ Relation.TransGen (Prod.GameAdd rα rβ)
The theorem `Prod.rprod_le_transGen_gameAdd` asserts that for any two types `α` and `β`, and any two relations `rα` and `rβ` on `α` and `β` respectively, the `Prod.RProd` of `rα` and `rβ` is a subrelation of the transitive closure of `Prod.GameAdd` of `rα` and `rβ`. In other words, if a pair of elements is related by `Prod.RProd`, then there is a sequence of steps via the `Prod.GameAdd` relation that connects the same two elements.
More concisely: For any types `α` and `β` and relations `rα` on `α` and `rβ` on `β`, the `Prod.RProd` of `rα` and `rβ` is included in the transitive closure of `Prod.GameAdd` of `rα` and `rβ`.
|
Prod.gameAdd_le_lex
theorem Prod.gameAdd_le_lex :
∀ {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop), Prod.GameAdd rα rβ ≤ Prod.Lex rα rβ := by
sorry
The theorem `Prod.gameAdd_le_lex` asserts that for any two types α and β, and any two relations `rα` and `rβ` on these types, the `GameAdd` relation on the product of α and β is a subrelation of the `Lex` (lexicographic) relation on the same product. In other words, if a pair of elements (a, b) from α x β relates to another pair (c, d) through the `GameAdd` relation, then the same pair (a, b) also relates to (c, d) through the `Lex` relation.
More concisely: For all types α and β and relations rα on α and rβ on β, the GameAdd relation on α × β is included in the lexicographic relation on α × β.
|