EQREL_1: Equivalence Relations and Classes of Abstraction

:: Equivalence Relations and Classes of Abstraction
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received November 16, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let X be set ;
func nabla X -> Relation of X equals :: EQREL_1:def 1
[:X,X:];
coherence

proof end;

end;

:: deftheorem defines nabla EQREL_1:def 1 :

registration

let X be set ;
cluster nabla X -> reflexive total ;
coherence

proof end;

end;

definition

let X be set ;
let R1, R2 be Relation of X;
:: original: /\
redefine func R1 /\ R2 -> Relation of X;
coherence

proof end;

:: original: \/
redefine func R1 \/ R2 -> Relation of X;
coherence

proof end;

end;

theorem :: EQREL_1:1

for X being set
for R1 being Relation of X holds (nabla X) \/ R1 = nabla X by XBOOLE_1:12;

theorem :: EQREL_1:2

canceled;

theorem :: EQREL_1:3

canceled;

theorem :: EQREL_1:4

for X being set holds
( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X )

proof end;

definition

let X be set ;
mode Tolerance of X is reflexive symmetric total Relation of X;
mode Equivalence_Relation of X is symmetric transitive total Relation of X;

end;

theorem :: EQREL_1:5

canceled;

theorem :: EQREL_1:6

for X being set holds id X is Equivalence_Relation of X ;

theorem Th7: :: EQREL_1:7

for X being set holds nabla X is Equivalence_Relation of X

proof end;

registration

let X be set ;
cluster nabla X -> symmetric transitive total ;
coherence by Th7;

end;

Lm1: for x, y, X being set
for R being Relation of X st [x,y] in R holds
( x in X & y in X )

proof end;

theorem :: EQREL_1:8

canceled;

theorem :: EQREL_1:9

canceled;

theorem :: EQREL_1:10

canceled;

theorem Th11: :: EQREL_1:11

for X, x being set
for R being reflexive total Relation of X st x in X holds
[x,x] in R

proof end;

theorem Th12: :: EQREL_1:12

for X, x, y being set
for R being symmetric total Relation of X st [x,y] in R holds
[y,x] in R

proof end;

theorem Th13: :: EQREL_1:13

for X, x, y, z being set
for R being transitive total Relation of X st [x,y] in R & [y,z] in R holds
[x,z] in R

proof end;

theorem :: EQREL_1:14

for X being set
for R being reflexive total Relation of X st ex x being set st x in X holds
R <> {} ;

theorem :: EQREL_1:15

canceled;

theorem Th16: :: EQREL_1:16

for X being set
for R being Relation of X holds
( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )

proof end;

definition

let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
:: original: /\
redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X;
coherence

proof end;

end;

theorem :: EQREL_1:17

for X being set
for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X

proof end;

theorem :: EQREL_1:18

canceled;

theorem Th19: :: EQREL_1:19

for X being set
for SFXX being Subset-Family of [:X,X:] st SFXX <> {} & ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) holds
meet SFXX is Equivalence_Relation of X

proof end;

theorem Th20: :: EQREL_1:20

for X being set
for R being Relation of X ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )

proof end;

definition

let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
canceled;
func EqR1 "\/" EqR2 -> Equivalence_Relation of X means :Def3: :: EQREL_1:def 3
( EqR1 \/ EqR2 c= it & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
it c= EqR ) );
existence by Th20;
uniqueness

proof end;

commutativity ;
idempotence ;

end;

:: deftheorem EQREL_1:def 2 :

:: deftheorem Def3 defines "\/" EQREL_1:def 3 :

theorem :: EQREL_1:21

for X being set
for EqR1, EqR2, EqR3 being Equivalence_Relation of X holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)

proof end;

theorem :: EQREL_1:22

for X being set
for EqR being Equivalence_Relation of X holds EqR "\/" EqR = EqR ;

theorem :: EQREL_1:23

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqR2 "\/" EqR1 ;

theorem :: EQREL_1:24

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1

proof end;

theorem :: EQREL_1:25

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" (EqR1 /\ EqR2) = EqR1

proof end;

scheme :: EQREL_1:sch 1
ExEqRel{ F₁() -> set , P₁[ set , set ] } :

ex EqR being Equivalence_Relation of F₁() st
for x, y being set holds
( [x,y] in EqR iff ( x in F₁() & y in F₁() & P₁[x,y] ) )

provided

A1: for x being set st x in F₁() holds
P₁[x,x] and
A2: for x, y being set st P₁[x,y] holds
P₁[y,x] and
A3: for x, y, z being set st P₁[x,y] & P₁[y,z] holds
P₁[x,z]

proof end;

notation

let R be Relation;
let x be set ;
synonym Class (R,x) for Im (R,x);

end;

definition

let X, Y be set ;
let R be Relation of X,Y;
let x be set ;
canceled;
:: original: Class
redefine func Class (R,x) -> Subset of Y;
coherence

proof end;

end;

:: deftheorem EQREL_1:def 4 :

theorem :: EQREL_1:26

for y, x being set
for R being Relation holds
( y in Class (R,x) iff [x,y] in R )

proof end;

theorem Th27: :: EQREL_1:27

for X, y, x being set
for R being symmetric total Relation of X holds
( y in Class (R,x) iff [y,x] in R )

proof end;

theorem Th28: :: EQREL_1:28

for X being set
for R being Tolerance of X
for x being set st x in X holds
x in Class (R,x)

proof end;

theorem :: EQREL_1:29

for X being set
for R being Tolerance of X
for x being set st x in X holds
ex y being set st x in Class (R,y)

proof end;

theorem :: EQREL_1:30

for X, y, x, z being set
for R being transitive Tolerance of X st y in Class (R,x) & z in Class (R,x) holds
[y,z] in R

proof end;

Lm2: for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )

proof end;

theorem Th31: :: EQREL_1:31

for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )

proof end;

theorem Th32: :: EQREL_1:32

for X being set
for EqR being Equivalence_Relation of X
for x, y being set holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )

proof end;

theorem Th33: :: EQREL_1:33

for X, x being set st x in X holds
Class ((id X),x) = {x}

proof end;

theorem Th34: :: EQREL_1:34

for X, x being set st x in X holds
Class ((nabla X),x) = X

proof end;

theorem Th35: :: EQREL_1:35

for X being set
for EqR being Equivalence_Relation of X st ex x being set st Class (EqR,x) = X holds
EqR = nabla X

proof end;

theorem :: EQREL_1:36

for x, X, y being set
for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )

proof end;

theorem Th37: :: EQREL_1:37

for X being set
for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )

proof end;

theorem :: EQREL_1:38

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds
( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )

proof end;

definition

let X be set ;
let EqR be Equivalence_Relation of X;
func Class EqR -> Subset-Family of X means :Def5: :: EQREL_1:def 5
for A being Subset of X holds
( A in it iff ex x being set st
( x in X & A = Class (EqR,x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Class EQREL_1:def 5 :

theorem :: EQREL_1:39

canceled;

theorem Th40: :: EQREL_1:40

for X being set
for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}

proof end;

definition

let X be set ;
mode a_partition of X -> Subset-Family of X means :Def6: :: EQREL_1:def 6
( union it = X & ( for A being Subset of X st A in it holds
( A <> {} & ( for B being Subset of X holds
( not B in it or A = B or A misses B ) ) ) ) );
existence

proof end;

end;

:: deftheorem Def6 defines a_partition EQREL_1:def 6 :

theorem Th41: :: EQREL_1:41

for P being a_partition of {} holds P = {}

proof end;

theorem Th42: :: EQREL_1:42

for X being set
for EqR being Equivalence_Relation of X holds Class EqR is a_partition of X

proof end;

theorem Th43: :: EQREL_1:43

for X being set
for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR

proof end;

theorem :: EQREL_1:44

for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) ) by Lm2;

theorem :: EQREL_1:45

for x, X being set
for EqR being Equivalence_Relation of X st x in Class EqR holds
ex y being Element of X st x = Class (EqR,y)

proof end;

begin

registration

let X be non empty set ;
cluster -> non empty a_partition of X;
coherence

proof end;

end;

registration

let X be set ;
cluster -> with_non-empty_elements a_partition of X;
coherence

proof end;

end;

definition

let X be set ;
let R be Equivalence_Relation of X;
:: original: Class
redefine func Class R -> a_partition of X;
coherence by Th42;

end;

registration

let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R -> non empty ;
coherence ;

end;

registration

let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R -> with_non-empty_elements ;
coherence ;

end;

notation

let I be non empty set ;
let R be Equivalence_Relation of I;
let x be Element of I;
synonym EqClass (R,x) for Class (I,R);

end;

definition

let I be non empty set ;
let R be Equivalence_Relation of I;
let x be Element of I;
:: original: Class
redefine func EqClass (R,x) -> Element of Class R;
coherence

proof end;

end;

definition

let X be set ;
func SmallestPartition X -> a_partition of X equals :: EQREL_1:def 7
Class (id X);
coherence ;

end;

:: deftheorem defines SmallestPartition EQREL_1:def 7 :

theorem :: EQREL_1:46

for X being non empty set holds SmallestPartition X = { {x} where x is Element of X : verum }

proof end;

definition

let X be non empty set ;
let x be Element of X;
let S1 be a_partition of X;
func EqClass (x,S1) -> Subset of X means :Def8: :: EQREL_1:def 8
( x in it & it in S1 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines EqClass EQREL_1:def 8 :

theorem Th47: :: EQREL_1:47

for X being non empty set
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

proof end;

theorem Th48: :: EQREL_1:48

for X being non empty set holds {X} is a_partition of X

proof end;

definition

let X be set ;
mode Family-Class of X is Subset-Family of (bool X);

end;

definition

canceled;
let X be set ;
let F be Family-Class of X;
attr F is partition-membered means :Def10: :: EQREL_1:def 10
for S being set st S in F holds
S is a_partition of X;

end;

:: deftheorem EQREL_1:def 9 :

:: deftheorem Def10 defines partition-membered EQREL_1:def 10 :

registration

let X be set ;
cluster partition-membered Element of bool (bool (bool X));
existence

proof end;

end;

definition

let X be set ;
mode Part-Family of X is partition-membered Family-Class of X;

end;

registration

let X be non empty set ;
cluster non empty with_non-empty_elements a_partition of X;
existence

proof end;

end;

theorem Th49: :: EQREL_1:49

for X being set
for p being a_partition of X holds {p} is Part-Family of X

proof end;

registration

let X be set ;
cluster non empty partition-membered Element of bool (bool (bool X));
existence

proof end;

end;

theorem Th50: :: EQREL_1:50

for X being non empty set
for S1 being a_partition of X
for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)

proof end;

Lm3: for X being non empty set
for x being Element of X
for F being Part-Family of X
for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )

proof end;

theorem :: EQREL_1:51

for A being set
for X being non empty set
for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)

proof end;

definition

let X be non empty set ;
let F be non empty Part-Family of X;
func Intersection F -> non empty a_partition of X means :: EQREL_1:def 11
for x being Element of X holds EqClass (x,it) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem defines Intersection EQREL_1:def 11 :

theorem Th52: :: EQREL_1:52

for X being non empty set
for S being a_partition of X
for A being Subset of S holds (union S) \ (union A) = union (S \ A)

proof end;

theorem :: EQREL_1:53

for X being non empty set
for A being Subset of X
for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A

proof end;

theorem :: EQREL_1:54

{} is a_partition of {}

proof end;

begin

theorem :: EQREL_1:55

for X, X1 being set
for F being Function st X c= F " X1 holds
F .: X c= X1

proof end;

theorem Th56: :: EQREL_1:56

for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e

proof end;

theorem Th57: :: EQREL_1:57

for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e

proof end;

theorem Th58: :: EQREL_1:58

for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )

proof end;

theorem Th59: :: EQREL_1:59

for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )

proof end;

theorem :: EQREL_1:60

for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A

proof end;

theorem :: EQREL_1:61

for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A

proof end;

theorem :: EQREL_1:62

for X being set
for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)

proof end;

theorem :: EQREL_1:63

for X being set
for a being Subset-Family of X holds union (union a) = union { (union A) where A is Subset of X : A in a }

proof end;

theorem Th64: :: EQREL_1:64

for X being set
for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)

proof end;

theorem :: EQREL_1:65

for X, Y, Z being non empty set
for F being Function of X,Y
for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G

proof end;

theorem :: EQREL_1:66

for X, Y, Z being non empty set
for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}

proof end;

theorem :: EQREL_1:67

for X, Y, Z being non empty set
for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]

proof end;

theorem :: EQREL_1:68

for X, Y, Z being non empty set
for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]

proof end;

theorem :: EQREL_1:69

for X, Y, Z being non empty set
for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]

proof end;

theorem :: EQREL_1:70

for X being non empty set
for D being Subset-Family of X
for A being Subset of D holds union A is Subset of X

proof end;

theorem :: EQREL_1:71

for X being set
for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)

proof end;

theorem :: EQREL_1:72

for X being non empty set
for D being a_partition of X
for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A `)

proof end;

theorem :: EQREL_1:73

for X being non empty set
for E being Equivalence_Relation of X holds not Class E is empty ;

registration

let X be non empty set ;
cluster non empty with_non-empty_elements a_partition of X;
existence

proof end;

end;

definition

let X be non empty set ;
let D be non empty a_partition of X;
func proj D -> Function of X,D means :Def12: :: EQREL_1:def 12
for p being Element of X holds p in it . p;
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def12 defines proj EQREL_1:def 12 :

theorem Th74: :: EQREL_1:74

for X being non empty set
for D being non empty a_partition of X
for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p

proof end;

theorem :: EQREL_1:75

for X being non empty set
for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}

proof end;

theorem :: EQREL_1:76

for X being non empty set
for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A

proof end;

theorem :: EQREL_1:77

for X being non empty set
for D being non empty a_partition of X
for W being Element of D ex W9 being Element of X st (proj D) . W9 = W

proof end;

theorem :: EQREL_1:78

for X being non empty set
for D being non empty a_partition of X
for 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)

proof end;