wellFoundedLT_of_finite — Mathlib

English

For a finite index set, DFinsupp.Lex with coordinatewise well-founded LT relations is well-founded.

Русский

Для конечного множества индексов DFinsupp.Lex с LT радиусами хорошо основано.

LaTeX

$$$\\mathrm{WellFoundedLT}(DFinsupp.Lex\\, (\\text{Π}_0 i, α_i))$$$

Lean4

instance wellFoundedLT_of_finite [Finite ι] [∀ i, Zero (α i)] [∀ i, Preorder (α i)] [∀ i, WellFoundedLT (α i)] :
    WellFoundedLT (Π₀ i, α i) :=
  have := Fintype.ofFinite ι
  ⟨InvImage.wf equivFunOnFintype Pi.wellFoundedLT.wf⟩

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