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 D178
Equivalence relation
Formulation 0
A D4424: Binary endorelation $(X \times X, R)$ is an equivalence relation if and only if
(1) \begin{equation} \forall \, x \in X : (x, x) \in R \end{equation} D287: Reflexive binary relation
(2) \begin{equation} \forall \, x, y \in X \left( (x, y) \in R \quad \implies \quad (y, x) \in R \right) \end{equation} D294: Symmetric binary relation
(3) \begin{equation} \forall \, x, y, z \in R \left( (x, y), (y, z) \in R \quad \implies \quad (x, z) \in R \right) \end{equation} D288: Transitive binary relation
Formulation 1
A D4424: Binary endorelation $(X \times X, R)$ is an equivalence relation if and only if
(1) \begin{equation} \forall \, x \in X : x R x \end{equation} D287: Reflexive binary relation
(2) \begin{equation} \forall \, x, y \in X \left( x R y \quad \implies \quad y R x \right) \end{equation} D294: Symmetric binary relation
(3) \begin{equation} \forall \, x, y, z \in R \left( x R y, y R z \quad \implies \quad x R z \right) \end{equation} D288: Transitive binary relation