Loading [MathJax]/jax/output/CommonHTML/jax.js
ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Binary endorelation
Definition D288
Transitive binary relation
Formulation 0
A D4424: Binary endorelation B=(X×Y,R) is transitive if and only if x,y,zX((x,y),(y,z)R(x,z)R)
Formulation 1
A D4424: Binary endorelation B=(X×Y,R) is transitive if and only if x,y,zX(xRy,yRzxRz)