Equivalence Relations and Classes of Abstraction 1
Konrad Raczkowski, Pawe l Sadowski · 1990
Summary. In this article we deal with the notion of equivalence relation. The main properties of equivalence relations are proved. Then we define the classes of abstraction determined by an equivalence relation. Finally, the connections between a partition of a set and an equivalence relation are presented. We introduce the following notation of modes: Equivalence Relation, a partition. MML Identifier:EQREL_1. WWW:http://mizar.org/JFM/Vol1/eqrel_1.html The articles [7], [5], [8], [9], [11], [10], [6], [2], [3], [1], and [4] provide the notation and terminology for this paper. For simplicity, we use the following convention: X, Y, x, y, z denote sets, i, j denote natural numbers, A, B denote subsets of X, R, R1, R2 denote binary relations on X, and S1 denotes a family of subsets of [:X, X:]. One can prove the following proposition (1) If i < j, then j − i is a natural number. Let us consider X. The functor ∇X yielding a binary relation on X is defined as follows: (Def. 1) ∇X = [:X, X:]. Let us consider X. Note that ∇X is total and reflexive. Let us consider X and let us consider R1, R2. Then R1 ∩ R2 is a binary relation on X. Then R1 ∪ R2 is a binary relation on X. The following proposition is true (4) 1 idX is reflexive in X and idX is symmetric in X and idX is transitive in X. Let us consider X. A tolerance of X is a total reflexive symmetric binary relation on X. An equivalence relation of X is a total symmetric transitive binary relation on X. One can prove the following propositions: (6) 2 idX is an equivalence relation of X. (7) ∇X is an equivalence relation of X. Let us consider X. Note that ∇X is total, symmetric, and transitive. In the sequel E1, E2, E3 are equivalence relations of X. Next we state several propositions: 1 Supported by RPBP.III-24.C8. 1 The propositions (2) and (3) have been removed. 2 The proposition (5) has been removed.