Finsupp.Lex.acc

theorem Finsupp.Lex.acc : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] {r : α → α → Prop} {s : N → N → Prop}, (∀ ⦃n : N⦄, ¬s n 0) → WellFounded s → ∀ (x : α →₀ N), (∀ a ∈ x.support, Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a) → Acc (Finsupp.Lex r s) x

The theorem `Finsupp.Lex.acc` states that for any types `α` and `N`, where `N` is an instance of `Zero`, and any relations `r` and `s` on `α` and `N` respectively, if for any `n` of type `N`, `s n 0` is not true and `s` is a well-founded relation, then for any function `x` from `α` to `N`, if all elements `a` in the support of `x` are accessible according to the infimum of the converse of `r` and the inequality relation, then `x` is accessible according to the lexicographic relation `Finsupp.Lex r s`. Here, accessibility (`Acc`) of a point in a relation refers to every point being related to a smaller point, the smaller point being related to an even smaller point, and so on, which guarantees the termination of a process built on the relation. The term "support of `x`" refers to the set of all points where `x` is non-zero. The "lexicographic relation" is a way to order pairs of elements: `(a, b)` is less than `(c, d)` in the lexicographic order if either `a < c` or `a = c` and `b < d`.

More concisely: If `r` is a well-founded relation on type `α`, `s` is a relation on type `N` (an instance of `Zero`), and for all `n` in `N`, `s n 0` is false, then for any function `x` from `α` to `N`, if all elements in the support of `x` are accessible according to the infimum of the converse of `r` and the inequality relation, then `x` is accessible according to the lexicographic relation `Finsupp.Lex r s`.