English
If r and s are transitive, then the lexicographic product order Prod.Lex r s is transitive on α×β.
Русский
Если r и s транзитивны, то лексикографическое произведение Prod.Lex r s транзитивно на α×β.
LaTeX
$$[IsTrans α r] [IsTrans β s] : ∀ {x y z : α × β}, Prod.Lex r s x y → Prod.Lex r s y z → Prod.Lex r s x z$$
Lean4
@[trans]
theorem trans {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] :
∀ {x y z : α × β}, Prod.Lex r s x y → Prod.Lex r s y z → Prod.Lex r s x z
| (_, _), (_, _), (_, _), left _ _ hxy₁, left _ _ hyz₁ => left _ _ (_root_.trans hxy₁ hyz₁)
| (_, _), (_, _), (_, _), left _ _ hxy₁, right _ _ => left _ _ hxy₁
| (_, _), (_, _), (_, _), right _ _, left _ _ hyz₁ => left _ _ hyz₁
| (_, _), (_, _), (_, _), right _ hxy₂, right _ hyz₂ => right _ (_root_.trans hxy₂ hyz₂)
