Transitive

• Transitive #Card
  • $y \in Rx$ and $z \in Ry \implies z \in Rx$ for all $x, y, z \in X$.

Back

$y \in Rx$ and $z \in Ry \implies z \in Rx$ for all $x, y, z \in X$.

Lean

IsTrans r / Transitive r := ∀ a b c, r a b → r b c → r a c