equivalence relations = partitions

Stream: maths

[Kevin Buzzard]

We have this canonical 1st year (in UK at least) theorem that we teach many 1st years: equivalence relations are the same thing as partitions. Am I right in thinking that docs#partition.order_iso is the way we say "there's a bijection between equivalence classes and partitions" but that this result is essentially never used in mathlib? Even the file it's in, data.setoid.partition is never imported, and it's barely used in that file either.

It was great for teaching though! The original proof was by an IC student and I'm sure they learnt a lot about Lean doing little projects like that.

[Kyle Miller]

Yep, docs#setoid.partition.order_iso is the bijection between equivalence classes and partitions. setoid conveniently packages up a relation with it's proof that it's an equivalence relation, and the right-hand side could be written as {p : set (set α) | setoid.is_partition p} (with an implicit coercion to subtype). (I realize you're not asking about this, but it took me a little while to work out what that was doing.)

[Kyle Miller]

I didn't know about the has_le on setoid. I guess s <= t iff the equivalence classes for s are a refinement of those of t.

[Patrick Massot]

This file is used in LTE.

[Johan Commelin]

Must be a sign that we're finally doing serious maths

[Adam Topaz]

We only use that file in LTE because mathlib's topological spaces haven't been replaced by condensed sets yet :wink: