English
If hr: ∀ a b c, r₁₂ a b → r₂₃ b c → r₁₃ a c and RightTotal r₁₂ and RightTotal r₂₃ hold, then RightTotal r₁₃ holds.
Русский
Если связь между α–β и β–γ транситивна через r₁₃ и существуют правые полноты, то exists правыйTotal для r₁₃.
LaTeX
$$$ (\\forall a\\,b\\,c, r_{12} a b \\rightarrow r_{23} b c \\rightarrow r_{13} a c) \\rightarrow \\operatorname{RightTotal}(r_{12}) \\rightarrow \\operatorname{RightTotal}(r_{23}) \\rightarrow \\operatorname{RightTotal}(r_{13}) $$$
Lean4
protected theorem trans (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) :
RightTotal r₁₂ → RightTotal r₂₃ → RightTotal r₁₃ :=
swap <| LeftTotal.trans (fun _ _ _ ↦ swap <| hr _ _ _)
