# mathlibdocumentation

data.setoid.partition

# Equivalence relations: partitions

This file comprises properties of equivalence relations viewed as partitions.

## Tags

setoid, equivalence, iseqv, relation, equivalence relation, partition, equivalence class

theorem setoid.eq_of_mem_eqv_class {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) {x : α} {b b' : set α} :
b cx bb' cx b'b = b'

If x ∈ α is in 2 elements of a set of sets partitioning α, those 2 sets are equal.

def setoid.mk_classes {α : Type u_1} (c : set (set α)) :
(∀ (a : α), ∃! (b : set α) (H : b c), a b)

Makes an equivalence relation from a set of sets partitioning α.

Equations
def setoid.classes {α : Type u_1} :
set (set α)

Makes the equivalence classes of an equivalence relation.

Equations
theorem setoid.mem_classes {α : Type u_1} (r : setoid α) (y : α) :
{x : α | r.rel x y} r.classes

theorem setoid.eq_iff_classes_eq {α : Type u_1} {r₁ r₂ : setoid α} :
r₁ = r₂ ∀ (x : α), {y : α | r₁.rel x y} = {y : α | r₂.rel x y}

Two equivalence relations are equal iff all their equivalence classes are equal.

theorem setoid.rel_iff_exists_classes {α : Type u_1} (r : setoid α) {x y : α} :
r.rel x y ∃ (c : set α) (H : c r.classes), x c y c

theorem setoid.classes_inj {α : Type u_1} {r₁ r₂ : setoid α} :
r₁ = r₂ r₁.classes = r₂.classes

Two equivalence relations are equal iff their equivalence classes are equal.

theorem setoid.empty_not_mem_classes {α : Type u_1} {r : setoid α} :

The empty set is not an equivalence class.

theorem setoid.classes_eqv_classes {α : Type u_1} {r : setoid α} (a : α) :
∃! (b : set α) (H : b r.classes), a b

Equivalence classes partition the type.

theorem setoid.eq_of_mem_classes {α : Type u_1} {r : setoid α} {x : α} {b : set α} (hc : b r.classes) (hb : x b) {b' : set α} :
b' r.classesx b'b = b'

If x ∈ α is in 2 equivalence classes, the equivalence classes are equal.

theorem setoid.eq_eqv_class_of_mem {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) {s : set α} {y : α} :
s cy ss = {x : α | H).rel x y}

The elements of a set of sets partitioning α are the equivalence classes of the equivalence relation defined by the set of sets.

theorem setoid.eqv_class_mem {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) {y : α} :
{x : α | H).rel x y} c

The equivalence classes of the equivalence relation defined by a set of sets partitioning α are elements of the set of sets.

theorem setoid.eqv_classes_disjoint {α : Type u_1} {c : set (set α)} :
(∀ (a : α), ∃! (b : set α) (H : b c), a b) → c.pairwise_disjoint

Distinct elements of a set of sets partitioning α are disjoint.

theorem setoid.eqv_classes_of_disjoint_union {α : Type u_1} {c : set (set α)} (hu : ⋃₀c = set.univ) (H : c.pairwise_disjoint) (a : α) :
∃! (b : set α) (H : b c), a b

A set of disjoint sets covering α partition α (classical).

def setoid.setoid_of_disjoint_union {α : Type u_1} {c : set (set α)} :

Makes an equivalence relation from a set of disjoints sets covering α.

Equations
theorem setoid.mk_classes_classes {α : Type u_1} (r : setoid α) :

The equivalence relation made from the equivalence classes of an equivalence relation r equals r.

@[simp]
theorem setoid.sUnion_classes {α : Type u_1} (r : setoid α) :

def setoid.is_partition {α : Type u_1} :
set (set α) → Prop

A collection c : set (set α) of sets is a partition of α into pairwise disjoint sets if ∅ ∉ c and each element a : α belongs to a unique set b ∈ c.

Equations
theorem setoid.nonempty_of_mem_partition {α : Type u_1} {c : set (set α)} (hc : setoid.is_partition c) {s : set α} :
s c → s.nonempty

A partition of α does not contain the empty set.

theorem setoid.is_partition_classes {α : Type u_1} (r : setoid α) :

theorem setoid.is_partition.pairwise_disjoint {α : Type u_1} {c : set (set α)} :

theorem setoid.is_partition.sUnion_eq_univ {α : Type u_1} {c : set (set α)} :

theorem setoid.exists_of_mem_partition {α : Type u_1} {c : set (set α)} (hc : setoid.is_partition c) {s : set α} :
s c(∃ (y : α), s = {x : α | _).rel x y})

All elements of a partition of α are the equivalence class of some y ∈ α.

theorem setoid.classes_mk_classes {α : Type u_1} (c : set (set α)) (hc : setoid.is_partition c) :
_).classes = c

The equivalence classes of the equivalence relation defined by a partition of α equal the original partition.

@[instance]
def setoid.partition.le {α : Type u_1} :

Defining ≤ on partitions as the ≤ defined on their induced equivalence relations.

Equations
@[instance]
def setoid.partition.partial_order {α : Type u_1} :

Defining a partial order on partitions as the partial order on their induced equivalence relations.

Equations
def setoid.partition.rel_iso (α : Type u_1) :

The order-preserving bijection between equivalence relations and partitions of sets.

Equations
@[instance]
def setoid.partition.complete_lattice {α : Type u_1} :

A complete lattice instance for partitions; there is more infrastructure for the equivalent complete lattice on equivalence relations.

Equations