wellFoundedLT — Mathlib

English

If α is linearly ordered and finite, and N has a well-founded LT, then Lex on α →₀ N is well-founded.

Русский

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

LaTeX

$$$WellFoundedLT (Lex (\alpha \to_{0} N))$$$

Lean4

instance wellFoundedLT {α N} [LT α] [IsTrichotomous α (· < ·)] [hα : WellFoundedGT α] [AddMonoid N] [PartialOrder N]
    [CanonicallyOrderedAdd N] [hN : WellFoundedLT N] : WellFoundedLT (Lex (α →₀ N)) :=
  ⟨Lex.wellFounded' (fun n => (zero_le n).not_gt) hN.wf hα.wf⟩

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