wellFounded_of_finite — Mathlib

English

For a finite index set, the Lex order on dependent finitely supported functions is well-founded provided each coordinate is well-founded.

Русский

Для конечного множества индексов порядок Lex над зависимыми функциями с конечной опорой хорошо основан, если каждая координата хорошо основана.

LaTeX

$$$\\text{WellFounded}(DFinsupp.Lex(r,s))$ при конечном ι и $\\forall i,\\text{WellFounded}(s_i)$$$

Lean4

theorem wellFounded_of_finite [IsStrictTotalOrder ι r] [Finite ι] [∀ i, Zero (α i)] (hs : ∀ i, WellFounded (s i)) :
    WellFounded (DFinsupp.Lex r s) :=
  have := Fintype.ofFinite ι
  InvImage.wf equivFunOnFintype (Pi.Lex.wellFounded r hs)

Похожие утверждения