wellFoundedLT — Mathlib

English

If α is finite and has LT, then the lexicographic order on α →₀ N is well-founded.

Русский

Если α конечно и имеет LT, то лексикографический порядок на α →₀ N хорошо основан.

LaTeX

$$$WellFoundedLT (Lex (\alpha →_{0} N))$$$

Lean4

protected theorem wellFoundedLT [Preorder N] [WellFoundedLT N] (hbot : ∀ n : N, ¬n < 0) : WellFoundedLT (α →₀ N) :=
  ⟨InvImage.wf toDFinsupp (DFinsupp.wellFoundedLT fun _ a => hbot a).wf⟩

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