English
If α is trichotomous and β is total, then the lexicographic order Prod.Lex r s is total on α×β.
Русский
Если α тричотомно упорядочено и β полностью упорядочено, то лексикографический порядок на α×β тотален.
LaTeX
$$[IsTrichotomous α r] [IsTotal β s] : IsTotal (α × β) (Prod.Lex r s)$$
Lean4
instance isTotal_right {r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r] [IsTotal β s] :
IsTotal (α × β) (Prod.Lex r s) :=
⟨fun ⟨i, a⟩ ⟨j, b⟩ ↦ by
obtain hij | rfl | hji := trichotomous_of r i j
· exact Or.inl (.left _ _ hij)
· exact (total_of s a b).imp (.right _) (.right _)
· exact Or.inr (.left _ _ hji)⟩