Equivalence relations: partitions
This file comprises properties of equivalence relations viewed as partitions.
Tags
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.
The equivalence classes of the equivalence relation defined by a set of sets partitioning α are elements of the set of sets.
Distinct elements of a set of sets partitioning α are disjoint.
Makes an equivalence relation from a set of disjoints sets covering α.
Equations
The equivalence relation made from the equivalence classes of an equivalence relation r equals r.
A partition of α does not contain the empty set.
All elements of a partition of α are the equivalence class of some y ∈ α.
The equivalence classes of the equivalence relation defined by a partition of α equal the original partition.
Defining ≤ on partitions as the ≤ defined on their induced equivalence relations.
Equations
- setoid.partition.le = {le := λ (x y : subtype setoid.is_partition), setoid.mk_classes x.val _ ≤ setoid.mk_classes y.val _}
Defining a partial order on partitions as the partial order on their induced equivalence relations.
Equations
- setoid.partition.partial_order = {le := has_le.le setoid.partition.le, lt := λ (x y : subtype setoid.is_partition), x ≤ y ∧ ¬y ≤ x, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
The order-preserving bijection between equivalence relations and partitions of sets.
Equations
- setoid.partition.rel_iso α = {to_equiv := {to_fun := λ (r : setoid α), ⟨r.classes, _⟩, inv_fun := λ (x : subtype setoid.is_partition), setoid.mk_classes x.val _, left_inv := _, right_inv := _}, map_rel_iff' := _}
A complete lattice instance for partitions; there is more infrastructure for the equivalent complete lattice on equivalence relations.