Documentation

Mathlib.Data.DFinsupp.WellFounded

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 (DFinsupp.Lex r s) (DFinsupp.Lex r s)) Prod.snd) (DFinsupp.Lex r s) 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} [DecidableEq ι] {x : Π₀ (i : ι), α i} (i : ι) (hs : Acc (DFinsupp.Lex r s) (DFinsupp.single i (x i))) (hu : Acc (DFinsupp.Lex r s) (DFinsupp.erase i 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) :
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) [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x 0)] (x : Π₀ (i : ι), α i) :
(∀ ix.support, Acc (DFinsupp.Lex r s) (DFinsupp.single i (x i)))Acc (DFinsupp.Lex r s) 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)) [DecidableEq ι] {i : ι} (hi : Acc (r fun (x1 x2 : ι) => x1 x2) i) (a : α i) :
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)) [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x 0)] (x : Π₀ (i : ι), α i) (h : ix.support, Acc (r fun (x1 x2 : ι) => x1 x2) i) :
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 (x1 x2 : ι) => x1 x2)) :
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)) [IsTrichotomous ι r] (hr : WellFounded (Function.swap r)) :
instance DFinsupp.Lex.wellFoundedLT {ι : Type u_1} {α : ιType u_2} [LT ι] [IsTrichotomous ι fun (x1 x2 : ι) => x1 < x2] [hι : WellFoundedGT ι] [(i : ι) → CanonicallyOrderedAddCommMonoid (α 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} [IsStrictTotalOrder ι r] [Finite ι] (hs : ∀ (i : ι), WellFounded (s i)) :
WellFounded (Pi.Lex r fun {i : ι} => s i)
instance Pi.Lex.wellFoundedLT {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [Finite ι] [(i : ι) → LT (α i)] [hwf : ∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT (Lex ((i : ι) → α i))
Equations
  • =
instance Function.Lex.wellFoundedLT {ι : Type u_1} {α : Type u_3} [LinearOrder ι] [Finite ι] [LT α] [WellFoundedLT α] :
WellFoundedLT (Lex (ια))
Equations
  • =
theorem DFinsupp.Lex.wellFounded_of_finite {ι : Type u_1} {α : ιType u_2} (r : ιιProp) {s : (i : ι) → α iα iProp} [IsStrictTotalOrder ι r] [Finite ι] [(i : ι) → Zero (α i)] (hs : ∀ (i : ι), WellFounded (s i)) :
instance DFinsupp.Lex.wellFoundedLT_of_finite {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [Finite ι] [(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 : ι) → CanonicallyOrderedAddCommMonoid (α i)] [∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT (Π₀ (i : ι), α i)
Equations
  • =
instance Pi.wellFoundedLT {ι : Type u_1} {α : ιType u_2} [Finite ι] [(i : ι) → Preorder (α i)] [hw : ∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT ((i : ι) → α i)
Equations
  • =
instance Function.wellFoundedLT {ι : Type u_1} {α : Type u_3} [Finite ι] [Preorder α] [WellFoundedLT α] :
WellFoundedLT (ια)
Equations
  • =
instance DFinsupp.wellFoundedLT_of_finite {ι : Type u_1} {α : ιType u_2} [Finite ι] [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] [∀ (i : ι), WellFoundedLT (α i)] :
WellFoundedLT (Π₀ (i : ι), α i)
Equations
  • =