English
If α is well-founded under a relation r, and the index function s is well-founded, then the homogeneous lexicographic order on α →₀ ℕ is well-founded.
Русский
Если множество α имеет хорошо основанный порядок по отношению r, и функция индексов s хорошо основана, тогда однородный лексикографический порядок на α→₀ ℕ хорошо основан.
LaTeX
$$$\text{WellFounded}\left(\mathrm{Finsupp.DegLex}\, r\, s\right)$$$
Lean4
theorem wellFounded {r : α → α → Prop} [IsTrichotomous α r] (hr : WellFounded (Function.swap r)) {s : ℕ → ℕ → Prop}
(hs : WellFounded s) (hs0 : ∀ ⦃n⦄, ¬s n 0) : WellFounded (Finsupp.DegLex r s) :=
by
have wft := WellFounded.prod_lex hs (Finsupp.Lex.wellFounded' hs0 hs hr)
rw [← Set.wellFoundedOn_univ] at wft
unfold Finsupp.DegLex
rw [← Set.wellFoundedOn_range]
exact Set.WellFoundedOn.mono wft (le_refl _) (fun _ _ ↦ trivial)
