instIsWellOrderLex — Mathlib

English

If α and β are well-ordered by r and s, then α ⊕ β with Lex r s is well-ordered. Every nonempty subset has a least element with respect to Lex.

Русский

Если α и β хорошо упорядочены по r и s соответственно, то α ⊕ β с порядком Lex r s хорошо упорядочено: у каждого непустого подмножества есть наименьший элемент относительно Lex.

LaTeX

$$$\operatorname{IsWellOrder}(\alpha \oplus \beta, \mathrm{Lex}(r,s))$$$

Lean4

instance [IsWellOrder α r] [IsWellOrder β s] : IsWellOrder (α ⊕ β) (Sum.Lex r s) where
  wf := Sum.lex_wf IsWellFounded.wf IsWellFounded.wf

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