mathlib documentation

data.dfinsupp.well_founded

Well-foundedness of the lexicographic and product orders on dfinsupp and pi #

The primary results are dfinsupp.lex.well_founded 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 well_founded.cut_expand.

The results are used to prove pi.lex.well_founded 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.well_founded_of_finite), because dfinsupp is order-isomorphic to pi when ι is finite.

Finally, we deduce dfinsupp.well_founded_lt, pi.well_founded_lt, dfinsupp.well_founded_lt_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 well_founded_lt 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} [hz : Π (i : ι), has_zero (α i)] (r : ι ι Prop) (s : Π (i : ι), α i α i Prop) [Π (i : ι) (s : set ι), decidable (i s)] :
relation.fibration (inv_image (prod.game_add (dfinsupp.lex r s) (dfinsupp.lex r s)) prod.snd) (dfinsupp.lex r s) (λ (x : set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i), x.snd.fst.piecewise x.snd.snd x.fst)

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} [hz : Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} [decidable_eq ι] {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} [hz : Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} (hbot : ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) :
theorem dfinsupp.lex.acc_of_single {ι : Type u_1} {α : ι Type u_2} [hz : Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} (hbot : ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) [decidable_eq ι] [Π (i : ι) (x : α i), decidable (x 0)] (x : Π₀ (i : ι), α i) :
( (i : ι), i x.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} [hz : Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} (hbot : ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : (i : ι), well_founded (s i)) [decidable_eq ι] {i : ι} (hi : acc (r ne) i) (a : α i) :
theorem dfinsupp.lex.acc {ι : Type u_1} {α : ι Type u_2} [hz : Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} (hbot : ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : (i : ι), well_founded (s i)) [decidable_eq ι] [Π (i : ι) (x : α i), decidable (x 0)] (x : Π₀ (i : ι), α i) (h : (i : ι), i x.support acc (r ne) i) :
theorem dfinsupp.lex.well_founded {ι : Type u_1} {α : ι Type u_2} [hz : Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} (hbot : ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : (i : ι), well_founded (s i)) (hr : well_founded (r ne)) :
theorem dfinsupp.lex.well_founded' {ι : Type u_1} {α : ι Type u_2} [hz : Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} (hbot : ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : (i : ι), well_founded (s i)) [is_trichotomous ι r] (hr : well_founded (function.swap r)) :
@[protected, instance]
def dfinsupp.lex.well_founded_lt {ι : Type u_1} {α : ι Type u_2} [has_lt ι] [is_trichotomous ι has_lt.lt] [hι : well_founded_gt ι] [Π (i : ι), canonically_ordered_add_monoid (α i)] [hα : (i : ι), well_founded_lt (α i)] :
well_founded_lt (lex (Π₀ (i : ι), α i))
theorem pi.lex.well_founded {ι : Type u_1} {α : ι Type u_2} (r : ι ι Prop) {s : Π (i : ι), α i α i Prop} [is_strict_total_order ι r] [finite ι] (hs : (i : ι), well_founded (s i)) :
@[protected, instance]
def pi.lex.well_founded_lt {ι : Type u_1} {α : ι Type u_2} [linear_order ι] [finite ι] [Π (i : ι), has_lt (α i)] [hwf : (i : ι), well_founded_lt (α i)] :
well_founded_lt (lex (Π (i : ι), α i))
@[protected, instance]
def function.lex.well_founded_lt {ι : Type u_1} {α : Type u_2} [linear_order ι] [finite ι] [has_lt α] [well_founded_lt α] :
theorem dfinsupp.lex.well_founded_of_finite {ι : Type u_1} {α : ι Type u_2} (r : ι ι Prop) {s : Π (i : ι), α i α i Prop} [is_strict_total_order ι r] [finite ι] [Π (i : ι), has_zero (α i)] (hs : (i : ι), well_founded (s i)) :
@[protected, instance]
def dfinsupp.lex.well_founded_lt_of_finite {ι : Type u_1} {α : ι Type u_2} [linear_order ι] [finite ι] [Π (i : ι), has_zero (α i)] [Π (i : ι), has_lt (α i)] [hwf : (i : ι), well_founded_lt (α i)] :
well_founded_lt (lex (Π₀ (i : ι), α i))
@[protected]
theorem dfinsupp.well_founded_lt {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), preorder (α i)] [ (i : ι), well_founded_lt (α i)] (hbot : ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0) :
well_founded_lt (Π₀ (i : ι), α i)
@[protected, instance]
def dfinsupp.well_founded_lt' {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), canonically_ordered_add_monoid (α i)] [ (i : ι), well_founded_lt (α i)] :
well_founded_lt (Π₀ (i : ι), α i)
@[protected, instance]
def pi.well_founded_lt {ι : Type u_1} {α : ι Type u_2} [finite ι] [Π (i : ι), preorder (α i)] [hw : (i : ι), well_founded_lt (α i)] :
well_founded_lt (Π (i : ι), α i)
@[protected, instance]
def function.well_founded_lt {ι : Type u_1} {α : Type u_2} [finite ι] [preorder α] [well_founded_lt α] :
@[protected, instance]
def dfinsupp.well_founded_lt_of_finite {ι : Type u_1} {α : ι Type u_2} [finite ι] [Π (i : ι), has_zero (α i)] [Π (i : ι), preorder (α i)] [ (i : ι), well_founded_lt (α i)] :
well_founded_lt (Π₀ (i : ι), α i)