begin
:: deftheorem defines nabla EQREL_1:def 1 :
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th7:
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 )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
canceled;
theorem Th16:
theorem
theorem
canceled;
theorem Th19:
theorem Th20:
:: deftheorem EQREL_1:def 2 :
canceled;
:: deftheorem Def3 defines "\/" EQREL_1:def 3 :
theorem
theorem
theorem
theorem
theorem
scheme
ExEqRel{
F1()
-> set ,
P1[
set ,
set ] } :
provided
A1:
for
x being
set st
x in F1() holds
P1[
x,
x]
and A2:
for
x,
y being
set st
P1[
x,
y] holds
P1[
y,
x]
and A3:
for
x,
y,
z being
set st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
:: deftheorem EQREL_1:def 4 :
canceled;
theorem
theorem Th27:
theorem Th28:
theorem
theorem
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 )
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem
:: deftheorem Def5 defines Class EQREL_1:def 5 :
theorem
canceled;
theorem Th40:
:: deftheorem Def6 defines a_partition EQREL_1:def 6 :
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem
begin
:: deftheorem defines SmallestPartition EQREL_1:def 7 :
theorem
:: deftheorem Def8 defines EqClass EQREL_1:def 8 :
theorem Th47:
theorem Th48:
:: deftheorem EQREL_1:def 9 :
canceled;
:: deftheorem Def10 defines partition-membered EQREL_1:def 10 :
theorem Th49:
theorem Th50:
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 )
theorem
:: deftheorem defines Intersection EQREL_1:def 11 :
theorem Th52:
theorem
theorem