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