Equivalence relation

When defining types of objects, we often want to define a new notion of equality. For example, we have already defined equality for pairs, sets, functions, and cardinalities.

Whenever you redefine a familiar definition or operation, it is important not to change the fundamental properties that peoBold textple expect of that operation: people should still be able to reason about your operator the way they always have.

The properties that people expect "equals" to have are defined below; relations that satisfy all three are called equivalence relations. You should always check these properties if you ever define something called "equals" (for example, when overriding the `.equals()` method in Java or the `__eq__` method in Python).

Reflexivity

Definition: Reflexive

In a picture, this means that every element of has a self-loop: an edge back to itself.

Symmetry

Definition: Symmetric
A binary relation on a set is symmetric if for all pairs of elements and with , we also have .

In a picture, this means that every edge from to has a corresponding edge from back to .

Transitivity

Definition: Transitive
A binary relation on a set is transitive if for all elements , , and with and , we also have .

In a picture, this means that every path from to has a corresponding direct edge from to .

Equivalence relation

Reflexivity lets you plug in definitions to show that things are equal (for example, it lets you conclude that ). Symmetry lets you use equality in both directions (e.g. since x = y, we know that "... = y = x = ..."). Transitivity lets you chain together statements. (For example, we often write things like ", so ").