English
If r is a trichotomous relation on α, then the lexicographic order on List α is trichotomous.
Русский
Если отношение r тричотомно на α, то лексикографический порядок на List α тричотомен.
LaTeX
$$$\\mathrm{IsTrichotomous}(\\mathrm{List}\\,\\alpha, \\mathrm{List.Lex}\\ r).$$$
Lean4
instance isTrichotomous (r : α → α → Prop) [IsTrichotomous α r] : IsTrichotomous (List α) (Lex r) where
trichotomous := aux
where aux
| [], [] => Or.inr (Or.inl rfl)
| [], _ :: _ => Or.inl nil
| _ :: _, [] => Or.inr (Or.inr nil)
| a :: l₁, b :: l₂ => by
rcases trichotomous_of r a b with (ab | rfl | ab)
· exact Or.inl (rel ab)
· exact (aux l₁ l₂).imp cons (Or.imp (congr_arg _) cons)
· exact Or.inr (Or.inr (rel ab))
