English
If r on α and s on β are trichotomous, then the lexicographic order on α ⊕ β is trichotomous. For any two elements there is a clear comparison: left-left, left-right, or right-right cases resolved by r or s.
Русский
Если r на α и s на β тричотомны, то лексикографический порядок на α ⊕ β тричотомен: для любых двух элементов существует однозначное сравнение, определяемое r или s.
LaTeX
$$$\operatorname{IsTrichotomous}(\alpha \oplus \beta, \mathrm{Lex}(r,s))$$$
Lean4
instance [IsTrichotomous α r] [IsTrichotomous β s] : IsTrichotomous (α ⊕ β) (Lex r s) :=
⟨fun a b =>
match a, b with
| inl a, inl b => (trichotomous_of r a b).imp3 Lex.inl (congr_arg _) Lex.inl
| inl _, inr _ => Or.inl (Lex.sep _ _)
| inr _, inl _ => Or.inr (Or.inr <| Lex.sep _ _)
| inr a, inr b => (trichotomous_of s a b).imp3 Lex.inr (congr_arg _) Lex.inr⟩
