English
If IsTrichotomous ι r and IsTrichotomous (α i) (s i) for all i, then Lex r s is trichotomous.
Русский
Если IsTrichotomous ι r и IsTrichotomous (α i) (s i) для всех i, то Lex r s тричотомичен.
LaTeX
$$$[IsTrichotomous ι r][\\forall i, IsTrichotomous (\\alpha i) (s i)] : IsTrichotomous ((i, \\alpha i)) (Sigma.Lex r s).$$$
Lean4
instance [IsTrichotomous ι r] [∀ i, IsTrichotomous (α i) (s i)] : IsTrichotomous _ (Lex r s) :=
⟨by
rintro ⟨i, a⟩ ⟨j, b⟩
obtain hij | rfl | hji := trichotomous_of r i j
· exact Or.inl (Lex.left _ _ hij)
· obtain hab | rfl | hba := trichotomous_of (s i) a b
· exact Or.inl (Lex.right _ _ hab)
· exact Or.inr (Or.inl rfl)
· exact Or.inr (Or.inr <| Lex.right _ _ hba)
· exact Or.inr (Or.inr <| Lex.left _ _ hji)⟩
