wellFoundedLT — Mathlib

English

If each component is well-founded in the strict total order sense, then the Lex order on the function space ι → α is well-founded.

Русский

Если каждое звено хорошо основано в виде строгого полного порядка, то Lex-порядок на пространстве функций ι → α хорошо основан.

LaTeX

$$$\\mathrm{WellFoundedLT}(\\mathrm{Function.Lex}(r))$$$

Lean4

instance wellFoundedLT {α} [LinearOrder ι] [Finite ι] [LT α] [WellFoundedLT α] : WellFoundedLT (Lex (ι → α)) :=
  Pi.Lex.wellFoundedLT

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