wellFoundedLT_of_finite — Mathlib

English

If α is finite and IsStrictTotalOrder r and s is well-founded, then Finsupp.Lex r s is well-founded.

Русский

Если α конечно и есть строгий полный порядок r и s хорошо основан, то Finsupp.Lex r s хорошо основан.

LaTeX

$$$WellFounded (Finsupp.Lex r s)$$$

Lean4

theorem wellFoundedLT_of_finite [LinearOrder α] [Finite α] [LT N] [hwf : WellFoundedLT N] :
    WellFoundedLT (Lex (α →₀ N)) :=
  ⟨Finsupp.Lex.wellFounded_of_finite (· < ·) hwf.1⟩

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