English
If the index set is finite and each coordinate is well-founded, then the Lex order on the dependent finite-support functions is well-founded.
Русский
Если множество индексов конечное, а координаты хорошо основаны, то Lex-порядок над зависимыми функциями с конечной опорой хорошо основан.
LaTeX
$$$\\text{WellFounded}(DFinsupp.Lex(r,s))$ for finite index set ι with IsStrictTotalOrder ι r and hs$$
Lean4
instance wellFoundedLT [LT ι] [IsTrichotomous ι (· < ·)] [hι : WellFoundedGT ι] [∀ i, AddMonoid (α i)]
[∀ i, PartialOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)] [hα : ∀ i, WellFoundedLT (α i)] :
WellFoundedLT (Lex (Π₀ i, α i)) :=
⟨Lex.wellFounded' (fun _ a => (zero_le a).not_gt) (fun i => (hα i).wf) hι.wf⟩
