linearOrder — Mathlib

English

If α and β are linearly ordered, then the Lex construction on their sum α ⊕ β is a linear order.

Русский

Если α и β образуют линейный порядок, то лексикографическое суммирование даёт линейный порядок.

LaTeX

$$$\\text{LinearOrder}(\\alpha \\oplus_ℓ \\beta)$$$

Lean4

instance linearOrder [LinearOrder α] [LinearOrder β] : LinearOrder (α ⊕ₗ β) :=
  { Lex.partialOrder with le_total := total_of (Lex (· ≤ ·) (· ≤ ·)), toDecidableLE := instDecidableRelSumLex,
    toDecidableLT := instDecidableRelSumLex, toDecidableEq := instDecidableEqSum }

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