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

:: Equivalence Relation and its properties

definition

let X be set ;

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

coherence
[:X,X:] is Relation of X

proof end;

end;

:: deftheorem defines nabla EQREL_1:def 1 :
for X being set holds nabla X = [:X,X:];

registration

let X be set ;

cluster nabla X -> reflexive total ;

coherence
( nabla X is total & nabla X is reflexive )

proof end;

end;

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

proof end;

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

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

for X being set holds
( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X ) by RELAT_1:def 10;

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

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

theorem Th4: :: EQREL_1:4

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
( nabla X is total & nabla X is symmetric & nabla X is transitive ) by Th4;

end;

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

proof end;

theorem Th5: :: EQREL_1:5

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

proof end;

theorem Th6: :: EQREL_1:6

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

proof end;

theorem Th7: :: EQREL_1:7

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

proof end;

theorem :: EQREL_1:8

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

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 ) ) by ORDERS_1:12, ORDERS_1:13, PARTFUN1:def 2;

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

proof end;

end;

theorem :: EQREL_1:10

for X being set
for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id 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

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

proof end;

definition

let X be set ;
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
ex b₁ being Equivalence_Relation of X st
( EqR1 \/ EqR2 c= b₁ & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b₁ c= EqR ) ) by Th12;
uniqueness
for b₁, b₂ being Equivalence_Relation of X st EqR1 \/ EqR2 c= b₁ & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b₁ c= EqR ) & EqR1 \/ EqR2 c= b₂ & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b₂ c= EqR ) holds
b₁ = b₂ ;
commutativity
for b₁, EqR1, EqR2 being Equivalence_Relation of X st EqR1 \/ EqR2 c= b₁ & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b₁ c= EqR ) holds
( EqR2 \/ EqR1 c= b₁ & ( for EqR being Equivalence_Relation of X st EqR2 \/ EqR1 c= EqR holds
b₁ 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;

:: deftheorem Def2 defines "\/" EQREL_1:def 2 :
for X being set
for EqR1, EqR2, b₄ being Equivalence_Relation of X holds
( b₄ = EqR1 "\/" EqR2 iff ( EqR1 \/ EqR2 c= b₄ & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b₄ c= EqR ) ) );

theorem :: EQREL_1:13

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

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

theorem :: EQREL_1:15

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

proof end;

theorem :: EQREL_1:17

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₁[ object , object ] } :

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

provided

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

proof end;

notation

let R be Relation;
let x be object ;
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 object ;
:: original: Class
redefine func Class (R,x) -> Subset of Y;
coherence
Class (R,x) is Subset of Y

proof end;

end;

theorem :: EQREL_1:18

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

proof end;

theorem Th19: :: EQREL_1:19

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

proof end;

theorem Th20: :: EQREL_1:20

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

proof end;

theorem :: EQREL_1:21

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

proof end;

theorem :: EQREL_1:22

for X being set
for x, y, z being object
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 being set
for y being object
for EqR being Equivalence_Relation of X
for x being object 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 being set
for y being object
for EqR being Equivalence_Relation of X
for x being object 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 object holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )

proof end;

theorem Th25: :: EQREL_1:25

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

proof end;

theorem Th26: :: EQREL_1:26

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

proof end;

theorem Th27: :: EQREL_1:27

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

proof end;

theorem :: EQREL_1:28

for X being set
for x, y being object
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 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 object 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 )

proof end;

definition

let X be set ;
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 object st
( x in X & A = Class (EqR,x) ) );

existence
ex b₁ being Subset-Family of X st
for A being Subset of X holds
( A in b₁ iff ex x being object st
( x in X & A = Class (EqR,x) ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of X st ( for A being Subset of X holds
( A in b₁ iff ex x being object st
( x in X & A = Class (EqR,x) ) ) ) & ( for A being Subset of X holds
( A in b₂ iff ex x being object st
( x in X & A = Class (EqR,x) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Class EQREL_1:def 3 :
for X being set
for EqR being Equivalence_Relation of X
for b₃ being Subset-Family of X holds
( b₃ = Class EqR iff for A being Subset of X holds
( A in b₃ iff ex x being object st
( x in X & A = Class (EqR,x) ) ) );

theorem Th31: :: EQREL_1:31

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 :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
ex b₁ being Subset-Family of X st
( union b₁ = X & ( for A being Subset of X st A in b₁ holds
( A <> {} & ( for B being Subset of X holds
( not B in b₁ or A = B or A misses B ) ) ) ) )

proof end;

end;

:: deftheorem Def4 defines a_partition EQREL_1:def 4 :
for X being set
for b₂ being Subset-Family of X holds
( b₂ is a_partition of X iff ( union b₂ = X & ( for A being Subset of X st A in b₂ holds
( A <> {} & ( for B being Subset of X holds
( not B in b₂ or A = B or A misses B ) ) ) ) ) );

theorem Th32: :: EQREL_1:32

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

proof end;

registration

let X be empty set ;

cluster -> empty for a_partition of X;

coherence
for b₁ being a_partition of X holds b₁ is empty by Th32;

end;

registration

let X be empty set ;

cluster empty trivial proper with_non-empty_elements Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real V29() V30() V31() V32() V34() V35() V36() V38() V39() V40() V50() FinSequence-like FinSubsequence-like FinSequence-membered for a_partition of X;

existence
ex b₁ being a_partition of X st b₁ is empty

proof end;

end;

theorem Th33: :: EQREL_1:33

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

proof end;

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

proof end;

theorem :: EQREL_1:35

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

theorem :: EQREL_1:36

for X being set
for x being object
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;

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

registration

let X be non empty set ;

cluster -> non empty for a_partition of X;

coherence
for b₁ being a_partition of X holds not b₁ is empty

proof end;

end;

:: from PUA2MSS1

registration

let X be set ;

cluster -> with_non-empty_elements for a_partition of X;

coherence
for b₁ being a_partition of X holds b₁ is with_non-empty_elements

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
Class R is a_partition of X by Th33;

end;

:: from PRALG_3

registration

let I be non empty set ;
let R be Equivalence_Relation of I;

cluster Class R -> non empty ;

coherence
not Class R is empty ;

end;

registration

let I be non empty set ;
let R be Equivalence_Relation of I;

cluster Class R -> with_non-empty_elements ;

coherence
Class R is with_non-empty_elements ;

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
Class (R,x) is Element of Class R

proof end;

end;

definition

let X be set ;

func SmallestPartition X -> set equals :: EQREL_1:def 5
Class (id X);

coherence
Class (id X) is set ;

end;

:: deftheorem defines SmallestPartition EQREL_1:def 5 :
for X being set holds SmallestPartition X = Class (id X);

definition

let X be set ;
:: original: SmallestPartition
redefine func SmallestPartition X -> a_partition of X;
correctness
coherence
SmallestPartition X is a_partition of X;
;

end;

theorem :: EQREL_1:37

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 :Def6: :: EQREL_1:def 6
( x in it & it in S1 );

existence
ex b₁ being Subset of X st
( x in b₁ & b₁ in S1 )

proof end;

uniqueness
for b₁, b₂ being Subset of X st x in b₁ & b₁ in S1 & x in b₂ & b₂ in S1 holds
b₁ = b₂ by Def4, XBOOLE_0:3;

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₄ being Subset of X holds
( b₄ = EqClass (x,S1) iff ( x in b₄ & b₄ in S1 ) );

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

proof end;

theorem Th39: :: EQREL_1:39

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

let X be set ;
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;

end;

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

registration

let X be set ;

cluster partition-membered for Element of bool (bool (bool X));

existence
ex b₁ being Family-Class of X st b₁ is partition-membered

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 V39() for a_partition of X;

existence
not for b₁ being a_partition of X holds b₁ is empty

proof end;

end;

theorem Th40: :: EQREL_1:40

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 for Element of bool (bool (bool X));

existence
not for b₁ being Part-Family of X holds b₁ is empty

proof end;

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)

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)

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 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 b₁, b₂ being non empty a_partition of X st ( for x being Element of X holds EqClass (x,b₁) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) & ( for x being Element of X holds EqClass (x,b₂) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) holds
b₁ = b₂

proof end;

existence
ex b₁ being non empty a_partition of X st
for x being Element of X holds EqClass (x,b₁) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }

proof end;

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₃ being non empty a_partition of X holds
( b₃ = Intersection F iff for x being Element of X holds EqClass (x,b₃) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } );

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)

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

proof end;

:: Added 2007.10.17, AK

registration

let A be empty set ;

cluster -> empty for a_partition of A;

coherence
for b₁ being a_partition of A holds b₁ is empty ;

end;

theorem :: EQREL_1:45

{} is a_partition of {}

proof end;

registration

let A be empty set ;

cluster empty trivial proper with_non-empty_elements Relation-like non-empty empty-yielding NAT -defined reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional ext-real V29() V30() V31() V32() V34() V35() V36() V38() V39() V40() V50() FinSequence-like FinSubsequence-like FinSequence-membered for a_partition of A;

existence
ex b₁ being a_partition of A st b₁ is empty

proof end;

end;

theorem :: EQREL_1:46

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

proof end;

theorem Th47: :: EQREL_1:47

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

proof end;

theorem Th48: :: EQREL_1:48

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

proof end;

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 )

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 )

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

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

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)

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 }

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

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

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

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]

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

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

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

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)

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

proof end;

theorem :: EQREL_1:64

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

definition

let X be non empty set ;
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
ex b₁ being Function of X,D st
for p being Element of X holds p in b₁ . p

proof end;

correctness
uniqueness
for b₁, b₂ being Function of X,D st ( for p being Element of X holds p in b₁ . p ) & ( for p being Element of X holds p in b₂ . p ) holds
b₁ = b₂;

proof end;

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₃ being Function of X,D holds
( b₃ = proj D iff for p being Element of X holds p in b₃ . p );

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

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}

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

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

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)

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 by Def4, XBOOLE_0:3;