Equivalence relations: partitions #
This file comprises properties of equivalence relations viewed as partitions.
setoid, equivalence, iseqv, relation, equivalence relation, partition, equivalence class
The elements of a set of sets partitioning α are the equivalence classes of the equivalence relation defined by the set of sets.
≤ on partitions as the
≤ defined on their induced equivalence relations.
Defining a partial order on partitions as the partial order on their induced equivalence relations.
The order-preserving bijection between equivalence relations and partitions of sets.
A complete lattice instance for partitions; there is more infrastructure for the equivalent complete lattice on equivalence relations.