English
There is an order-preserving bijection between the set of all equivalence relations on α and the set of all partitions of α.
Русский
Существует упорядоченный биекция между множеством эквивалентностей на α и множеством разбиений α.
LaTeX
$$$\\text{Setoid}(\\alpha) \\simeq_o \\{ C : Set(Set \\alpha) \\,|\\, \\text{IsPartition}(C) \\}$$$
Lean4
/-- The order-preserving bijection between equivalence relations on a type `α`, and
partitions of `α` into subsets. -/
protected def orderIso : Setoid α ≃o { C : Set (Set α) // IsPartition C }
where
toFun r := ⟨r.classes, empty_notMem_classes, classes_eqv_classes⟩
invFun C := mkClasses C.1 C.2.2
left_inv := mkClasses_classes
right_inv C := by rw [Subtype.ext_iff, ← classes_mkClasses C.1 C.2]
map_rel_iff'
{r s} := by
conv_rhs => rw [← mkClasses_classes r, ← mkClasses_classes s]
rfl
