Documentation

Mathlib.Data.Finsupp.WellFounded

Well-foundedness of the lexicographic and product orders on Finsupp #

Finsupp.Lex.wellFounded and the two variants that follow it essentially say that if (· > ·) is a well order on α, (· < ·) is well-founded on N, and 0 is a bottom element in N, then the lexicographic (· < ·) is well-founded on α →₀ N.

Finsupp.Lex.wellFoundedLT_of_finite says that if α is finite and equipped with a linear order and (· < ·) is well-founded on N, then the lexicographic (· < ·) is well-founded on α →₀ N.

Finsupp.wellFoundedLT and wellFoundedLT_of_finite state the same results for the product order (· < ·), but without the ordering conditions on α.

All results are transferred from DFinsupp via Finsupp.toDFinsupp.

theorem Finsupp.Lex.acc {α : Type u_1} {N : Type u_2} [Zero N] {r : ααProp} {s : NNProp} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : WellFounded s) (x : α →₀ N) (h : ax.support, Acc (r fun (x1 x2 : α) => x1 x2) a) :

Transferred from DFinsupp.Lex.acc. See the top of that file for an explanation for the appearance of the relation rᶜ ⊓ (≠).

theorem Finsupp.Lex.wellFounded {α : Type u_1} {N : Type u_2} [Zero N] {r : ααProp} {s : NNProp} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : WellFounded s) (hr : WellFounded (r fun (x1 x2 : α) => x1 x2)) :
theorem Finsupp.Lex.wellFounded' {α : Type u_1} {N : Type u_2} [Zero N] {r : ααProp} {s : NNProp} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : WellFounded s) [IsTrichotomous α r] (hr : WellFounded (Function.swap r)) :
instance Finsupp.Lex.wellFoundedLT {α : Type u_3} {N : Type u_4} [LT α] [IsTrichotomous α fun (x1 x2 : α) => x1 < x2] [hα : WellFoundedGT α] [CanonicallyOrderedAddCommMonoid N] [hN : WellFoundedLT N] :
Equations
  • =
theorem Finsupp.Lex.wellFounded_of_finite {α : Type u_1} {N : Type u_2} [Zero N] (r : ααProp) {s : NNProp} [IsStrictTotalOrder α r] [Finite α] (hs : WellFounded s) :
theorem Finsupp.Lex.wellFoundedLT_of_finite {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [Finite α] [LT N] [hwf : WellFoundedLT N] :
theorem Finsupp.wellFoundedLT {α : Type u_1} {N : Type u_2} [Zero N] [Preorder N] [WellFoundedLT N] (hbot : ∀ (n : N), ¬n < 0) :
Equations
  • =
instance Finsupp.wellFoundedLT_of_finite {α : Type u_1} {N : Type u_2} [Zero N] [Finite α] [Preorder N] [WellFoundedLT N] :
Equations
  • =