English
If α and β are both IsTrichotomous with respect to r and s, then Prod.Lex r s is IsTrichotomous.
Русский
Если на α и β выполняются трихотомность по r и s соответственно, то лексикографическое произведение имеет три направления.
LaTeX
$$[IsTrichotomous α r] [IsTrichotomous β s] : IsTrichotomous (Prod α β) (Prod.Lex r s)$$
Lean4
instance IsTrichotomous [IsTrichotomous α r] [IsTrichotomous β s] : IsTrichotomous (α × β) (Prod.Lex r s) :=
⟨fun ⟨i, a⟩ ⟨j, b⟩ ↦ by
obtain hij | rfl | hji := trichotomous_of r i j
{ exact Or.inl (Lex.left _ _ hij)
}
{ exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _)
}
{ exact Or.inr (Or.inr <| Lex.left _ _ hji)
}⟩
