wellFoundedLT — Mathlib

English

If each coordinate has a well-founded linear order, then the Lex order on a family of such coordinates also has a well-founded linear extension.

Русский

Если каждое координатное множество имеет хорошо основанный линейный порядок, то Lex-порядок над семейством таких множеств тоже имеет хорошо основанный линейный продолжатель.

LaTeX

$$$\\text{WellFoundedLT}(\\mathrm{Lex}(\\Pi_0 i, \\alpha_i))$$$

Lean4

instance wellFoundedLT [LinearOrder ι] [Finite ι] [∀ i, LT (α i)] [hwf : ∀ i, WellFoundedLT (α i)] :
    WellFoundedLT (Lex (∀ i, α i)) :=
  ⟨Pi.Lex.wellFounded (· < ·) fun i => (hwf i).1⟩

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