environ
vocabulary RELAT_1, SETFAM_1, ARYTM_1, BOOLE, RELAT_2, LATTICES, FINSEQ_1,
FUNCT_1, TARSKI, EQREL_1, PARTFUN1, TOLER_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, RELAT_1,
RELAT_2, RELSET_1, SETFAM_1, FINSEQ_1, FUNCT_1, NAT_1, PARTFUN1;
constructors RELAT_2, SETFAM_1, FINSEQ_1, REAL_1, NAT_1, XREAL_0, MEMBERED,
PARTFUN1, ORDERS_1, XBOOLE_0;
clusters RELSET_1, FINSEQ_1, SUBSET_1, XREAL_0, ARYTM_3, ZFMISC_1, PARTFUN1,
XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve X,Y,Z,x,y,y1,y2,z for set;
reserve i,j,k for Nat;
reserve A,B,C for Subset of X;
reserve R,R1,R2 for Relation of X;
reserve AX for Subset of [:X,X:];
reserve SFXX for Subset-Family of [:X,X:];
:: Auxiliary theorems
theorem :: EQREL_1:1
i < j implies j - i is Nat;
:: Equivalence Relation and its properties
definition let X;
func nabla X -> Relation of X equals
:: EQREL_1:def 1
[:X,X:];
end;
definition let X;
cluster nabla X -> total reflexive;
end;
definition let X; let R1,R2;
redefine func R1 /\ R2 -> Relation of X;
func R1 \/ R2 -> Relation of X;
end;
canceled 2;
theorem :: EQREL_1:4
id X is_reflexive_in X & id X is_symmetric_in X &
id X is_transitive_in X;
definition let X;
mode Tolerance of X is total reflexive symmetric Relation of X;
mode Equivalence_Relation of X is total symmetric transitive Relation of X;
end;
canceled;
theorem :: EQREL_1:6
id X is Equivalence_Relation of X;
theorem :: EQREL_1:7
nabla X is Equivalence_Relation of X;
definition let X;
cluster nabla X -> total symmetric transitive;
end;
reserve EqR,EqR1,EqR2,EqR3 for Equivalence_Relation of X;
canceled 3;
theorem :: EQREL_1:11
for R being total reflexive Relation of X holds
x in X implies [x,x] in R;
theorem :: EQREL_1:12
for R being total symmetric Relation of X holds
[x,y] in R implies [y,x] in R;
theorem :: EQREL_1:13
for R being total transitive Relation of X holds
[x,y] in R & [y,z] in R implies [x,z] in R;
theorem :: EQREL_1:14
for R being total reflexive Relation of X holds
(ex x being set st x in X) implies R <> {};
theorem :: EQREL_1:15
for R being total Relation of X holds
field R = X;
theorem :: EQREL_1:16
R is Equivalence_Relation of X iff
R is reflexive symmetric transitive & field R = X;
definition let X; let EqR1,EqR2;
redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X;
end;
theorem :: EQREL_1:17
id X /\ EqR = id X;
theorem :: EQREL_1:18
nabla X /\ R = R;
theorem :: EQREL_1:19
for SFXX st (SFXX <> {} & for Y st Y in SFXX
holds Y is Equivalence_Relation of X)
holds meet SFXX is Equivalence_Relation of X;
theorem :: EQREL_1:20
for R holds ex EqR st R c= EqR & for EqR2 st R c= EqR2 holds EqR c= EqR2;
definition let X; let EqR1,EqR2;
canceled;
func EqR1 "\/" EqR2 -> Equivalence_Relation of X means
:: EQREL_1:def 3
EqR1 \/ EqR2 c= it & for EqR st EqR1 \/ EqR2 c= EqR holds it c= EqR;
end;
canceled;
theorem :: EQREL_1:22
EqR "\/" EqR = EqR;
theorem :: EQREL_1:23
EqR1 "\/" EqR2 = EqR2 "\/" EqR1;
definition let X; let EqR1,EqR2;
redefine func EqR1 "\/" EqR2;
commutativity;
end;
theorem :: EQREL_1:24
EqR1 /\ (EqR1 "\/" EqR2) = EqR1;
theorem :: EQREL_1:25
EqR1 "\/" (EqR1 /\ EqR2) = EqR1;
scheme Ex_Eq_Rel {X() -> set,P[set,set]}:
ex EqR being Equivalence_Relation of X() st
for x,y holds [x,y] in EqR iff x in X() & y in X() & P[x,y]
provided
for x st x in X() holds P[x,x] and
for x,y st P[x,y] holds P[y,x] and
for x,y,z st P[x,y] & P[y,z] holds P[x,z];
:: Classes of abstraction
definition let X be set,
R be Tolerance of X,
x be set;
func Class(R,x) -> Subset of X equals
:: EQREL_1:def 4
R.:{x};
end;
canceled;
theorem :: EQREL_1:27
for R being Tolerance of X holds
y in Class (R,x) iff [y,x] in R;
theorem :: EQREL_1:28
for R being Tolerance of X holds
for x st x in X holds x in Class (R,x);
theorem :: EQREL_1:29
for R being Tolerance of X holds
for x st x in X holds ex y st x in Class(R,y);
theorem :: EQREL_1:30
for R being transitive Tolerance of X holds
y in Class(R,x) & z in Class(R,x) implies [y,z] in R;
theorem :: EQREL_1:31
for x st x in X holds y in Class(EqR,x) iff Class(EqR,x) = Class(EqR,y);
theorem :: EQREL_1:32
for x,y st x in X & y in X holds Class(EqR,x) = Class(EqR,y) or
Class(EqR,x) misses Class(EqR,y);
theorem :: EQREL_1:33
for x st x in X holds Class(id X,x) = {x};
theorem :: EQREL_1:34
for x st x in X holds Class(nabla X,x) = X;
theorem :: EQREL_1:35
(ex x st Class(EqR,x) = X) implies EqR = nabla X;
theorem :: EQREL_1:36
x in X implies ([x,y] in EqR1 "\/" EqR2 iff
ex f being FinSequence st 1 <= len f & x = f.1 & y = f.(len f) &
for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2);
theorem :: EQREL_1:37
for E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x st x in X holds
Class(E,x) = Class(EqR1,x) or Class(E,x) = Class(EqR2,x);
theorem :: EQREL_1:38
EqR1 \/ EqR2 = nabla X implies EqR1 = nabla X or EqR2 = nabla X;
definition let X; let EqR;
func Class EqR -> Subset-Family of X means
:: EQREL_1:def 5
A in it iff ex x st x in X & A = Class(EqR,x);
end;
canceled;
theorem :: EQREL_1:40
X = {} implies Class EqR = {};
definition let X;
mode a_partition of X -> Subset-Family of X means
:: EQREL_1:def 6
union it = X & for A st A in it holds A<>{} &
for B st B in it holds A = B or A misses B if X <> {} otherwise it = {};
end;
canceled;
theorem :: EQREL_1:42
Class EqR is a_partition of X;
theorem :: EQREL_1:43
for P being a_partition of X holds ex EqR st P = Class EqR;
theorem :: EQREL_1:44
for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y);
theorem :: EQREL_1:45
x in Class EqR implies ex y being Element of X st x = Class(EqR,y);