English
If r and s are transitive, then LiftRel r s is transitive on α ⊕ β; composition respects the Sum structure.
Русский
Если r и s транзитивны, то LiftRel r s транзитивно на α ⊕ β; композиции сохраняют структуру суммы.
LaTeX
$$$[IsTrans\\; α\\ r] [IsTrans\\; β\\ s] ⇒ \\forall {a b c}, LiftRel r s a b → LiftRel r s b c → LiftRel r s a c$$$
Lean4
@[trans]
theorem trans [IsTrans α r] [IsTrans β s] : ∀ {a b c}, LiftRel r s a b → LiftRel r s b c → LiftRel r s a c
| _, _, _, LiftRel.inl hab, LiftRel.inl hbc => LiftRel.inl <| _root_.trans hab hbc
| _, _, _, LiftRel.inr hab, LiftRel.inr hbc => LiftRel.inr <| _root_.trans hab hbc
