English
If the base relations and the coordinate relations are well-founded, then the Lex order on DFinsupp is well-founded.
Русский
Если базовые и координатные отношения хорошо основаны, то Lex порядок на DFinsupp хорошо основан.
LaTeX
$$$\\mathrm{WellFounded}(DFinsupp.Lex(r,s))$ given hbot, hs, hr$$
Lean4
instance wellFoundedLT [Finite ι] [∀ i, Preorder (α i)] [hw : ∀ i, WellFoundedLT (α i)] : WellFoundedLT (∀ i, α i) :=
⟨by
obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
· convert emptyWf.wf
letI : ∀ i, Zero (α i) := fun i => ⟨(hw i).wf.min ⊤ ⟨x i, trivial⟩⟩
haveI := Fintype.ofFinite ι
refine InvImage.wf equivFunOnFintype.symm (DFinsupp.wellFoundedLT fun i a => ?_).wf
exact (hw i).wf.not_lt_min ⊤ _ trivial⟩
