Theorem·T04
Equivalence classes form a partition
An equivalence relation slices its set into disjoint classes covering it.
For every equivalence relation
on a set
, the quotient
is a partition of
; moreover, for all
:
In words
For every equivalence relation R on a set A, the quotient is a partition of A: the classes are non-empty, pairwise disjoint, and together cover A. Moreover, for any elements a and b, the class of a equals the class of b exactly when a is related to b.
Never needed: F05 · F06 · F08 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1
- 2The classes cover . Each is a subset of , so (D004, D001). Conversely each lies in by step 1, so . By Extensionality, .
- 3If then . Let , i.e. . From and transitivity, , so : thus . By symmetry of , also holds, and the same argument gives . Extensionality concludes .
- 4If then . By step 1, , and membership in means precisely (D021, substitutivity).
- 5
∎
Remarks
The fundamental theorem of equivalence relations. It has a converse: given a partition
of
, declaring
when
and
share a piece defines an equivalence relation whose classes are exactly the pieces of
; so equivalence relations and partitions are the same structure in two presentations. This theorem is the engine of every quotient construction, and its finite counting consequence (L27) is what makes Lagrange's theorem work.