English
For a finite index set, the Lex order on the Pi-type with coordinatewise well-founded relations is well-founded.
Русский
Для конечного множества индексов порядок Lex на типе Pi с координатно хорошо основанными отношениями тоже хорошо основан.
LaTeX
$$$\\mathrm{WellFounded}\\big(\\mathrm{Pi.Lex}(r, (\\lambda i. s_i))\\big)$$$
Lean4
theorem wellFounded [IsStrictTotalOrder ι r] [Finite ι] (hs : ∀ i, WellFounded (s i)) :
WellFounded (Pi.Lex r (fun {i} ↦ s i)) :=
by
obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
· convert emptyWf.wf
letI : ∀ i, Zero (α i) := fun i => ⟨(hs i).min ⊤ ⟨x i, trivial⟩⟩
haveI := IsTrans.swap r; haveI := IsIrrefl.swap r; haveI := Fintype.ofFinite ι
refine InvImage.wf equivFunOnFintype.symm (Lex.wellFounded' (fun i a => ?_) hs ?_)
exacts [(hs i).not_lt_min ⊤ _ trivial, Finite.wellFounded_of_trans_of_irrefl (Function.swap r)]
