DFinsupp.lex_fibration
theorem DFinsupp.lex_fibration :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] (r : ι → ι → Prop)
(s : (i : ι) → α i → α i → Prop) [inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)],
Relation.Fibration (InvImage (Prod.GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) Prod.snd) (DFinsupp.Lex r s)
fun x => x.2.1.piecewise x.2.2 x.1
This theorem states that for any types `ι` and `α`, and any relations `r` and `s`, if a dependent function `x₀` with finite support is obtained by merging two such functions `x₁` and `x₂`, and if `x₀` is evolved down the `DFinsupp.Lex` relation one step to obtain `x`, then we can evolve either `x₁` or `x₂` down the `DFinsupp.Lex` relation one step while keeping the other unchanged, and merge them back (possibly differently) to get `x` again. In essence, the theorem says that the two parts of a function evolve essentially independently under the `DFinsupp.Lex` relation. This is useful for showing that a function `x` is accessible if `DFinsupp.single i (x i)` is accessible for each `i` in the finite support of `x`. It is an instance of `Relation.Fibration` for the inverse image of the `Prod.GameAdd` of `DFinsupp.Lex r s` and `DFinsupp.Lex r s` by `Prod.snd` and the `DFinsupp.Lex r s` relation.
More concisely: Given types `ι`, `α`, relations `r` and `s`, and dependent functions `x₀` with finite support obtained by merging `x₁` and `x₂`, if `x` is obtained from `x₀` by evolving one step down the `DFinsupp.Lex r s` relation, then there exist evolutions of `x₁` and `x₂` down the same relation such that merging their evolved functions yields `x`.
|
DFinsupp.Lex.wellFounded'
theorem DFinsupp.Lex.wellFounded' :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop}
{s : (i : ι) → α i → α i → Prop},
(∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) →
(∀ (i : ι), WellFounded (s i)) →
∀ [inst_1 : IsTrichotomous ι r], WellFounded (Function.swap r) → WellFounded (DFinsupp.Lex r s)
The theorem `DFinsupp.Lex.wellFounded'` states that for any type `ι`, and any type function `α : ι → Type` which gives a Type, presumed to have a zero, for each `ι`, along with an instance `(i : ι) → Zero (α i)` for each `ι`, if we have a relation `r : ι → ι → Prop` on `ι` and a family of relations `s : (i : ι) → α i → α i → Prop`, such that for all `i : ι` and `a : α i`, `s i a 0` is false (that is, no element compares smaller than zero) and `s i` is well-founded for each `i`, and if `r` is trichotomous and its opposite relation is well-founded, then the lexicographic relation `DFinsupp.Lex r s` on the direct sum of functions from `i` to `α i` is also well-founded.
This condition is important in formalizing the concept of "lexicographic order", where we first compare the input indexes according to `r` and then compare the function values according to `s i`, which is often used in mathematical proofs that require well-founded induction or recursion over the domain of the direct sum of functions.
More concisely: If `ι` is a type, `α : ι → Type` is a type-valued function with a zero instance, `r : ι → ι → Prop` is a trichotomous and well-founded relation, and `s : (i : ι) → α i → α i → Prop` is a family of well-founded relations such that `s i a 0` is false for all `a : α i`, then the lexicographic relation `DFinsupp.Lex r s` on the direct sum of functions from `i` to `α i` is well-founded.
|
Pi.Lex.wellFounded
theorem Pi.Lex.wellFounded :
∀ {ι : Type u_1} {α : ι → Type u_2} (r : ι → ι → Prop) {s : (i : ι) → α i → α i → Prop}
[inst : IsStrictTotalOrder ι r] [inst : Finite ι],
(∀ (i : ι), WellFounded (s i)) → WellFounded (Pi.Lex r fun {i} => s i)
This theorem states that, for any types ι and α (with α depending on ι), given a relation r on ι and a family of relations s indexed by ι on α, if r is a strict total order, the type ι is finite, and each relation s(i) is well-founded, then the lexicographic relation formed by r and s on the product type, (i : ι) → α i, is also well-founded.
In simpler words, it says that if we have a well-ordered type and a family of well-ordered types indexed by the first, the lexicographic order defined over the whole family is also well-ordered.
More concisely: If ι is a finite, strictly totally ordered type and each relation s(i) on α (for i : ι) is well-founded, then the lexicographic order on the product type (i : ι) → α i is well-founded.
|