:: by Konrad Raczkowski and Pawe{\l} Sadowski

::

:: Received November 16, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

:: Equivalence Relation and its properties

definition

let X be set ;

let R1, R2 be Relation of X;

:: original: /\

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

coherence

R1 /\ R2 is Relation of X

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

coherence

R1 \/ R2 is Relation of X

end;
let R1, R2 be Relation of X;

:: original: /\

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

coherence

R1 /\ R2 is Relation of X

proof end;

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

coherence

R1 \/ R2 is Relation of X

proof end;

theorem :: EQREL_1:1

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;
mode Tolerance of X is reflexive symmetric total Relation of X;

mode Equivalence_Relation of X is symmetric transitive total Relation of X;

registration

let X be set ;

coherence

( nabla X is total & nabla X is symmetric & nabla X is transitive ) by Th4;

end;
coherence

( nabla X is total & nabla X is symmetric & nabla X is transitive ) by Th4;

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 Th7: :: EQREL_1:7

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

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:8

theorem Th9: :: EQREL_1:9

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 ) )

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

EqR1 /\ EqR2 is Equivalence_Relation of X

end;
let EqR1, EqR2 be Equivalence_Relation of X;

:: original: /\

redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X;

coherence

EqR1 /\ EqR2 is Equivalence_Relation of X

proof end;

theorem Th11: :: EQREL_1:11

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

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 Th12: :: EQREL_1:12

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 ) )

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;

ex b_{1} being Equivalence_Relation of X st

( EqR1 \/ EqR2 c= b_{1} & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds

b_{1} c= EqR ) )
by Th12;

uniqueness

for b_{1}, b_{2} being Equivalence_Relation of X st EqR1 \/ EqR2 c= b_{1} & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds

b_{1} c= EqR ) & EqR1 \/ EqR2 c= b_{2} & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds

b_{2} c= EqR ) holds

b_{1} = b_{2}

for b_{1}, EqR1, EqR2 being Equivalence_Relation of X st EqR1 \/ EqR2 c= b_{1} & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds

b_{1} c= EqR ) holds

( EqR2 \/ EqR1 c= b_{1} & ( for EqR being Equivalence_Relation of X st EqR2 \/ EqR1 c= EqR holds

b_{1} c= EqR ) )
;

idempotence

for EqR1 being Equivalence_Relation of X holds

( EqR1 \/ EqR1 c= EqR1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR1 c= EqR holds

EqR1 c= EqR ) ) ;

end;
let EqR1, EqR2 be Equivalence_Relation of X;

func EqR1 "\/" EqR2 -> Equivalence_Relation of X means :Def2: :: EQREL_1:def 2

( EqR1 \/ EqR2 c= it & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds

it c= EqR ) );

existence ( EqR1 \/ EqR2 c= it & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds

it c= EqR ) );

ex b

( EqR1 \/ EqR2 c= b

b

uniqueness

for b

b

b

b

proof end;

commutativity for b

b

( EqR2 \/ EqR1 c= b

b

idempotence

for EqR1 being Equivalence_Relation of X holds

( EqR1 \/ EqR1 c= EqR1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR1 c= EqR holds

EqR1 c= EqR ) ) ;

:: deftheorem Def2 defines "\/" EQREL_1:def 2 :

for X being set

for EqR1, EqR2, b_{4} being Equivalence_Relation of X holds

( b_{4} = EqR1 "\/" EqR2 iff ( EqR1 \/ EqR2 c= b_{4} & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds

b_{4} c= EqR ) ) );

for X being set

for EqR1, EqR2, b

( b

b

theorem :: EQREL_1:13

for X being set

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

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

proof end;

theorem :: EQREL_1:14

theorem :: EQREL_1:15

for X being set

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

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

theorem :: EQREL_1:16

for X being set

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

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

proof end;

theorem :: EQREL_1:17

for X being set

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

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

proof end;

scheme :: EQREL_1:sch 1

ExEqRel{ F_{1}() -> set , P_{1}[ set , set ] } :

ExEqRel{ F

ex EqR being Equivalence_Relation of F_{1}() st

for x, y being set holds

( [x,y] in EqR iff ( x in F_{1}() & y in F_{1}() & P_{1}[x,y] ) )

providedfor x, y being set holds

( [x,y] in EqR iff ( x in F

A1:
for x being set st x in F_{1}() holds

P_{1}[x,x]
and

A2: for x, y being set st P_{1}[x,y] holds

P_{1}[y,x]
and

A3: for x, y, z being set st P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]

P

A2: for x, y being set st P

P

A3: for x, y, z being set st P

P

proof end;

definition

let X, Y be set ;

let R be Relation of X,Y;

let x be set ;

:: original: Class

redefine func Class (R,x) -> Subset of Y;

coherence

Class (R,x) is Subset of Y

end;
let R be Relation of X,Y;

let x be set ;

:: original: Class

redefine func Class (R,x) -> Subset of Y;

coherence

Class (R,x) is Subset of Y

proof end;

theorem Th19: :: EQREL_1:19

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 )

for R being symmetric total Relation of X holds

( y in Class (R,x) iff [y,x] in R )

proof end;

theorem :: EQREL_1:21

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)

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:22

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

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 Th23: :: EQREL_1:23

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) )

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 Th24: :: EQREL_1:24

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) )

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 Th27: :: EQREL_1:27

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

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:28

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 ) ) )

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 Th29: :: EQREL_1:29

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) )

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:30

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 )

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;

ex b_{1} being Subset-Family of X st

for A being Subset of X holds

( A in b_{1} iff ex x being set st

( x in X & A = Class (EqR,x) ) )

for b_{1}, b_{2} being Subset-Family of X st ( for A being Subset of X holds

( A in b_{1} iff ex x being set st

( x in X & A = Class (EqR,x) ) ) ) & ( for A being Subset of X holds

( A in b_{2} iff ex x being set st

( x in X & A = Class (EqR,x) ) ) ) holds

b_{1} = b_{2}

end;
let EqR be Equivalence_Relation of X;

func Class EqR -> Subset-Family of X means :Def3: :: EQREL_1:def 3

for A being Subset of X holds

( A in it iff ex x being set st

( x in X & A = Class (EqR,x) ) );

existence for A being Subset of X holds

( A in it iff ex x being set st

( x in X & A = Class (EqR,x) ) );

ex b

for A being Subset of X holds

( A in b

( x in X & A = Class (EqR,x) ) )

proof end;

uniqueness for b

( A in b

( x in X & A = Class (EqR,x) ) ) ) & ( for A being Subset of X holds

( A in b

( x in X & A = Class (EqR,x) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines Class EQREL_1:def 3 :

for X being set

for EqR being Equivalence_Relation of X

for b_{3} being Subset-Family of X holds

( b_{3} = Class EqR iff for A being Subset of X holds

( A in b_{3} iff ex x being set st

( x in X & A = Class (EqR,x) ) ) );

for X being set

for EqR being Equivalence_Relation of X

for b

( b

( A in b

( x in X & A = Class (EqR,x) ) ) );

definition

let X be set ;

ex b_{1} being Subset-Family of X st

( union b_{1} = X & ( for A being Subset of X st A in b_{1} holds

( A <> {} & ( for B being Subset of X holds

( not B in b_{1} or A = B or A misses B ) ) ) ) )

end;
mode a_partition of X -> Subset-Family of X means :Def4: :: EQREL_1:def 4

( 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 ( 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 ) ) ) ) );

ex b

( union b

( A <> {} & ( for B being Subset of X holds

( not B in b

proof end;

:: deftheorem Def4 defines a_partition EQREL_1:def 4 :

for X being set

for b_{2} being Subset-Family of X holds

( b_{2} is a_partition of X iff ( union b_{2} = X & ( for A being Subset of X st A in b_{2} holds

( A <> {} & ( for B being Subset of X holds

( not B in b_{2} or A = B or A misses B ) ) ) ) ) );

for X being set

for b

( b

( A <> {} & ( for B being Subset of X holds

( not B in b

theorem Th34: :: EQREL_1:34

for X being set

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

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

proof end;

theorem :: EQREL_1:35

theorem :: EQREL_1:36

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)

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

:: from FSM_1, PARTIT1, 2005.02.06, A.T.

registration

let X be non empty set ;

coherence

for b_{1} being a_partition of X holds not b_{1} is empty

end;
coherence

for b

proof end;

:: from PUA2MSS1

registration

let X be set ;

coherence

for b_{1} being a_partition of X holds b_{1} is with_non-empty_elements

end;
coherence

for b

proof end;

definition

let X be set ;

let R be Equivalence_Relation of X;

:: original: Class

redefine func Class R -> a_partition of X;

coherence

Class R is a_partition of X by Th33;

end;
let R be Equivalence_Relation of X;

:: original: Class

redefine func Class R -> a_partition of X;

coherence

Class R is a_partition of X by Th33;

:: from PRALG_3

registration
end;

registration

let I be non empty set ;

let R be Equivalence_Relation of I;

coherence

Class R is with_non-empty_elements ;

end;
let R be Equivalence_Relation of I;

coherence

Class R is with_non-empty_elements ;

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;
let R be Equivalence_Relation of I;

let x be Element of I;

synonym EqClass (R,x) for Class (I,R);

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

Class (R,x) is Element of Class R

end;
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

Class (R,x) is Element of Class R

proof end;

:: deftheorem defines SmallestPartition EQREL_1:def 5 :

for X being set holds SmallestPartition X = Class (id X);

for X being set holds SmallestPartition X = Class (id X);

definition

let X be non empty set ;

let x be Element of X;

let S1 be a_partition of X;

existence

ex b_{1} being Subset of X st

( x in b_{1} & b_{1} in S1 )

for b_{1}, b_{2} being Subset of X st x in b_{1} & b_{1} in S1 & x in b_{2} & b_{2} in S1 holds

b_{1} = b_{2}

end;
let x be Element of X;

let S1 be a_partition of X;

existence

ex b

( x in b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines EqClass EQREL_1:def 6 :

for X being non empty set

for x being Element of X

for S1 being a_partition of X

for b_{4} being Subset of X holds

( b_{4} = EqClass (x,S1) iff ( x in b_{4} & b_{4} in S1 ) );

for X being non empty set

for x being Element of X

for S1 being a_partition of X

for b

( b

theorem Th38: :: EQREL_1:38

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

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;

definition

let X be set ;

let F be Family-Class of X;

end;
let F be Family-Class of X;

attr F is partition-membered means :Def7: :: EQREL_1:def 7

for S being set st S in F holds

S is a_partition of X;

for S being set st S in F holds

S is a_partition of X;

:: deftheorem Def7 defines partition-membered EQREL_1:def 7 :

for X being set

for F being Family-Class of X holds

( F is partition-membered iff for S being set st S in F holds

S is a_partition of X );

for X being set

for F being Family-Class of X holds

( F is partition-membered iff for S being set st S in F holds

S is a_partition of X );

registration
end;

registration

let X be non empty set ;

existence

not for b_{1} being a_partition of X holds b_{1} is empty

end;
existence

not for b

proof end;

registration
end;

theorem Th41: :: EQREL_1:41

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)

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:42

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)

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;

for b_{1}, b_{2} being non empty a_partition of X st ( for x being Element of X holds EqClass (x,b_{1}) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) & ( for x being Element of X holds EqClass (x,b_{2}) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) holds

b_{1} = b_{2}

ex b_{1} being non empty a_partition of X st

for x being Element of X holds EqClass (x,b_{1}) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }

end;
let 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 } ;

uniqueness for x being Element of X holds EqClass (x,it) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ;

for b

b

proof end;

existence ex b

for x being Element of X holds EqClass (x,b

proof end;

:: deftheorem defines Intersection EQREL_1:def 8 :

for X being non empty set

for F being non empty Part-Family of X

for b_{3} being non empty a_partition of X holds

( b_{3} = Intersection F iff for x being Element of X holds EqClass (x,b_{3}) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } );

for X being non empty set

for F being non empty Part-Family of X

for b

( b

theorem Th43: :: EQREL_1:43

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)

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:44

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

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;

:: Added 2007.10.17, AK

begin

theorem Th49: :: EQREL_1:49

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 )

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 Th50: :: EQREL_1:50

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 )

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:51

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

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:52

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

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:53

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)

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:54

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 }

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 Th55: :: EQREL_1:55

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 `)

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:56

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

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:57

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)}

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:58

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]

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:59

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:]

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:60

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}:]

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:61

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

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:62

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)

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:63

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 `)

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:64

registration

let X be non empty set ;

existence

not for b_{1} being a_partition of X holds b_{1} is empty

end;
existence

not for b

proof end;

definition

let X be non empty set ;

let D be non empty a_partition of X;

ex b_{1} being Function of X,D st

for p being Element of X holds p in b_{1} . p

uniqueness

for b_{1}, b_{2} being Function of X,D st ( for p being Element of X holds p in b_{1} . p ) & ( for p being Element of X holds p in b_{2} . p ) holds

b_{1} = b_{2};

end;
let D be non empty a_partition of X;

func proj D -> Function of X,D means :Def9: :: EQREL_1:def 9

for p being Element of X holds p in it . p;

existence for p being Element of X holds p in it . p;

ex b

for p being Element of X holds p in b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def9 defines proj EQREL_1:def 9 :

for X being non empty set

for D being non empty a_partition of X

for b_{3} being Function of X,D holds

( b_{3} = proj D iff for p being Element of X holds p in b_{3} . p );

for X being non empty set

for D being non empty a_partition of X

for b

( b

theorem Th65: :: EQREL_1:65

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

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:66

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}

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:67

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

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:68

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

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:69

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)

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;

theorem :: EQREL_1:70

for X being set

for P being a_partition of X

for x, a, b being set st x in a & a in P & x in b & b in P holds

a = b

for P being a_partition of X

for x, a, b being set st x in a & a in P & x in b & b in P holds

a = b

proof end;