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