instIsTotalLex — Mathlib

English

If r on α and s on β are total, then the lexicographic order on α ⊕ β is total; every pair is comparable under Lex.

Русский

Если r на α и s на β суммарно-совокупны, то лексикографический порядок на α ⊕ β конечно (полон): любая пара элементов сравнима.

LaTeX

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

Lean4

instance [IsTotal α r] [IsTotal β s] : IsTotal (α ⊕ β) (Lex r s) :=
  ⟨fun a b =>
    match a, b with
    | inl a, inl b => (total_of r a b).imp Lex.inl Lex.inl
    | inl _, inr _ => Or.inl (Lex.sep _ _)
    | inr _, inl _ => Or.inr (Lex.sep _ _)
    | inr a, inr b => (total_of s a b).imp Lex.inr Lex.inr⟩

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