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 : N → N → Prop} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : WellFounded s) (x : α →₀ N) (h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x x_1 : α) => x ≠ x_1) a) : Acc (Finsupp.Lex r s) 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 : N → N → Prop} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : WellFounded s) (hr : WellFounded (rᶜ ⊓ fun (x x_1 : α) => x ≠ x_1)) : WellFounded (Finsupp.Lex r s)

theorem Finsupp.Lex.wellFounded' {α : Type u_1} {N : Type u_2} [Zero N] {r : α → α → Prop} {s : N → N → Prop} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : WellFounded s) [IsTrichotomous α r] (hr : WellFounded (Function.swap r)) : WellFounded (Finsupp.Lex r s)

instance Finsupp.Lex.wellFoundedLT {α : Type u_3} {N : Type u_4} [LT α] [IsTrichotomous α fun (x x_1 : α) => x < x_1] [hα : WellFoundedGT α] [CanonicallyOrderedAddCommMonoid N] [hN : WellFoundedLT N] : WellFoundedLT (Lex (α →₀ N))

Equations

• (_ : WellFoundedLT (Lex (α →₀ N))) = (_ : IsWellFounded (Lex (α →₀ N)) fun (x x_1 : Lex (α →₀ N)) => x < x_1)

theorem Finsupp.Lex.wellFounded_of_finite {α : Type u_1} {N : Type u_2} (r : α → α → Prop) {s : N → N → Prop} [IsStrictTotalOrder α r] [Finite α] [Zero N] (hs : WellFounded s) : WellFounded (Finsupp.Lex r s)

theorem Finsupp.Lex.wellFoundedLT_of_finite {α : Type u_1} {N : Type u_2} [LinearOrder α] [Finite α] [Zero N] [LT N] [hwf : WellFoundedLT N] : WellFoundedLT (Lex (α →₀ N))

theorem Finsupp.wellFoundedLT {α : Type u_1} {N : Type u_2} [Zero N] [Preorder N] [WellFoundedLT N] (hbot : ∀ (n : N), ¬n < 0) : WellFoundedLT (α →₀ N)

instance Finsupp.wellFoundedLT' {α : Type u_1} {N : Type u_3} [CanonicallyOrderedAddCommMonoid N] [WellFoundedLT N] : WellFoundedLT (α →₀ N)

Equations

• (_ : WellFoundedLT (α →₀ N)) = (_ : WellFoundedLT (α →₀ N))

instance Finsupp.wellFoundedLT_of_finite {α : Type u_1} {N : Type u_2} [Finite α] [Zero N] [Preorder N] [WellFoundedLT N] : WellFoundedLT (α →₀ N)

Equations

• (_ : WellFoundedLT (α →₀ N)) = (_ : IsWellFounded (α →₀ N) fun (x x_1 : α →₀ N) => x < x_1)