The first section of the file defines the complete lattice of equivalence relations on a type, results about the inductively defined equivalence closure of a binary relation, and the analogues of some isomorphism theorems for quotients of arbitrary types.
The second section comprises properties of equivalence relations viewed as partitions.
The function rel and lemmas ending in ' make it easier to talk about different equivalence relations on the same type.
The complete lattice instance for equivalence relations could have been defined by lifting the Galois insertion of equivalence relations on α into binary relations on α, and then using complete_lattice.copy to define a complete lattice instance with more appropriate definitional equalities (a similar example is filter.lattice.complete_lattice in order/filter/basic.lean). This does not save space, however, and is less clear.
Partitions are not defined as a separate structure here; users are encouraged to reason about them using the existing setoid and its infrastructure.
setoid, equivalence, iseqv, relation, equivalence relation, partition, equivalence class
A version of setoid.r that takes the equivalence relation as an explicit argument.
A version of quotient.eq' compatible with setoid.rel, to make rewriting possible.
Two equivalence relations are equal iff their underlying binary operations are equal.
Defining ≤ for equivalence relations.
The kernel of a function is an equivalence relation.
The kernel of the quotient map induced by an equivalence relation r equals r.
The infimum of two equivalence relations.
The infimum of 2 equivalence relations r and s is the same relation as the infimum of the underlying binary operations.
The infimum of a set of equivalence relations.
The underlying binary operation of the infimum of a set of equivalence relations is the infimum of the set's image under the map to the underlying binary operation.
The infimum of a set of equivalence relations is contained in any element of the set.
If an equivalence relation r is contained in every element of a set of equivalence relations, r is contained in the infimum of the set.
The inductively defined equivalence closure of a binary relation r is the infimum of the set of all equivalence relations containing r.
The supremum of two equivalence relations, defined as the infimum of the set of equivalence relations containing both.
The supremum of two equivalence relations r and s is the equivalence closure of the binary relation x is related to y by r or s.
The supremum of 2 equivalence relations r and s is the equivalence closure of the supremum of the underlying binary operations.
The complete lattice of equivalence relations on a type, with bottom element = and top element the trivial equivalence relation.
The supremum of a set S of equivalence relations is the equivalence closure of the binary relation there exists r ∈ S relating x and y.
The supremum of a set of equivalence relations is the equivalence closure of the supremum of the set's image under the map to the underlying binary operation.
The equivalence closure of an equivalence relation r is r.
Equivalence closure is idempotent.
The equivalence closure of a binary relation r is contained in any equivalence relation containing r.
Equivalence closure of binary relations is monotonic.
There is a Galois insertion of equivalence relations on α into binary relations on α, with equivalence closure the lower adjoint.
A function from α to β is injective iff its kernel is the bottom element of the complete lattice of equivalence relations on α.
The elements related to x ∈ α by the kernel of f are those in the preimage of f(x) under f.
The uniqueness part of the universal property for quotients of an arbitrary type.
Given a map f from α to β, the natural map from the quotient of α by the kernel of f is injective.
Given a map f from α to β, the kernel of f is the unique equivalence relation on α whose induced map from the quotient of α to β is injective.
The first isomorphism theorem for sets: the quotient of α by the kernel of a function f bijects with f's image.
The quotient of α by the kernel of a surjective function f bijects with f's codomain.
The third isomorphism theorem for sets.
Given a function f whose kernel is contained in an equivalence relation r, the equivalence closure of the relation on f's image defined by x ≈ y ↔ the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by r.
Given a surjective function f whose kernel is contained in an equivalence relation r, the equivalence relation on f's codomain defined by x ≈ y ↔ the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by r.
A special case of the equivalence closure of an equivalence relation r equalling r.
Given an equivalence relation r on α and a map f to the quotient of α by r, an equivalence relation s on the quotient induces an equivalence relation on f's domain defined by x ≈ y ↔ f(x) is related to f(y) by s.
Given an equivalence relation r on α, the order-preserving bijection between the set of equivalence relations containing r and the equivalence relations on the quotient of α by r.
If x ∈ α is in 2 elements of a set of sets partitioning α, those 2 sets are equal.
Makes an equivalence relation from a set of sets partitioning α.
Makes the equivalence classes of an equivalence relation.
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 α.
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 and partitions of sets.
A complete lattice instance for partitions; there is more infrastructure for the equivalent complete lattice on equivalence relations.