:: Equivalence Relations and Classes of Abstraction
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received November 16, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ZFMISC_1, SETFAM_1, TARSKI, PARTFUN1,
RELAT_2, XBOOLE_0, FINSEQ_1, XXREAL_0, FUNCT_1, ARYTM_3, ORDINAL4,
ARYTM_1, NAT_1, CARD_1, EQREL_1, MCART_1, CARD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, DOMAIN_1, SUBSET_1,
XCMPLX_0, XXREAL_0, RELAT_1, RELAT_2, SETFAM_1, FINSEQ_1, FUNCT_1,
ORDINAL1, NUMBERS, NAT_1, FUNCT_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1;
constructors SETFAM_1, RELAT_2, PARTFUN1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
RELSET_1, FUNCT_3, BINOP_1, DOMAIN_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, PARTFUN1, XXREAL_0, XREAL_0, FINSEQ_1,
RELAT_1, ORDINAL1, RELSET_1, FUNCT_2, ZFMISC_1, FUNCT_1, RELAT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve X,Y,Z for set, x,y,z for object;
reserve i,j 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:];
:: Equivalence Relation and its properties
definition
let X;
func nabla X -> Relation of X equals
:: EQREL_1:def 1
[:X,X:];
end;
registration
let X;
cluster nabla X -> total reflexive;
end;
definition
let X,R1,R2;
redefine func R1 /\ R2 -> Relation of X;
redefine func R1 \/ R2 -> Relation of X;
end;
theorem :: EQREL_1:1
nabla X \/ R1 = nabla X;
theorem :: EQREL_1:2
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;
theorem :: EQREL_1:3
id X is Equivalence_Relation of X;
theorem :: EQREL_1:4
nabla X is Equivalence_Relation of X;
registration
let X;
cluster nabla X -> total symmetric transitive;
end;
reserve EqR,EqR1,EqR2,EqR3 for Equivalence_Relation of X;
theorem :: EQREL_1:5
for R being total reflexive Relation of X holds x in X implies [x,x] in R;
theorem :: EQREL_1:6
for R being total symmetric Relation of X holds [x,y] in R implies [y,x] in R
;
theorem :: EQREL_1:7
for R being total transitive Relation of X
for x,y being object
holds [x,y] in R & [y,z] in R implies [x,z] in R;
theorem :: EQREL_1:8
for R being total reflexive Relation of X holds
(ex x being set st x in X) implies R <> {};
theorem :: EQREL_1:9
R is Equivalence_Relation of X iff
R is reflexive symmetric transitive & field R = X;
definition
let X,EqR1,EqR2;
redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X;
end;
theorem :: EQREL_1:10
id X /\ EqR = id X;
theorem :: EQREL_1:11
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:12
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;
func EqR1 "\/" EqR2 -> Equivalence_Relation of X means
:: EQREL_1:def 2
EqR1 \/ EqR2 c= it & for EqR st EqR1 \/ EqR2 c= EqR holds it c= EqR;
commutativity;
idempotence;
end;
theorem :: EQREL_1:13
(EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3);
theorem :: EQREL_1:14
EqR "\/" EqR = EqR;
theorem :: EQREL_1:15
EqR1 "\/" EqR2 = EqR2 "\/" EqR1;
theorem :: EQREL_1:16
EqR1 /\ (EqR1 "\/" EqR2) = EqR1;
theorem :: EQREL_1:17
EqR1 "\/" (EqR1 /\ EqR2) = EqR1;
scheme :: EQREL_1:sch 1
ExEqRel {X() -> set,P[object,object]}:
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
notation
let R be Relation, x be object;
synonym Class(R,x) for Im(R,x);
end;
definition
let X, Y be set, R be Relation of X, Y, x be object;
redefine func Class(R,x) -> Subset of Y;
end;
theorem :: EQREL_1:18
for R being Relation holds y in Class (R,x) iff [x,y] in R;
theorem :: EQREL_1:19
for R being total symmetric Relation of X holds y in Class (R,x)
iff [y,x] in R;
theorem :: EQREL_1:20
for R being Tolerance of X holds for x st x in X holds x in Class (R,x);
theorem :: EQREL_1:21
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:22
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:23
for x st x in X holds y in Class(EqR,x) iff Class(EqR,x) = Class (EqR,y);
theorem :: EQREL_1:24
for x,y st y in X holds Class(EqR,x) = Class(EqR,y) or Class(EqR
,x) misses Class(EqR,y);
theorem :: EQREL_1:25
for x st x in X holds Class(id X,x) = {x};
theorem :: EQREL_1:26
for x st x in X holds Class(nabla X,x) = X;
theorem :: EQREL_1:27
(ex x st Class(EqR,x) = X) implies EqR = nabla X;
theorem :: EQREL_1:28
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:29
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:30
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 3
A in it iff ex x st x in X & A = Class(EqR,x);
end;
theorem :: EQREL_1:31
X = {} implies Class EqR = {};
definition
let X;
mode a_partition of X -> Subset-Family of X means
:: EQREL_1:def 4
union it = X &
for A st A in it holds A<>{} & for B st B in it holds A = B or A misses B;
end;
theorem :: EQREL_1:32
for P being a_partition of {} holds P = {};
registration let X be empty set;
cluster -> empty for a_partition of X;
end;
registration let X be empty set;
cluster empty for a_partition of X;
end;
theorem :: EQREL_1:33
Class EqR is a_partition of X;
theorem :: EQREL_1:34
for P being a_partition of X holds ex EqR st P = Class EqR;
theorem :: EQREL_1:35
for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y);
theorem :: EQREL_1:36
x in Class EqR implies ex y being Element of X st x = Class(EqR,y);
begin :: Addenda
:: from FSM_1, PARTIT1, 2005.02.06, A.T.
registration
let X be non empty set;
cluster -> non empty for a_partition of X;
end;
:: from PUA2MSS1
registration
let X be set;
cluster -> with_non-empty_elements for a_partition of X;
end;
definition
let X be set, R be Equivalence_Relation of X;
redefine func Class R -> a_partition of X;
end;
:: from PRALG_3
registration
let I be non empty set, R be Equivalence_Relation of I;
cluster Class R -> non empty;
end;
registration
let I be non empty set, R be Equivalence_Relation of I;
cluster Class R -> with_non-empty_elements;
end;
notation
let I be non empty set, R be Equivalence_Relation of I;
let x be Element of I;
synonym EqClass(R,x) for Class(R,x);
end;
definition
let I be non empty set, R be Equivalence_Relation of I;
let x be Element of I;
redefine func EqClass(R,x) -> Element of Class R;
end;
definition
let X be set;
func SmallestPartition X -> a_partition of X equals
:: EQREL_1:def 5
Class id X;
end;
theorem :: EQREL_1:37
for X being non empty set holds SmallestPartition X = the set of all
{x} where x is
Element of X;
:: from T_1TOPSP, 30.12.2006, AK
:: Classes of partitions of a set
reserve X for non empty set,
x for Element of X;
definition
let X be non empty set,x be Element of X,S1 be a_partition of X;
func EqClass(x,S1) -> Subset of X means
:: EQREL_1:def 6
x in it & it in S1;
end;
theorem :: EQREL_1:38
for S1,S2 being a_partition of X st (for x being Element of X
holds EqClass(x,S1) = EqClass(x,S2)) holds S1=S2;
theorem :: EQREL_1:39
for X being non empty set holds {X} is a_partition of X;
definition
let X be set;
mode Family-Class of X is Subset-Family of bool X;
end;
definition
let X be set;
let F be Family-Class of X;
attr F is partition-membered means
:: EQREL_1:def 7
for S being set st S in F holds S is a_partition of X;
end;
registration
let X be set;
cluster partition-membered for Family-Class of X;
end;
definition
let X be set;
mode Part-Family of X is partition-membered Family-Class of X;
end;
reserve F for Part-Family of X;
registration
let X be non empty set;
cluster non empty for a_partition of X;
end;
theorem :: EQREL_1:40
for X being set, p being a_partition of X holds {p} is Part-Family of X;
registration
let X be set;
cluster non empty for Part-Family of X;
end;
theorem :: EQREL_1:41
for S1 being a_partition of X, x,y being Element of X holds
EqClass(x,S1) meets EqClass(y,S1) implies EqClass(x,S1) = EqClass(y,S1);
theorem :: EQREL_1:42
for A being set,X being non empty set,S being a_partition of X holds A
in S implies ex x being Element of X st A = EqClass(x,S);
definition
let X be non empty set,F be non empty Part-Family of X;
func Intersection F -> non empty a_partition of X means
:: EQREL_1:def 8
for x being Element
of X holds EqClass(x,it) = meet{EqClass(x,S) where S is a_partition of X : S in
F};
end;
theorem :: EQREL_1:43
for X being non empty set, S being a_partition of X, A being
Subset of S holds (union S) \ (union A) = union (S \ A);
theorem :: EQREL_1:44
for X being non empty set,A being Subset of X, S being a_partition of
X holds A in S implies union(S \ {A}) = X \ A;
:: Added 2007.10.17, AK
theorem :: EQREL_1:45
{} is a_partition of {};
begin :: Moved from BORSUK_1, 2010.03.15, A.T.
reserve e,u,v for object, E,X,Y,X1 for set;
theorem :: EQREL_1:46
for F being Function st X c= F"X1 holds F.:X c= X1;
theorem :: EQREL_1:47
E c= [:X,Y:] implies (.:pr1(X,Y)).E = pr1(X,Y).:E;
theorem :: EQREL_1:48
E c= [:X,Y:] implies (.:pr2(X,Y)).E = pr2(X,Y).:E;
theorem :: EQREL_1:49
for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <>
{} holds pr1(X,Y).:[:X1,Y1:] = X1 & pr2(X,Y).:[:X1,Y1:] = Y1;
theorem :: EQREL_1:50
for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <>
{} holds .:pr1(X,Y). [:X1,Y1:] = X1 & .:pr2(X,Y). [:X1,Y1:] = Y1;
theorem :: EQREL_1:51
for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:]
st for E st E in H holds E c= A &
ex X1 being Subset of X, Y1 being Subset of Y
st E =[:X1,Y1:] holds [:union(.:pr1(X,Y).:H), meet(.:pr2(X,Y).:H):] c= A;
theorem :: EQREL_1:52
for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:] st for E
st E in H holds E c= A & ex X1 being Subset of X, Y1 being Subset of Y
st E = [:X1,Y1:]
holds [:meet(.:pr1(X,Y).:H), union(.:pr2(X,Y).:H):] c= A;
theorem :: EQREL_1:53
for X being set, Y being non empty set, f being Function of X,Y
for H being Subset-Family of X holds union(.:f.:H) = f.: union H;
reserve X,Y,Z for non empty set;
theorem :: EQREL_1:54
for X being set, a being Subset-Family of X holds union union a
= union { union A where A is Subset of X: A in a };
theorem :: EQREL_1:55
for X being set for D being Subset-Family of X st union D = X
for A being Subset of D, B being Subset of X st B = union A holds B` c= union A
`;
theorem :: EQREL_1:56
for F being Function of X,Y, G being Function of X,Z st for x,x9
being Element of X st F.x=F.x9 holds G.x=G.x9 ex H being Function of Y,Z st H*F
=G;
theorem :: EQREL_1:57
for X,Y,Z for y being Element of Y, F being (Function of X,Y), G
being Function of Y,Z holds F"{y} c= (G*F)"{G.y};
theorem :: EQREL_1:58
for F being Function of X,Y, x being Element of X, z being
Element of Z holds [:F,id Z:].(x,z) = [F.x,z];
theorem :: EQREL_1:59
for F being Function of X,Y, A being Subset of X, B being Subset
of Z holds [:F,id Z:].:[:A,B:] = [:F.:A,B:];
theorem :: EQREL_1:60
for F being Function of X,Y, y being Element of Y, z being
Element of Z holds [:F,id Z:]"{[y,z]} = [:F"{y},{z}:];
theorem :: EQREL_1:61
for D being Subset-Family of X, A being Subset of D holds
union A is Subset of X;
theorem :: EQREL_1:62
for X being set, D being a_partition of X, A,B being Subset of D
holds union(A /\ B) = union A /\ union B;
theorem :: EQREL_1:63
for D being a_partition of X, A being Subset of D, B being
Subset of X st B = union A holds B` = union A`;
theorem :: EQREL_1:64 :: Class(id X) is non-empty
for E being Equivalence_Relation of X holds Class(E) is non empty;
definition
let X;
let D be non empty a_partition of X;
func proj D -> Function of X, D means
:: EQREL_1:def 9
for p being Element of X holds p in it.p;
end;
theorem :: EQREL_1:65
for D being non empty a_partition of X, p being Element of X, A
being Element of D st p in A holds A = (proj D).p;
theorem :: EQREL_1:66
for D being non empty a_partition of X, p being Element of D
holds p = proj D " {p};
theorem :: EQREL_1:67
for D being non empty a_partition of X, A being Subset of D
holds (proj D)"A = union A;
theorem :: EQREL_1:68
for D being non empty a_partition of X, W being Element of D ex
W9 being Element of X st proj(D).W9=W;
theorem :: EQREL_1:69
for D being non empty a_partition of X, W being Subset of X st
for B being Subset of X st B in D & B meets W holds B c= W holds W = proj D " (
proj D .: W);
theorem :: EQREL_1:70
for X being set, P being a_partition of X, x, a, b being set st
x in a & a in P & x in b & b in P holds a = b;