Relations, equivalence relations and partitions

Lens

MotivationH

Sorting by sameness

A teacher in Nairobi wants to celebrate birthdays, so she groups her class by birth month. A librarian in Montevideo shelves books by the first letter of the author's surname. A train timetable in Delhi treats 14:00 and 2 p.m. as the same time, and a recipe treats $\tfrac{1}{2}$ cup and $\tfrac{2}{4}$ cup as the same amount.

Each time, a rule says when two things are “the same in some respect” — and then everything can be sorted into boxes, with every item in exactly one box.

But not every rule of the form “these two are alike” sorts so neatly. Try grouping people by “lives within 1 km of each other”: Amara lives 1 km east of Bongani, and Bongani 1 km east of Chen, so Amara and Bongani belong together, and Bongani and Chen belong together — yet Amara and Chen are 2 km apart. Which box does Bongani go in?

This lesson finds the three properties that make a sameness rule sort cleanly, and proves that such rules and ways of splitting a set into boxes are really one idea, seen from two sides.

IntuitionH

A relation is a yes-or-no question about pairs

A relation on a set answers a yes-or-no question for every pair of its elements: is $a$ related to $b$ ? Take the set $A = \{1, 2, 3, 4\}$ and the question “does $a$ divide $b$ ?”. The pairs that answer yes are

(1,1),\ (1,2),\ (1,3),\ (1,4),\ (2,2),\ (2,4),\ (3,3),\ (4,4).

We can show the same information in three ways: as this set of ordered pairs, as a table with a mark in row $a$ , column $b$ whenever $a$ is related to $b$ , or as an arrow diagram with an arrow from $a$ to $b$ (a little loop when $a$ is related to itself).

The relation “a divides b” on {1, 2, 3, 4}, twice. Left: a table, with a gold dot in row a, column b when a divides b. Right: an arrow diagram; every number has a loop because every number divides itself.

Three questions about any relation turn out to matter most, and each has a picture in the arrow diagram:

Does every element have a loop? (Is everything related to itself?)
Does every arrow have a return arrow? (If $a$ is related to $b$ , is $b$ related to $a$ ?)
Does every two-step path have a shortcut? (If $a \to b \to c$ , is there an arrow $a \to c$ ?)

DefinitionsH

Definitions

Definition— relation

A relation $R$ on a set $A$ is a subset of the Cartesian product $A \times A$ , that is, a set of ordered pairs of elements of $A$ . We write $a \mathrel{R} b$ , read “ $a$ is related to $b$ ”, when $(a, b) \in R$ .

Order matters in a pair: $(1, 2)$ and $(2, 1)$ are different pairs (see sets), so a relation can contain one without the other.

Definition— reflexive, symmetric, transitive

A relation $R$ on $A$ is

reflexive if $a \mathrel{R} a$ for every $a \in A$ ;
symmetric if whenever $a \mathrel{R} b$ , also $b \mathrel{R} a$ ;
transitive if whenever $a \mathrel{R} b$ and $b \mathrel{R} c$ , also $a \mathrel{R} c$ .

Definition— equivalence relation

An equivalence relation is a relation that is reflexive, symmetric and transitive. Equivalence relations are often written $\sim$ (“tilde”), and $a \sim b$ is read “ $a$ is equivalent to $b$ ”.

Definition— equivalence class

If $\sim$ is an equivalence relation on $A$ and $a \in A$ , the equivalence class of $a$ is the set of everything equivalent to $a$ :

[a] = \{\, x \in A \mid x \sim a \,\}.

Definition— partition

A partition of a set $A$ is a collection of subsets of $A$ , called blocks, such that

every block is non-empty;
every element of $A$ lies in some block;
different blocks are disjoint: they have no element in common.

Conditions 2 and 3 together say: every element of $A$ lies in exactly one block. That is precisely what a teacher's birthday boxes achieve.

Note

To show that a relation has one of the three properties, we must check every case. To show that it fails a property, one counterexample is enough: a single element without a loop, a single arrow without its return, or a single two-step path without its shortcut.

Worked examplesH

Examples and non-examples

Example— Testing six relations

Relation	Set	Reflexive?	Symmetric?	Transitive?
same remainder on division by 3	$\Z$	yes	yes	yes
same birth month	people	yes	yes	yes
$a$ divides $b$	$\{1, \dots, 6\}$	yes	no: $1 \mid 2$ , but $2 \nmid 1$	yes
$a < b$	$\Z$	no: $0 \not< 0$	no: $0 < 1$ , but $1 \not< 0$	yes
differ by at most 1	$\Z$	yes	yes	no: $0, 1$ and $1, 2$ , but not $0, 2$
is a sibling of	people	no	yes	no

Only the first two are equivalence relations. The last row has a subtle failure of transitivity: if Ana and Ben are siblings, then Ana is a sibling of Ben and Ben is a sibling of Ana — but Ana is not her own sibling.

Example— Finding the classes

On $\Z$ , let $a \sim b$ mean “ $a$ and $b$ leave the same remainder on division by $3$ ”. Remainders on division by $3$ are $0$ , $1$ or $2$ , also for negative numbers: $-1 = 3 \cdot (-1) + 2$ has remainder $2$ . So

\begin{aligned} [0] &= \{\dots, -6, -3, 0, 3, 6, \dots\},\\ [1] &= \{\dots, -5, -2, 1, 4, 7, \dots\},\\ [2] &= \{\dots, -4, -1, 2, 5, 8, \dots\}. \end{aligned}

Every class has many names: $[2] = [5] = [-1]$ , because $2 \sim 5 \sim -1$ . A class is a set, and any of its members can be used to name it.

Example— From a table to a partition

The relation $\{(0,0), (1,1), (2,2), (0,1), (1,0)\}$ on $\{0, 1, 2\}$ is an equivalence relation (check the three properties — there are only $3 + 9 + 27$ cases). Its classes are $[0] = [1] = \{0, 1\}$ and $[2] = \{2\}$ , so it splits the set into the partition $\{\{0, 1\}, \{2\}\}$ .

Example— From a partition to a relation

The partition $\{\{1, 4\}, \{2\}, \{3, 5\}\}$ of $\{1, 2, 3, 4, 5\}$ defines the relation “lies in the same block as”. Its pairs are all pairs from the same block:

(1,1), (1,4), (4,1), (4,4),\quad (2,2),\quad (3,3), (3,5), (5,3), (5,5).

A block with $k$ elements contributes $k \cdot k$ ordered pairs, so there are $4 + 1 + 4 = 9$ pairs in all.

ProofH

Classes, partitions and remainders

Throughout, $\sim$ is an equivalence relation on a set $A$ .

Theorem— Lemma 1 (every element is in its own class)

For every $a \in A$ , $a \in [a]$ . In particular, every class is non-empty.

Proof

$a \sim a$ by reflexivity, so $a \in [a]$ .

∎

Theorem— Lemma 2 (equivalent elements have equal classes)

If $a \sim b$ , then $[a] = [b]$ .

Proof

Two sets are equal when they have the same elements, so we show each is a subset of the other.

If $x \in [a]$ , then $x \sim a$ ; together with $a \sim b$ , transitivity gives $x \sim b$ , so $x \in [b]$ .

If $x \in [b]$ , then $x \sim b$ . By symmetry $b \sim a$ , and transitivity gives $x \sim a$ , so $x \in [a]$ .

∎

Theorem— Theorem 1 (equal or disjoint)

Any two equivalence classes $[a]$ and $[b]$ are either equal or disjoint.

Proof

Suppose $[a]$ and $[b]$ are not disjoint: some $x$ lies in both. Then $x \sim a$ and $x \sim b$ . By symmetry $a \sim x$ , and by transitivity $a \sim b$ . By Lemma 2, $[a] = [b]$ . So if two classes share even one element, they are equal.

∎

Theorem— Theorem 2 (the classes form a partition)

The equivalence classes of $\sim$ form a partition of $A$ .

Proof

Check the three conditions. Every class is non-empty and every element $a$ lies in a class, namely $[a]$ (Lemma 1). Different classes are disjoint by Theorem 1.

∎

Now go the other way, starting from boxes instead of a rule.

Theorem— Theorem 3 (every partition comes from exactly one equivalence relation)

Let $P$ be a partition of $A$ , and say $a \approx b$ when $a$ and $b$ lie in the same block. Then $\approx$ is an equivalence relation whose classes are exactly the blocks of $P$ , and it is the only equivalence relation with those classes.

Proof

Reflexive: every $a$ lies in some block $B$ , so $a$ and $a$ lie in the same block. Symmetric: “ $a$ and $b$ lie in a common block” says the same as “ $b$ and $a$ lie in a common block”. Transitive: suppose $a, b \in B$ and $b, c \in C$ for blocks $B$ and $C$ . The blocks $B$ and $C$ share the element $b$ , so they are not disjoint, and therefore $B = C$ . So $a$ and $c$ both lie in $B$ .

The classes are the blocks: if $a$ lies in the block $B$ , then $[a]$ is the set of $x$ that share a block with $a$ . Since $a$ lies in exactly one block, that block is $B$ , so $[a] = B$ .

Only one: if $\sim$ is any equivalence relation whose classes are the blocks of $P$ , then $a \sim b$ means $a \in [b]$ , which means $a$ and $b$ lie in the same class — the same block. So $\sim$ is $\approx$ .

∎

So equivalence relations on $A$ and partitions of $A$ are two descriptions of the same thing: a rule for “the same” gives boxes, boxes give a rule for “the same”, and doing one after the other brings you back where you started.

Theorem— Theorem 4 (remainders)

Let $n \ge 1$ . On $\Z$ , the relation “ $a$ and $b$ have the same remainder on division by $n$ ” is an equivalence relation with exactly $n$ classes, namely $[0], [1], \dots, [n-1]$ .

Proof

Write $r(a)$ for the remainder of $a$ on division by $n$ : the unique number $r$ with $0 \le r \le n - 1$ and $a = qn + r$ for some integer $q$ . The relation is “ $r(a) = r(b)$ ”. Equality of remainders is reflexive ( $r(a) = r(a)$ ), symmetric (if $r(a) = r(b)$ then $r(b) = r(a)$ ) and transitive (if $r(a) = r(b)$ and $r(b) = r(c)$ then $r(a) = r(c)$ ).

At most $n$ classes: every integer $a$ has some remainder $r$ with $0 \le r \le n - 1$ , and $r(r) = r$ (because $r = 0 \cdot n + r$ ), so $a \sim r$ and $a \in [r]$ . So every class is one of $[0], [1], \dots, [n-1]$ .

At least $n$ classes: if $0 \le r, s \le n - 1$ and $[r] = [s]$ , then $r \sim s$ , so $r = r(r) = r(s) = s$ . So these $n$ classes are all different.

∎

The same proof works for any rule of the form “ $f(a) = f(b)$ ”, where $f$ is a function on $A$ : same birth month, same first letter, same last digit, same remainder. And every equivalence relation is of this form — take $f(a) = [a]$ , the function that sends each element to its own class.

Formal mathematicsF

The proofs, checked by Lean

In Lean, a relation on a type α is a function R : α → α → Prop: give it two elements and it returns the statement “they are related”. That holds the same information as a set of ordered pairs. Here are the three properties:

ReflexiveLean 4Formally verified

/-- A relation is **reflexive** if every element is related to itself: `a R a` for all `a`. -/
def Reflexive {α : Type} (R : α → α → Prop) : Prop := ∀ a, R a a

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

SymmetricLean 4Formally verified

/-- A relation is **symmetric** if `a R b` always implies `b R a`. -/
def Symmetric {α : Type} (R : α → α → Prop) : Prop := ∀ a b, R a b → R b a

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

TransitiveLean 4Formally verified

/-- A relation is **transitive** if `a R b` and `b R c` always imply `a R c`. -/
def Transitive {α : Type} (R : α → α → Prop) : Prop := ∀ a b c, R a b → R b c → R a c

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

On a finite set, Lean can check a property by running through every case. Here is the relation from the “table to partition” example:

tableRelLean 4Formally verified

/-- A relation on the three-element set `{0, 1, 2}`, given as a list of ordered pairs:
`{(0,0), (1,1), (2,2), (0,1), (1,0)}`. `a` is related to `b` when the list contains `(a, b)`. -/
def tableRel (a b : Fin 3) : Prop :=
  [(0, 0), (1, 1), (2, 2), (0, 1), (1, 0)].contains (a, b) = true

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

table_exampleLean 4Proved here from basic factsFormally verified

/-- `tableRel` is an equivalence relation (its classes are `{0, 1}` and `{2}`). Lean checks all
three properties by running through every case: `3` cases for reflexivity, `9` for symmetry and
`27` for transitivity. On a finite set, checking every case *is* a proof. -/
theorem table_example : Reflexive tableRel ∧ Symmetric tableRel ∧ Transitive tableRel := by
  unfold Reflexive Symmetric Transitive tableRel
  decide

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

To show that a property fails, one counterexample is enough — and Lean wants us to name it:

lt_not_symmetricLean 4Proved here from basic factsFormally verified

/-- "Is less than" is not symmetric. One counterexample suffices: `0 < 1` but not `1 < 0`. -/
theorem lt_not_symmetric : ¬ Symmetric (fun a b : Int => a < b) := by
  intro h
  have h10 : (1 : Int) < 0 := h 0 1 (by decide)
  exact absurd h10 (by decide)

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

near_not_transitiveLean 4Proved here from basic factsFormally verified

/-- … but not transitive: `0` is near `1` and `1` is near `2`, yet `0` is not near `2`.
So "differ by at most 1" is **not** an equivalence relation. -/
theorem near_not_transitive : ¬ Transitive Near := by
  intro h
  have h02 : Near 0 2 := h 0 1 2 ⟨by decide, by decide⟩ ⟨by decide, by decide⟩
  exact absurd h02.2 (by decide)

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

symm_trans_not_reflLean 4Proved here from basic factsFormally verified

/-- A tempting false "proof": from `a R b`, symmetry gives `b R a`, and transitivity gives `a R a`.
The flaw is the first step — there may be no `b` with `a R b` at all. Here is a relation on the
natural numbers that is symmetric and transitive but not reflexive: `a R b` means `a = 0 ∧ b = 0`.
The number `1` is related to nothing, not even to itself. -/
theorem symm_trans_not_refl :
    ∃ R : Nat → Nat → Prop, Symmetric R ∧ Transitive R ∧ ¬ Reflexive R := by
  refine ⟨fun a b => a = 0 ∧ b = 0, ?_, ?_, ?_⟩
  · intro a b ⟨ha, hb⟩
    exact ⟨hb, ha⟩
  · intro a b c ⟨ha, _⟩ ⟨_, hc⟩
    exact ⟨ha, hc⟩
  · intro h
    exact absurd (h 1).1 (by decide)

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

refl_of_symm_transLean 4Proved here from basic factsFormally verified

/-- The tempting argument *does* work when every element is related to **something**:
pick `b` with `a R b`; symmetry gives `b R a`; transitivity gives `a R a`. -/
theorem refl_of_symm_trans {α : Type} (R : α → α → Prop) (hs : Symmetric R) (ht : Transitive R)
    (hsome : ∀ a, ∃ b, R a b) : Reflexive R := by
  intro a
  obtain ⟨b, hab⟩ := hsome a
  exact ht a b a hab (hs a b hab)

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

Now the main theorems. A set of elements of α is represented as a predicate α → Prop, so the class of a is the predicate “is related to a”. Two sets are equal when they have the same members; in Lean that step is funext followed by propext.

clsLean 4Formally verified

/-- The **equivalence class** of `a`: the set `[a] = {x | x R a}`, represented as a predicate.
`cls R a x` says "x belongs to the class of a". -/
def cls {α : Type} (R : α → α → Prop) (a : α) : α → Prop := fun x => R x a

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

cls_eq_of_relLean 4Proved here from basic factsFormally verified

/-- If `a R b` then `[a] = [b]`. If `x R a`, then `x R b` by transitivity; if `x R b`, then
`b R a` (symmetry) and transitivity give `x R a`. Two sets with the same members are equal
(`funext` and `propext` express this in Lean). -/
theorem cls_eq_of_rel {α : Type} {R : α → α → Prop} (h : Equivalence R) {a b : α} (hab : R a b) :
    cls R a = cls R b := by
  funext x
  apply propext
  constructor
  · intro hxa
    exact h.trans hxa hab
  · intro hxb
    exact h.trans hxb (h.symm hab)

Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

cls_eq_or_disjointLean 4Proved here from basic factsFormally verified

/-- **Two equivalence classes are either equal or disjoint.** Either `a R b`, and then
`[a] = [b]`; or not, and then no `x` can lie in both — otherwise `a R x` (symmetry) and `x R b`
would give `a R b` (transitivity). The case split uses the law of excluded middle. -/
theorem cls_eq_or_disjoint {α : Type} {R : α → α → Prop} (h : Equivalence R) (a b : α) :
    cls R a = cls R b ∨ ∀ x, ¬ (cls R a x ∧ cls R b x) := by
  cases Classical.em (R a b) with
  | inl hab => exact Or.inl (cls_eq_of_rel h hab)
  | inr hnot =>
    right
    intro x ⟨hxa, hxb⟩
    exact hnot (h.trans (h.symm hxa) hxb)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

A partition is a family P of subsets (P B means “B is a block”) satisfying our three conditions, with condition 3 in the form “two blocks that share an element are equal”, which says the same thing:

IsPartitionLean 4Formally verified

/-- A family `P` of subsets of `α` is a **partition** of `α` if every block is non-empty, every
element lies in some block, and two blocks that share an element are equal (equivalently:
different blocks are disjoint). Here a subset is a predicate `B : α → Prop`, and `P B` says
"`B` is one of the blocks". -/
structure IsPartition {α : Type} (P : (α → Prop) → Prop) : Prop where
  nonempty : ∀ B, P B → ∃ x, B x
  covers : ∀ x, ∃ B, P B ∧ B x
  disjoint : ∀ B C, P B → P C → (∃ x, B x ∧ C x) → B = C

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

classes_partitionLean 4Proved here from basic factsFormally verified

/-- **The equivalence classes of an equivalence relation form a partition.** Classes are non-empty
and cover everything because `a ∈ [a]`; two classes sharing an element `x` are equal because
`x R a` and `x R b` give `a R b`, so `[a] = [b]`. -/
theorem classes_partition {α : Type} {R : α → α → Prop} (h : Equivalence R) :
    IsPartition (classes R) where
  nonempty := by
    intro B ⟨a, hB⟩
    exact ⟨a, hB ▸ mem_cls_self h a⟩
  covers := fun x => ⟨cls R x, ⟨x, rfl⟩, mem_cls_self h x⟩
  disjoint := by
    intro B C ⟨a, hB⟩ ⟨b, hC⟩ ⟨x, hxB, hxC⟩
    rw [hB] at hxB
    rw [hC] at hxC
    rw [hB, hC]
    exact cls_eq_of_rel h (h.trans (h.symm hxB) hxC)

Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

same_block_equivalenceLean 4Proved here from basic factsFormally verified

/-- **"Lie in the same block" is an equivalence relation.** Reflexive: every element lies in
some block. Symmetric: obvious. Transitive: if `a, b ∈ B` and `b, c ∈ C`, then `B` and `C` share
`b`, so `B = C`, and `a, c` lie in the same block. -/
theorem same_block_equivalence {α : Type} {P : (α → Prop) → Prop} (hP : IsPartition P) :
    Equivalence (SameBlock P) where
  refl := by
    intro a
    obtain ⟨B, hB, ha⟩ := hP.covers a
    exact ⟨B, hB, ha, ha⟩
  symm := by
    intro a b ⟨B, hB, ha, hb⟩
    exact ⟨B, hB, hb, ha⟩
  trans := by
    intro a b c ⟨B, hB, ha, hb⟩ ⟨C, hC, hb', hc⟩
    have hBC : B = C := hP.disjoint B C hB hC ⟨b, hb, hb'⟩
    rw [← hBC] at hc
    exact ⟨B, hB, ha, hc⟩

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

The two round trips of Theorem 3 — relation to partition and back, and partition to relation and back:

same_block_classesLean 4Proved here from basic factsFormally verified

/-- Round trip 1: start with an equivalence relation `R`, form its classes, and ask "same class?".
You get `R` back: `a` and `b` lie in a common class exactly when `a R b`. -/
theorem same_block_classes {α : Type} {R : α → α → Prop} (h : Equivalence R) (a b : α) :
    SameBlock (classes R) a b ↔ R a b := by
  constructor
  · intro ⟨B, ⟨c, hB⟩, ha, hb⟩
    rw [hB] at ha hb
    exact h.trans ha (h.symm hb)
  · intro hab
    exact ⟨cls R b, ⟨b, rfl⟩, hab, mem_cls_self h b⟩

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

classes_same_blockLean 4Proved here from basic factsFormally verified

/-- Round trip 2: start with a partition `P`, form the relation "same block", and take its
classes. You get exactly the blocks of `P` back. Together with round trip 1 this says that
equivalence relations and partitions are two descriptions of the same thing, and that each
partition comes from exactly one equivalence relation. -/
theorem classes_same_block {α : Type} {P : (α → Prop) → Prop} (hP : IsPartition P)
    (B : α → Prop) : classes (SameBlock P) B ↔ P B := by
  constructor
  · intro ⟨a, hB⟩
    obtain ⟨C, hC, haC⟩ := hP.covers a
    -- The class of `a` is the block `C` containing `a`.
    have hcls : cls (SameBlock P) a = C := by
      funext x
      apply propext
      constructor
      · intro ⟨D, hD, hxD, haD⟩
        have hDC : D = C := hP.disjoint D C hD hC ⟨a, haD, haC⟩
        rw [← hDC]
        exact hxD
      · intro hxC
        exact ⟨C, hC, hxC, haC⟩
    rw [hB, hcls]
    exact hC
  · intro hB
    obtain ⟨a, haB⟩ := hP.nonempty B hB
    refine ⟨a, ?_⟩
    funext x
    apply propext
    constructor
    · intro hxB
      exact ⟨B, hB, hxB, haB⟩
    · intro ⟨D, hD, hxD, haD⟩
      have hDB : D = B := hP.disjoint D B hD hB ⟨a, haD, haB⟩
      rw [← hDB]
      exact hxD

Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

Finally, remainders. Lean's % gives the remainder between $0$ and $n - 1$ , also for negative numbers.

same_output_equivalenceLean 4Proved here from basic factsFormally verified

/-- For any function `f`, "has the same output under `f`" is an equivalence relation. "Same
remainder", "same colour", "same birth month" and "same last digit" are all of this kind. -/
theorem same_output_equivalence {α β : Type} (f : α → β) :
    Equivalence (fun a b => f a = f b) where
  refl := fun _ => rfl
  symm := fun hab => hab.symm
  trans := fun hab hbc => hab.trans hbc

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

remainder_examplesLean 4Proved here from basic factsFormally verified

/-- Examples, checked by calculation: `17` and `2` have the same remainder on division by `3`;
so do `-1` and `5` (remainder `2`); but `4` and `6` do not. -/
theorem remainder_examples :
    SameRemainder 3 17 2 ∧ SameRemainder 3 (-1) 5 ∧ ¬ SameRemainder 3 4 6 := by
  unfold SameRemainder
  decide

Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

exactly_n_classesLean 4Proved here from basic factsFormally verified

/-- **"Same remainder on division by `n`" has exactly `n` classes** (for `n > 0`): every integer
`a` is related to exactly one of `0, 1, …, n − 1`, namely its remainder `r = a % n`. So the
classes are `[0], [1], …, [n − 1]`, and these are all different. -/
theorem exactly_n_classes (n : Int) (hn : 0 < n) (a : Int) :
    ∃ r, 0 ≤ r ∧ r < n ∧ SameRemainder n a r ∧
      ∀ s, 0 ≤ s → s < n → SameRemainder n a s → s = r := by
  refine ⟨a % n, Int.emod_nonneg a (by omega), Int.emod_lt_of_pos a hn, ?_, ?_⟩
  · -- `a % n` has the same remainder as `a`: taking the remainder twice changes nothing.
    show a % n = a % n % n
    exact (Int.emod_emod_of_dvd a (Int.dvd_refl n)).symm
  · intro s hs0 hsn hsame
    -- A number between `0` and `n - 1` is its own remainder.
    have hss : s % n = s := Int.emod_eq_of_lt hs0 hsn
    show s = a % n
    rw [hsame, hss]

Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

What is formalised: every theorem in the proof section, in full generality (any set, any equivalence relation, any partition, any $n \ge 1$ ), using core Lean only. One step deserves a comment: the proof that classes are equal or disjoint splits into the cases “ $a \sim b$ ” and “not $a \sim b$ ”, which uses the law of excluded middle (Classical.em). Mathlib, Lean's large mathematical library, has all of this in general form: an equivalence relation is a Setoid, the set of classes is a Quotient, and Setoid.IsPartition and Setoid.classes connect the two.

ComputationC

A relation checker, and counting every case

A relation checker: counterexamples and classesPythonExhaustive finite checkCounterexampleComputationally tested

"""A relation checker: properties, counterexamples and classes.

Give it a finite set and a yes/no rule for pairs. It tests reflexivity,
symmetry and transitivity by running through every case, prints a
counterexample for each property that fails, and, when the rule is an
equivalence relation, prints its classes - which always come out as a
partition. On a finite set this exhaustive check is a proof for that set;
it says nothing about larger sets.
"""

def reflexive_counterexample(elements, rel):
    """An a with not rel(a, a), or None if rel is reflexive."""
    for a in elements:
        if not rel(a, a):
            return (a,)
    return None

def symmetric_counterexample(elements, rel):
    """A pair (a, b) with rel(a, b) but not rel(b, a), or None."""
    for a in elements:
        for b in elements:
            if rel(a, b) and not rel(b, a):
                return (a, b)
    return None

def transitive_counterexample(elements, rel):
    """A triple (a, b, c) with rel(a, b), rel(b, c), not rel(a, c), or None."""
    for a in elements:
        for b in elements:
            if not rel(a, b):
                continue
            for c in elements:
                if rel(b, c) and not rel(a, c):
                    return (a, b, c)
    return None

def equivalence_classes(elements, rel):
    """The classes [a] = [x for x in elements if rel(x, a)], without repeats,
    in order of first appearance."""
    found = []
    for a in elements:
        cls = [x for x in elements if rel(x, a)]
        if cls not in found:
            found.append(cls)
    return found

def is_partition(elements, blocks):
    """Blocks are non-empty, pairwise disjoint and together cover elements."""
    members = [x for block in blocks for x in block]
    return (all(blocks) and len(members) == len(set(members))
            and set(members) == set(elements))

def same_letters_count(u, v):
    return len(u) == len(v)

def share_a_letter(u, v):
    return bool(set(u.lower()) & set(v.lower()))

COUNTRIES = ["Chad", "Peru", "Iran", "Fiji", "Ghana", "Nepal", "Kenya",
             "Malta", "Bhutan", "Mexico"]

RELATIONS = [
    ("same remainder mod 3", list(range(12)), lambda a, b: a % 3 == b % 3),
    ("differ by at most 1", list(range(6)), lambda a, b: abs(a - b) <= 1),
    ("a divides b", list(range(1, 7)), lambda a, b: b % a == 0),
    ("a is less than b", list(range(6)), lambda a, b: a < b),
    ("same number of letters", COUNTRIES, same_letters_count),
    ("share a letter", COUNTRIES, share_a_letter),
]

def report(name, elements, rel):
    """Lines of text describing one relation."""
    checks = [("reflexive", reflexive_counterexample(elements, rel)),
              ("symmetric", symmetric_counterexample(elements, rel)),
              ("transitive", transitive_counterexample(elements, rel))]
    verdict = ", ".join(("" if cx is None else "not ") + p for p, cx in checks)
    lines = [f"{name}: {verdict}"]
    for prop, cx in checks:
        if cx is not None:
            shown = ", ".join(str(x) for x in cx)
            lines.append(f"   fails {prop}: ({shown})")
    if all(cx is None for _, cx in checks):
        blocks = equivalence_classes(elements, rel)
        shown = " ".join("{" + ",".join(str(x) for x in b) + "}" for b in blocks)
        lines.append(f"   {len(blocks)} classes: {shown}")
        lines.append(f"   the classes form a partition: {is_partition(elements, blocks)}")
    return lines

def main():
    for name, elements, rel in RELATIONS:
        for line in report(name, elements, rel):
            print(line)
    print()
    print("Epistemic status: every case on these finite sets was checked, so")
    print("each verdict is proved for that set - and one counterexample")
    print("settles a failure for good. A rule that passes on a small set may")
    print("still fail on a larger one; for 'same remainder' on all of Z the")
    print("lesson gives a proof.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Notice that “same number of letters” sorts the country names into a partition, but “share a letter” does not: Chad and Iran share an a, Iran and Peru share an r, but Chad and Peru share nothing.

Equivalence relations and partitions, counted exhaustivelyPythonExact computationExhaustive finite checkComputationally tested

"""Counting relations, equivalence relations and partitions on small sets.

A relation on {0, ..., n-1} is any set of ordered pairs, so there are 2^(n*n)
of them. The experiment runs through relations exhaustively, tests the three
properties, and compares the equivalence relations with the partitions of the
set, generated independently. For n <= 4 it confirms that "take the classes"
matches the equivalence relations one-to-one with the partitions, and it
counts the relations that are symmetric and transitive but NOT reflexive.
This is exhaustive-finite evidence; the lesson proves the theorem for every
set.
"""

import itertools

def is_reflexive(n, rel):
    """Every a in {0..n-1} is related to itself."""
    return all((a, a) in rel for a in range(n))

def is_symmetric(rel):
    """(a, b) in rel always implies (b, a) in rel."""
    return all((b, a) in rel for a, b in rel)

def is_transitive(rel):
    """(a, b) and (b, c) in rel always imply (a, c) in rel."""
    return all((a, d) in rel for a, b in rel for c, d in rel if b == c)

def is_equivalence(n, rel):
    """Reflexive, symmetric and transitive."""
    return is_reflexive(n, rel) and is_symmetric(rel) and is_transitive(rel)

def all_relations(n):
    """Yield every relation on {0..n-1} as a frozenset of pairs (2^(n*n))."""
    pairs = list(itertools.product(range(n), repeat=2))
    for mask in range(2 ** len(pairs)):
        yield frozenset(p for i, p in enumerate(pairs) if mask >> i & 1)

def symmetric_relations(n):
    """Yield every symmetric relation on {0..n-1} (2^(n(n+1)/2) of them)."""
    slots = [(a, b) for a in range(n) for b in range(a, n)]
    for mask in range(2 ** len(slots)):
        rel = set()
        for i, (a, b) in enumerate(slots):
            if mask >> i & 1:
                rel.update({(a, b), (b, a)})
        yield frozenset(rel)

def classes(n, rel):
    """The partition into classes [a] = {x : (x, a) in rel}, as a frozenset."""
    return frozenset(frozenset(x for x in range(n) if (x, a) in rel)
                     for a in range(n))

def set_partitions(n):
    """Yield all partitions of {0..n-1}, built by placing one element at a
    time into an existing block or a new block (no relations involved)."""
    def build(i, blocks):
        if i == n:
            yield frozenset(frozenset(b) for b in blocks)
            return
        for b in blocks:
            b.append(i)
            yield from build(i + 1, blocks)
            b.pop()
        blocks.append([i])
        yield from build(i + 1, blocks)
        blocks.pop()
    yield from build(0, [])

def bell_numbers(count):
    """First `count` Bell numbers B_0, B_1, ... via the Bell triangle."""
    bells, row = [1], [1]
    while len(bells) < count:
        new = [row[-1]]
        for x in row:
            new.append(new[-1] + x)
        row = new
        bells.append(row[0])
    return bells[:count]

def property_counts(n):
    """Counts of reflexive/symmetric/transitive/equivalence relations."""
    counts = {"all": 0, "refl": 0, "symm": 0, "trans": 0, "equiv": 0}
    for rel in all_relations(n):
        r, s, t = is_reflexive(n, rel), is_symmetric(rel), is_transitive(rel)
        counts["all"] += 1
        counts["refl"] += r
        counts["symm"] += s
        counts["trans"] += t
        counts["equiv"] += r and s and t
    return counts

def compare(n):
    """Return (number of equivalence relations, number of partitions,
    whether "take the classes" is a bijection between them, number of
    symmetric and transitive relations) for the set {0..n-1}."""
    equivs, sym_trans = [], 0
    for rel in symmetric_relations(n):
        if is_transitive(rel):
            sym_trans += 1
            if is_reflexive(n, rel):
                equivs.append(rel)
    images = {classes(n, rel) for rel in equivs}
    parts = set(set_partitions(n))
    bijective = images == parts and len(images) == len(equivs)
    return len(equivs), len(parts), bijective, sym_trans

def main():
    c = property_counts(3)
    print("1. Every relation on {0, 1, 2}: 2^9 =", c["all"])
    print(f"   reflexive {c['refl']}, symmetric {c['symm']}, "
          f"transitive {c['trans']}, equivalence {c['equiv']}")
    print()
    print("2. Equivalence relations versus partitions (generated separately)")
    print("   n  equivalences  partitions  Bell  classes match?  symm+trans")
    bells = bell_numbers(6)
    for n in range(1, 5):
        eq, parts, match, st = compare(n)
        print(f"   {n}  {eq:12}  {parts:10}  {bells[n]:4}  "
              f"{'yes' if match else 'NO':>14}  {st:10}")
    print("   Symmetric + transitive relations outnumber the equivalences:")
    print("   the extra ones relate some element to nothing at all. (Their")
    print("   number is the NEXT Bell number: 2, 5, 15, 52.)")
    rel = frozenset({(0, 0)})
    print(f"   An example on {{0, 1}}: {set(rel)} - symmetric "
          f"{is_symmetric(rel)}, transitive {is_transitive(rel)},")
    print(f"   reflexive {is_reflexive(2, rel)} (1 is related to nothing).")
    print()
    print("Epistemic status: exact, exhaustive checks of every case for sets")
    print("with at most 4 elements (at most 3 for the full table). They agree")
    print("with the theorem that equivalence relations and partitions match")
    print("one-to-one, but only the lesson's proof shows it for every set.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The counts of equivalence relations and of partitions agree — $1, 2, 5, 15$ — and “take the classes” matches them up one-to-one, exactly as Theorems 2 and 3 predict. These numbers are the Bell numbers. The last column counts relations that are symmetric and transitive: there are more of them than equivalence relations, and every extra one leaves some element related to nothing. This is exhaustive evidence for sets of at most four elements; the proofs above cover every set, finite or infinite.

Explore

Explore: classes you can see

Colour every integer by its remainder. Every integer gets exactly one colour, so the colours form a partition — and the “add” panel previews something remarkable: the colour of a sum depends only on the colours you add.

Remainder families

Colour each integer by its remainder after dividing by k. Every integer lands in exactly one family.

Divide by k = 3

−15−14−13−12−11−10−9−8−7−6−5−4−3−2−10123456789101112131415

[0]{ …, −15, −12, −9, −6, −3, 0, … }
[1]{ …, −14, −11, −8, −5, −2, 1, … }
[2]{ …, −13, −10, −7, −4, −1, 2, … }

Add a member of one family to a member of another…

A grid shows the same partition in another way. With $7$ numbers in each row, numbers in the same column differ by a multiple of $7$ , so each column is an equivalence class of “same remainder on division by $7$ ”. Change the number $k$ whose multiples are marked and see which columns light up.

Columns are classes

With 7 numbers per row, each column holds one remainder class for division by 7.

Multiples of7

multiple of 7

There are 10 multiples of 7 from 1 to 70.

Tap a number to see how it is related.

A symmetric relation can be drawn as a network: one dot per element and a line between two different elements when they are related (we leave out the loops). For an equivalence relation, transitivity forces every two dots in a connected piece to be joined directly, so each piece is a complete cluster, and a dot in a class of size $k$ has exactly $k - 1$ lines. Compare “same remainder on division by 3” on $\{0, \dots, 8\}$ with “differ by at most 1” on $\{0, \dots, 5\}$ :

Same remainder on division by 3

Three classes, three complete triangles: every dot has 3 − 1 = 2 lines.

|V| = 9|E| = 9Select a vertex to see the edges that meet there.

deg(0) = 2deg(1) = 2deg(2) = 2deg(3) = 2deg(4) = 2deg(5) = 2deg(6) = 2deg(7) = 2deg(8) = 2

2 + 2 + 2 + 2 + 2 + 2 + 2 + 2 + 2 = 18 = 2 × 9

Every edge has two ends, so it adds exactly 2 to the total: the degrees add up to 18 = 2 × 9. This is the handshake lemma, Σ deg(v) = 2|E|.

Vertices of odd degree: 0. This number is always even, because the total is even.

Differ by at most 1

One connected piece, but 0 and 2 are not joined: a two-step path with no shortcut.

|V| = 6|E| = 5Select a vertex to see the edges that meet there.

deg(0) = 1deg(1) = 2deg(2) = 2deg(3) = 2deg(4) = 2deg(5) = 1

1 + 2 + 2 + 2 + 2 + 1 = 10 = 2 × 5

Every edge has two ends, so it adds exactly 2 to the total: the degrees add up to 10 = 2 × 5. This is the handshake lemma, Σ deg(v) = 2|E|.

Vertices of odd degree: 2. This number is always even, because the total is even.

Things to try: in the first picture, select a dot and check that its lines go exactly to the other members of its class. In the second, find two dots in the same connected piece that are not joined — each such pair is a counterexample to transitivity.

Exercises

1. Relations, equivalence relations and partitions

Warm-upHuman

On the set $\{0, 1, 2, \dots, 11\}$ , let $a \sim b$ mean that $a$ and $b$ have the same remainder on division by $4$ . List the elements of the class $[6]$ .

2. Relations, equivalence relations and partitions

Warm-upHuman

Which properties does the relation $a \le b$ (“ $a$ is less than or equal to $b$ ”) on $\Z$ have? Choose all that apply.

Choose all that apply

ReflexiveSymmetricTransitive

3. Relations, equivalence relations and partitions

CoreHuman

On $\Z$ , let $a \approx b$ mean that $a$ and $b$ differ by at most $2$ . This relation is not an equivalence relation. Which of these is a genuine counterexample?

Choose one

0 \approx 2

and

2 \approx 4

, but

0 \not\approx 4

3 \not\approx 3

1 \approx 3

but

3 \not\approx 1

0 \approx 1

and

1 \approx 2

, and

0 \approx 2

4. Relations, equivalence relations and partitions

Warm-upHuman

On the whole numbers $0, 1, 2, 3, \dots$ , let $a \sim b$ mean “ $a$ and $b$ have the same last digit”. How many equivalence classes are there?

5. Relations, equivalence relations and partitions

CoreHuman

The partition $\{\{a, b, c\}, \{d\}, \{e, f\}\}$ of $\{a, b, c, d, e, f\}$ defines the relation “lies in the same block as”. How many ordered pairs does this relation contain?

6. Relations, equivalence relations and partitions

CoreHuman

Here is a “proof” that every symmetric, transitive relation is reflexive.

Let $a$ be any element. (1) Choose $b$ with $a \sim b$ . (2) By symmetry, $b \sim a$ . (3) By transitivity, from $a \sim b$ and $b \sim a$ we get $a \sim a$ .

What is wrong?

Choose one

Step (1): there might be no

b

with

a \sim b

Step (2) uses symmetry the wrong way roundStep (3): transitivity needs three different elementsNothing — the proof is correct

7. Relations, equivalence relations and partitions

CoreHuman

Which of these is a partition of $\{1, 2, 3, 4, 5, 6\}$ ?

Choose one

\{\{1, 2\}, \{3, 4\}, \{5, 6\}\}

\{\{1, 2, 3\}, \{3, 4, 5, 6\}\}

\{\{1, 2\}, \{4, 5, 6\}\}

\{\{1, 2, 3, 4, 5, 6\}, \varnothing\}

8. Relations, equivalence relations and partitions

StretchHuman

How many different equivalence relations are there on the set $\{1, 2, 3, 4\}$ ? (Use Theorem 3: count the partitions instead.)

9. Relations, equivalence relations and partitions

CoreFormal

In the Lean section, cls R a x means “ $x$ belongs to the class of $a$ ”. Which statement says that any two classes are equal or disjoint?

Choose one

cls R a = cls R b ∨ ∀ x, ¬ (cls R a x ∧ cls R b x)cls R a = cls R b ∧ ∀ x, ¬ (cls R a x ∧ cls R b x)∀ x, cls R a x → cls R b xcls R a ≠ cls R b → ∃ x, cls R a x ∧ cls R b x

10. Relations, equivalence relations and partitions

StretchComputational

Write is_equivalence(elements, related), where elements is a list and related(a, b) returns True or False. It should return True exactly when the relation is reflexive, symmetric and transitive on elements. Python's all(...) is handy: all(related(a, a) for a in elements) tests reflexivity. What should your function return for an empty list, and why?

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

“Symmetric and transitive together imply reflexive.” The argument “ $a \sim b$ , so $b \sim a$ , so $a \sim a$ ” assumes there is some $b$ related to $a$ . If an element is related to nothing, the argument never starts. On $\{0, 1\}$ , the relation $\{(0, 0)\}$ is symmetric and transitive, but $1$ is not related to itself. Reflexivity has to be checked separately.

Misconception

“An equivalence class is a single element.” The class $[2]$ for remainders on division by $3$ is the whole set $\{\dots, -4, -1, 2, 5, 8, \dots\}$ . The number $2$ is just one convenient name for it; $[5]$ and $[-1]$ name the same set.

Misconception

“Every relation is symmetric.” Many everyday relations are not: “is less than”, “divides”, “is a parent of”, “is taller than”. In a symmetric relation every arrow has a return arrow; check for one before assuming it.

Misconception

“A relation that is true for nearby things is transitive.” “Differ by at most 1” and “lives within 1 km of” feel like sameness, but small differences add up: $0$ is close to $1$ , and $1$ to $2$ , yet $0$ is not close to $2$ . Such relations do not sort a set into boxes.

Misconception

“Transitivity only matters for three different elements.” The definition covers all $a, b, c$ , including $c = a$ . That is exactly why “is a sibling of” fails: Ana is Ben's sibling and Ben is Ana's, but Ana is not her own sibling.

ViewpointsH

Other ways of seeing

Geometry— What is a shape?

Two triangles are congruent if a rigid motion — a slide, turn or flip — carries one exactly onto the other, and similar if this is possible after also scaling (see rigid motions, congruence and similarity). Both are equivalence relations: every triangle is congruent to itself (do nothing), a motion can be undone (symmetry), and two motions can be done one after another (transitivity). The classes of “similar” are what we mean by a shape: “the shape of an equilateral triangle” is a whole class of triangles of every size, position and orientation. This viewpoint — study what stays the same under a family of transformations — grew into Felix Klein's Erlangen programme (1872; see transformation geometry).

Topology— Gluing

Take a line segment from $0$ to $1$ and declare its two endpoints equivalent (and every other point equivalent only to itself). The classes are the points of a new space, and it is a circle: walking off the end at $1$ brings you back in at $0$ . Do the same with a square, gluing each point of the left edge to the point at the same height on the right edge, and each point of the top edge to the point below it on the bottom edge, and you get a torus, the surface of a doughnut. A video game in which leaving the screen on the right brings you back on the left, and leaving at the top brings you back at the bottom, is played on such a torus. Mathematicians build many spaces this way, as quotient spaces (see point-set topology); the extra work at that level is to say what “nearby” means for the new points.

Number theory— Arithmetic with classes

The remainder classes on division by $n$ can be added and multiplied: $[a] + [b] = [a + b]$ and $[a] \cdot [b] = [a b]$ . This only makes sense because the answer does not depend on which member names each class — if $a \sim a'$ and $b \sim b'$ , then $a - a'$ and $b - b'$ are multiples of $n$ , so $(a + b) - (a' + b')$ is one too. The result is a number system with exactly $n$ elements, written $\Z/n\Z$ : the arithmetic of clocks and calendars (see clock arithmetic and, later, congruences). The Remainder families trail below explores it.

Set-theoretic connectionH

Set-theoretic connection: numbers as classes

Equivalence relations let mathematicians build number systems. A fraction $\tfrac{a}{b}$ can be thought of as a pair $(a, b)$ of integers with $b \neq 0$ , where two pairs count as the same number when $a d = b c$ : so $(1, 2) \sim (2, 4) \sim (3, 6)$ . This is an equivalence relation, and a rational number is a class of such pairs. Writing $\tfrac{1}{2} = \tfrac{2}{4}$ means that the two pairs lie in the same class.

The integers can be built the same way from pairs of natural numbers, with $(m, n)$ standing for “ $m - n$ ” and $(m, n) \sim (m', n')$ when $m + n' = m' + n$ — a construction mentioned in the integers lesson. In both cases the hard work is checking that the relation really is an equivalence relation, and that addition and multiplication do not depend on which member of a class you pick.

Category-theoretic connectionH

A glimpse of structure: the quotient map

Write $A/{\sim}$ for the set of equivalence classes, and $\pi : A \to A/{\sim}$ for the function $\pi(a) = [a]$ that sends each element to its class. Now suppose $f : A \to B$ is any function that is constant on classes: whenever $a \sim a'$ , $f(a) = f(a')$ . Then $f$ “only looks at the class”, so there is exactly one function $\bar f : A/{\sim} \to B$ with $\bar f([a]) = f(a)$ .

Every

f

that is constant on classes factors through

\pi

by exactly one dashed arrow:

\bar f(\pi(a)) = f(a)

For example, $f(a) = (-1)^a$ is $1$ for every even integer and $-1$ for every odd one. It is constant on the classes of “same remainder on division by $2$ ”, so it is really a function on the two classes: $\bar f([0]) = 1$ and $\bar f([1]) = -1$ . Category theorists call this property of $\pi$ a universal property (see universal properties): it describes $A/{\sim}$ completely by how functions out of it behave, and the same pattern produces quotient groups and rings (see quotients).

Wonder Trails

Wonder Trail

Sort the integers into remainder families, then discover that you can add and multiply the families themselves.

Wonder Trail · Optional · never gradedRemainder familiesSort every integer — positive, negative and zero — into families by its remainder after dividing by 3. If you add a member of one family to a member of another, does the family of the answer depend on which members you chose?Follow the trail

History & global context

History and global context

The first of the “common notions” in Book I of Euclid's Elements (Alexandria, around 300 BCE) reads: things which are equal to the same thing are also equal to one another. It is a transitivity principle for equality, used throughout Greek geometry.
Reasoning by remainders is ancient. The Chinese Sunzi Suanjing (Master Sun's Mathematical Manual, around the 3rd to 5th century CE) asks for a number that leaves remainder $2$ when counted by threes, $3$ when counted by fives and $2$ when counted by sevens. In India, Āryabhaṭa's Āryabhaṭīya (499 CE) gave the kuṭṭaka (“pulveriser”) method for problems of this kind, and in China Qin Jiushao's Shushu Jiuzhang (1247) gave a general method.
Carl Friedrich Gauss's Disquisitiones Arithmeticae (1801) introduced the notation $a \equiv b \pmod{n}$ and treated the remainder classes as objects in their own right.
Gottlob Frege, in Die Grundlagen der Arithmetik (1884), proposed defining the direction of a line as the class of all lines parallel to it — an early, explicit use of equivalence classes to define a new kind of object. Defining numbers, shapes and spaces as classes became standard in 20th-century mathematics.

Sorting by sameness

A relation is a yes-or-no question about pairs

Definitions

Examples and non-examples

Classes, partitions and remainders

The proofs, checked by Lean

A relation checker, and counting every case

Explore: classes you can see

Exercises

Common misconceptions

Other ways of seeing

Set-theoretic connection: numbers as classes

A glimpse of structure: the quotient map

Wonder Trail

History and global context

Further reading