# Well-foundedness of the lexicographic and product orders on DFinsupp and Pi#

The primary results are DFinsupp.Lex.wellFounded and the two variants that follow it, which essentially say that if (· > ·) is a well order on ι, (· < ·) is well-founded on each α i, and 0 is a bottom element in α i, then the lexicographic (· < ·) is well-founded on Π₀ i, α i. The proof is modelled on the proof of WellFounded.cutExpand.

The results are used to prove Pi.Lex.wellFounded and two variants, which say that if ι is finite and equipped with a linear order and (· < ·) is well-founded on each α i, then the lexicographic (· < ·) is well-founded on Π i, α i, and the same is true for Π₀ i, α i (DFinsupp.Lex.wellFounded_of_finite), because DFinsupp is order-isomorphic to pi when ι is finite.

Finally, we deduce DFinsupp.wellFoundedLT, Pi.wellFoundedLT, DFinsupp.wellFoundedLT_of_finite and variants, which concern the product order rather than the lexicographic one. An order on ι is not required in these results, but we deduce them from the well-foundedness of the lexicographic order by choosing a well order on ι so that the product order (· < ·) becomes a subrelation of the lexicographic (· < ·).

All results are provided in two forms whenever possible: a general form where the relations can be arbitrary (not the (· < ·) of a preorder, or not even transitive, etc.) and a specialized form provided as WellFoundedLT instances where the (d)Finsupp/pi type (or their Lex type synonyms) carries a natural (· < ·).

Notice that the definition of DFinsupp.Lex says that x < y according to DFinsupp.Lex r s iff there exists a coordinate i : ι such that x i < y i according to s i, and at all r-smaller coordinates j (i.e. satisfying r j i), x remains unchanged relative to y; in other words, coordinates j such that ¬ r j i and j ≠ i are exactly where changes can happen arbitrarily. This explains the appearance of rᶜ ⊓ (≠) in dfinsupp.acc_single and dfinsupp.well_founded. When r is trichotomous (e.g. the (· < ·) of a linear order), ¬ r j i ∧ j ≠ i implies r i j, so it suffices to require r.swap to be well-founded.

theorem DFinsupp.lex_fibration {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] (r : ιιProp) (s : (i : ι) → α iα iProp) [(i : ι) → (s : Set ι) → Decidable (i s)] :
Relation.Fibration (InvImage (Prod.GameAdd () ()) Prod.snd) () fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) => x.2.1.piecewise x.2.2 x.1

This key lemma says that if a finitely supported dependent function x₀ is obtained by merging two such functions x₁ and x₂, and if we evolve x₀ down the DFinsupp.Lex relation one step and get x, we can always evolve one of x₁ and x₂ down the DFinsupp.Lex relation one step while keeping the other unchanged, and merge them back (possibly in a different way) to get back x. In other words, the two parts evolve essentially independently under DFinsupp.Lex. This is used to show that a function x is accessible if DFinsupp.single i (x i) is accessible for each i in the (finite) support of x (DFinsupp.Lex.acc_of_single).

theorem DFinsupp.Lex.acc_of_single_erase {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} [] {x : Π₀ (i : ι), α i} (i : ι) (hs : Acc () (DFinsupp.single i (x i))) (hu : Acc () ()) :
Acc () x
theorem DFinsupp.Lex.acc_zero {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} (hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) :
Acc () 0
theorem DFinsupp.Lex.acc_of_single {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} (hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) [] [(i : ι) → (x : α i) → Decidable (x 0)] (x : Π₀ (i : ι), α i) :
(ix.support, Acc () (DFinsupp.single i (x i)))Acc () x
theorem DFinsupp.Lex.acc_single {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} (hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : ∀ (i : ι), WellFounded (s i)) [] {i : ι} (hi : Acc (r fun (x x_1 : ι) => x x_1) i) (a : α i) :
Acc () ()
theorem DFinsupp.Lex.acc {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} (hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : ∀ (i : ι), WellFounded (s i)) [] [(i : ι) → (x : α i) → Decidable (x 0)] (x : Π₀ (i : ι), α i) (h : ix.support, Acc (r fun (x x_1 : ι) => x x_1) i) :
Acc () x
theorem DFinsupp.Lex.wellFounded {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} (hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : ∀ (i : ι), WellFounded (s i)) (hr : WellFounded (r fun (x x_1 : ι) => x x_1)) :
theorem DFinsupp.Lex.wellFounded' {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} (hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : ∀ (i : ι), WellFounded (s i)) [] (hr : ) :
instance DFinsupp.Lex.wellFoundedLT {ι : Type u_1} {α : ιType u_2} [LT ι] [IsTrichotomous ι fun (x x_1 : ι) => x < x_1] [hι : ] [(i : ι) → ] [hα : ∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT (Lex (Π₀ (i : ι), α i))
Equations
• =
theorem Pi.Lex.wellFounded {ι : Type u_1} {α : ιType u_2} (r : ιιProp) {s : (i : ι) → α iα iProp} [] [] (hs : ∀ (i : ι), WellFounded (s i)) :
WellFounded (Pi.Lex r fun {i : ι} => s i)
instance Pi.Lex.wellFoundedLT {ι : Type u_1} {α : ιType u_2} [] [] [(i : ι) → LT (α i)] [hwf : ∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT (Lex ((i : ι) → α i))
Equations
• =
instance Function.Lex.wellFoundedLT {ι : Type u_1} {α : Type u_3} [] [] [LT α] [] :
WellFoundedLT (Lex (ια))
Equations
• =
theorem DFinsupp.Lex.wellFounded_of_finite {ι : Type u_1} {α : ιType u_2} (r : ιιProp) {s : (i : ι) → α iα iProp} [] [] [(i : ι) → Zero (α i)] (hs : ∀ (i : ι), WellFounded (s i)) :
instance DFinsupp.Lex.wellFoundedLT_of_finite {ι : Type u_1} {α : ιType u_2} [] [] [(i : ι) → Zero (α i)] [(i : ι) → LT (α i)] [hwf : ∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT (Lex (Π₀ (i : ι), α i))
Equations
• =
theorem DFinsupp.wellFoundedLT {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] [∀ (i : ι), WellFoundedLT (α i)] (hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0) :
WellFoundedLT (Π₀ (i : ι), α i)
instance DFinsupp.wellFoundedLT' {ι : Type u_1} {α : ιType u_2} [(i : ι) → ] [∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT (Π₀ (i : ι), α i)
Equations
• =
instance Pi.wellFoundedLT {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Preorder (α i)] [hw : ∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT ((i : ι) → α i)
Equations
• =
instance Function.wellFoundedLT {ι : Type u_1} {α : Type u_3} [] [] [] :
WellFoundedLT (ια)
Equations
• =
instance DFinsupp.wellFoundedLT_of_finite {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] [∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT (Π₀ (i : ι), α i)
Equations
• =