Equivalence relations: partitions #
This file comprises properties of equivalence relations viewed as partitions. There are two implementations of partitions here:
- A collection
c : Set (Set α)
of sets is a partition ofα
if∅ ∉ c
and each elementa : α
belongs to a unique setb ∈ c
. This is expressed asIsPartition c
- An indexed partition is a map
s : ι → α
whose image is a partition. This is expressed asIndexedPartition s
.
Of course both implementations are related to Quotient
and Setoid
.
Setoid.isPartition.partition
and Finpartition.isPartition_parts
furnish
a link between Setoid.IsPartition
and Finpartition
.
TODO #
Could the design of Finpartition
inform the one of Setoid.IsPartition
? Maybe bundling it and
changing it from Set (Set α)
to Set α
where [Lattice α] [OrderBot α]
would make it more
usable.
Tags #
setoid, equivalence, iseqv, relation, equivalence relation, partition, equivalence class
Two equivalence relations are equal iff all their equivalence classes are equal.
Two equivalence relations are equal iff their equivalence classes are equal.
The empty set is not an equivalence class.
Equivalence classes partition the type.
If x ∈ α is in 2 equivalence classes, the equivalence classes are equal.
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.
A set of disjoint sets covering α partition α (classical).
Makes an equivalence relation from a set of disjoints sets covering α.
Instances For
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.
Defining a partial order on partitions as the partial order on their induced equivalence relations.
The order-preserving bijection between equivalence relations on a type α
, and
partitions of α
into subsets.
Instances For
A complete lattice instance for partitions; there is more infrastructure for the equivalent complete lattice on equivalence relations.
A finite setoid partition furnishes a finpartition
Instances For
A finpartition gives rise to a setoid partition
two indexes are equal if they are equal in membership
- some : ι → α
sends an index to an element of the corresponding set
- some_mem : ∀ (i : ι), IndexedPartition.some s i ∈ s✝ i
membership invariance for
some
- index : α → ι
index for type
α
- mem_index : ∀ (x : α), x ∈ s✝ (IndexedPartition.index s x)
membership invariance for
index
Constructive information associated with a partition of a type α
indexed by another type ι
,
s : ι → Set α
.
IndexedPartition.index
sends an element to its index, while IndexedPartition.some
sends
an index to an element of the corresponding set.
This type is primarily useful for definitional control of s
- if this is not needed, then
Setoid.ker index
by itself may be sufficient.
Instances For
The non-constructive constructor for IndexedPartition
.
Instances For
On a unique index set there is the obvious trivial partition
The equivalence relation associated to an indexed partition. Two elements are equivalent if they belong to the same set of the partition.
Instances For
The quotient associated to an indexed partition.
Instances For
The projection onto the quotient associated to an indexed partition.
Instances For
The obvious equivalence between the quotient associated to an indexed partition and the indexing type.
Instances For
A map choosing a representative for each element of the quotient associated to an indexed
partition. This is a computable version of Quotient.out'
using IndexedPartition.some
.
Instances For
This lemma is analogous to Quotient.mk_out'
.
The indices of Quotient.out'
and IndexedPartition.out
are equal.
This lemma is analogous to Quotient.out_eq'
.