mathlib3 documentation

data.finsupp.well_founded

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

finsupp.lex.well_founded 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.well_founded_lt_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.well_founded_lt and well_founded_lt_of_finite state the same results for the product order (<), but without the ordering conditions on α.

All results are transferred from dfinsupp via finsupp.to_dfinsupp.

source
theorem finsupp.lex.acc {α : Type u_1} {N : Type u_2} [hz : has_zero N] {r : α → α → Prop} {s : N → N → Prop} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : well_founded s) (x : α →₀ N) (h : ∀ (a : α), a ∈ x.support → acc (rᶜ ⊓ ne) 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ᶜ ⊓ (≠).

source
theorem finsupp.lex.well_founded {α : Type u_1} {N : Type u_2} [hz : has_zero N] {r : α → α → Prop} {s : N → N → Prop} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : well_founded s) (hr : well_founded (rᶜ ⊓ ne)) :
well_founded (finsupp.lex r s)
source
theorem finsupp.lex.well_founded' {α : Type u_1} {N : Type u_2} [hz : has_zero N] {r : α → α → Prop} {s : N → N → Prop} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : well_founded s) [is_trichotomous α r] (hr : well_founded (function.swap r)) :
well_founded (finsupp.lex r s)
source
@[protected, instance]
def finsupp.lex.well_founded_lt {α : Type u_1} {N : Type u_2} [has_lt α] [is_trichotomous α has_lt.lt] [hα : well_founded_gt α] [canonically_ordered_add_monoid N] [hN : well_founded_lt N] :
well_founded_lt (lex (α →₀ N))
source
theorem finsupp.lex.well_founded_of_finite {α : Type u_1} {N : Type u_2} (r : α → α → Prop) {s : N → N → Prop} [is_strict_total_order α r] [finite α] [has_zero N] (hs : well_founded s) :
well_founded (finsupp.lex r s)
source
theorem finsupp.lex.well_founded_lt_of_finite {α : Type u_1} {N : Type u_2} [linear_order α] [finite α] [has_zero N] [has_lt N] [hwf : well_founded_lt N] :
well_founded_lt (lex (α →₀ N))
source
@[protected]
theorem finsupp.well_founded_lt {α : Type u_1} {N : Type u_2} [has_zero N] [preorder N] [well_founded_lt N] (hbot : ∀ (n : N), ¬n < 0) :
well_founded_lt (α →₀ N)
source
@[protected, instance]
def finsupp.well_founded_lt' {α : Type u_1} {N : Type u_2} [canonically_ordered_add_monoid N] [well_founded_lt N] :
well_founded_lt (α →₀ N)
source
@[protected, instance]
def finsupp.well_founded_lt_of_finite {α : Type u_1} {N : Type u_2} [finite α] [has_zero N] [preorder N] [well_founded_lt N] :
well_founded_lt (α →₀ N)