English
If α and β are types equipped with well-orders r and s, then the product α × β endowed with the lexicographic order Prod.Lex r s is a well-order.
Русский
Если $\alpha$ и $\beta$ — типы, на которых определены хорошо упорядочения $r$ и $s$, соответственно, то произведение $\alpha\times\beta$ с лексикографическим порядком $\mathrm{Prod.Lex}\,r\,s$ является хорошо упорядоченным.
LaTeX
$$$IsWellOrder(\\alpha \\times \\beta) (Prod.Lex r s)$$$
Lean4
instance [IsWellOrder α r] [IsWellOrder β s] : IsWellOrder (α × β) (Prod.Lex r s)
where
trichotomous := fun ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ =>
match @trichotomous _ r _ a₁ b₁ with
| Or.inl h₁ => Or.inl <| Prod.Lex.left _ _ h₁
| Or.inr (Or.inr h₁) => Or.inr <| Or.inr <| Prod.Lex.left _ _ h₁
| Or.inr (Or.inl (.refl _)) =>
match @trichotomous _ s _ a₂ b₂ with
| Or.inl h => Or.inl <| Prod.Lex.right _ h
| Or.inr (Or.inr h) => Or.inr <| Or.inr <| Prod.Lex.right _ h
| Or.inr (Or.inl (.refl _)) => Or.inr <| Or.inl rfl
trans a b c h₁
h₂ := by
rcases h₁ with ⟨a₂, b₂, ab⟩ | ⟨a₁, ab⟩ <;> rcases h₂ with ⟨c₁, c₂, bc⟩ | ⟨c₂, bc⟩
exacts [.left _ _ (_root_.trans ab bc), .left _ _ ab, .left _ _ bc, .right _ (_root_.trans ab bc)]
