mathlib documentation

lean_problem_sheets / 2020.relations.partition_challenge_official_solution

The partition challenge! #

Prove that equivalence relations on α are the same as partitions of α.

Three sections:

  1. partitions
  2. equivalence classes
  3. the challenge

Say α is a type, and R is a binary relation on α. The following things are already in Lean:

reflexive R := ∀ (x : α), R x x symmetric R := ∀ ⦃x y : α⦄, R x y → R y x transitive R := ∀ ⦃x y z : α⦄, R x y → R y z → R x z

equivalence R := reflexive R ∧ symmetric R ∧ transitive R

In the file below, we will define partitions of α and "build some interface" (i.e. prove some propositions). We will define equivalence classes and do the same thing. Finally, we will prove that there's a bijection between equivalence relations on α and partitions of α.