# 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 : ) (x : α →₀ N) (h : ∀ (a : α), a x.supportAcc (r fun x x_1 => x x_1) a) :
Acc () x

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 : ) (hr : WellFounded (r fun x x_1 => x x_1)) :
theorem Finsupp.Lex.wellFounded' {α : Type u_1} {N : Type u_2} [Zero N] {r : ααProp} {s : NNProp} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : ) [] (hr : ) :
instance Finsupp.Lex.wellFoundedLT {α : Type u_3} {N : Type u_4} [LT α] [IsTrichotomous α fun x x_1 => x < x_1] [hα : ] [hN : ] :
theorem Finsupp.Lex.wellFounded_of_finite {α : Type u_1} {N : Type u_2} (r : ααProp) {s : NNProp} [] [] [Zero N] (hs : ) :
theorem Finsupp.Lex.wellFoundedLT_of_finite {α : Type u_1} {N : Type u_2} [] [] [Zero N] [LT N] [hwf : ] :
theorem Finsupp.wellFoundedLT {α : Type u_1} {N : Type u_2} [Zero N] [] [] (hbot : ∀ (n : N), ¬n < 0) :
instance Finsupp.wellFoundedLT' {α : Type u_1} {N : Type u_3} [] :
instance Finsupp.wellFoundedLT_of_finite {α : Type u_1} {N : Type u_2} [] [Zero N] [] [] :