trans — Mathlib

English

Let p=(x,y), q=(u,v), r=(s,t) be elements of α×α. If p is related to q and q is related to r, then p is related to r.

Русский

Пусть p=(x,y), q=(u,v), r=(s,t) принадлежат α×α. Если p связано с q и q связано с r, тогда p связано с r.

LaTeX

$$$$ \forall x,y,z \in \alpha \times \alpha,\ Rel\,\alpha\,x\,y \to Rel\,\alpha\,y\,z \to Rel\,\alpha\,x\,z. $$$$

Lean4

@[trans]
theorem trans {x y z : α × α} (a : Rel α x y) (b : Rel α y z) : Rel α x z := by aesop (rule_sets := [Sym2])

Похожие утверждения