English
If hr: ∀ a b c, r₁₂ a b → r₂₃ b c → r₁₃ a c and BiTotal r₁₂ and BiTotal r₂₃ hold, then BiTotal r₁₃ holds.
Русский
Если r₁₂ и r₂₃ связаны через r₁₃ и существуют обе стороны BiTotal, тогда BiTotal r₁₃.
LaTeX
$$$ (\\forall a\\,b\\,c, r_{12} a b \\rightarrow r_{23} b c \\rightarrow r_{13} a c) \\rightarrow \\operatorname{BiTotal}(r_{12}) \\rightarrow \\operatorname{BiTotal}(r_{23}) \\rightarrow \\operatorname{BiTotal}(r_{13}) $$$
Lean4
protected theorem trans (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) :
BiTotal r₁₂ → BiTotal r₂₃ → BiTotal r₁₃ := fun h₁ h₂ ↦ ⟨h₁.1.trans hr h₂.1, h₁.2.trans hr h₂.2⟩
