begin
:: deftheorem COH_SP:def 1 :
canceled;
:: deftheorem Def2 defines binary_complete COH_SP:def 2 :
for IT being set holds
( IT is binary_complete iff for A being set st A c= IT & ( for a, b being set st a in A & b in A holds
a \/ b in IT ) holds
union A in IT );
theorem
theorem Th2:
theorem
theorem Th4:
:: deftheorem Def3 defines Web COH_SP:def 3 :
for C being Coherence_Space
for b2 being Tolerance of (union C) holds
( b2 = Web C iff for x, y being set holds
( [x,y] in b2 iff ex X being set st
( X in C & x in X & y in X ) ) );
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem
theorem
theorem
:: deftheorem Def4 defines CohSp COH_SP:def 4 :
for X being set
for E being Tolerance of X
for b3 being Coherence_Space holds
( b3 = CohSp E iff for a being set holds
( a in b3 iff for x, y being set st x in a & y in a holds
[x,y] in E ) );
theorem
theorem
theorem Th14:
theorem
begin
:: deftheorem defines CSp COH_SP:def 5 :
for X being set holds CSp X = { x where x is Subset-Family of X : x is Coherence_Space } ;
theorem Th16:
:: deftheorem COH_SP:def 6 :
canceled;
:: deftheorem defines FuncsC COH_SP:def 7 :
for X being set holds FuncsC X = union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ;
theorem Th17:
definition
let X be
set ;
func MapsC X -> set equals
{ [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) ) } ;
coherence
{ [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) ) } is set
;
end;
:: deftheorem defines MapsC COH_SP:def 8 :
for X being set holds MapsC X = { [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) ) } ;
theorem Th18:
theorem Th19:
:: deftheorem COH_SP:def 9 :
canceled;
:: deftheorem defines dom COH_SP:def 10 :
for X being set
for l being Element of MapsC X holds dom l = (l `1) `1 ;
:: deftheorem defines cod COH_SP:def 11 :
for X being set
for l being Element of MapsC X holds cod l = (l `1) `2 ;
theorem Th20:
Lm1:
for X being set
for l, l1 being Element of MapsC X st l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 holds
l = l1
:: deftheorem defines id$ COH_SP:def 12 :
for X being set
for C being Element of CSp X holds id$ C = [[C,C],(id (union C))];
Lm2:
for x1, y1, x2, y2, x3, y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds
( x1 = y1 & x2 = y2 )
theorem Th21:
:: deftheorem Def13 defines * COH_SP:def 13 :
for X being set
for l1, l2 being Element of MapsC X st cod l1 = dom l2 holds
l2 * l1 = [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
definition
let X be
set ;
func CDom X -> Function of
(MapsC X),
(CSp X) means :
Def14:
for
l being
Element of
MapsC X holds
it . l = dom l;
existence
ex b1 being Function of (MapsC X),(CSp X) st
for l being Element of MapsC X holds b1 . l = dom l
uniqueness
for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = dom l ) & ( for l being Element of MapsC X holds b2 . l = dom l ) holds
b1 = b2
func CCod X -> Function of
(MapsC X),
(CSp X) means :
Def15:
for
l being
Element of
MapsC X holds
it . l = cod l;
existence
ex b1 being Function of (MapsC X),(CSp X) st
for l being Element of MapsC X holds b1 . l = cod l
uniqueness
for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = cod l ) & ( for l being Element of MapsC X holds b2 . l = cod l ) holds
b1 = b2
func CComp X -> PartFunc of
[:(MapsC X),(MapsC X):],
(MapsC X) means :
Def16:
( ( for
l2,
l1 being
Element of
MapsC X holds
(
[l2,l1] in dom it iff
dom l2 = cod l1 ) ) & ( for
l2,
l1 being
Element of
MapsC X st
dom l2 = cod l1 holds
it . [l2,l1] = l2 * l1 ) );
existence
ex b1 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st
( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) )
uniqueness
for b1, b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b2 . [l2,l1] = l2 * l1 ) holds
b1 = b2
func CId X -> Function of
(CSp X),
(MapsC X) means :
Def17:
for
C being
Element of
CSp X holds
it . C = id$ C;
existence
ex b1 being Function of (CSp X),(MapsC X) st
for C being Element of CSp X holds b1 . C = id$ C
uniqueness
for b1, b2 being Function of (CSp X),(MapsC X) st ( for C being Element of CSp X holds b1 . C = id$ C ) & ( for C being Element of CSp X holds b2 . C = id$ C ) holds
b1 = b2
end;
:: deftheorem Def14 defines CDom COH_SP:def 14 :
for X being set
for b2 being Function of (MapsC X),(CSp X) holds
( b2 = CDom X iff for l being Element of MapsC X holds b2 . l = dom l );
:: deftheorem Def15 defines CCod COH_SP:def 15 :
for X being set
for b2 being Function of (MapsC X),(CSp X) holds
( b2 = CCod X iff for l being Element of MapsC X holds b2 . l = cod l );
:: deftheorem Def16 defines CComp COH_SP:def 16 :
for X being set
for b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) holds
( b2 = CComp X iff ( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b2 . [l2,l1] = l2 * l1 ) ) );
:: deftheorem Def17 defines CId COH_SP:def 17 :
for X being set
for b2 being Function of (CSp X),(MapsC X) holds
( b2 = CId X iff for C being Element of CSp X holds b2 . C = id$ C );
theorem Th26:
definition
let X be
set ;
func CohCat X -> Category equals
CatStr(#
(CSp X),
(MapsC X),
(CDom X),
(CCod X),
(CComp X),
(CId X) #);
coherence
CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X),(CId X) #) is Category
by Th26;
end;
:: deftheorem defines CohCat COH_SP:def 18 :
for X being set holds CohCat X = CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X),(CId X) #);
begin
:: deftheorem Def19 defines Toler COH_SP:def 19 :
for X, b2 being set holds
( b2 = Toler X iff for x being set holds
( x in b2 iff x is Tolerance of X ) );
:: deftheorem defines Toler_on_subsets COH_SP:def 20 :
for X being set holds Toler_on_subsets X = union { (Toler Y) where Y is Subset of X : verum } ;
theorem
theorem
theorem
canceled;
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem
:: deftheorem defines TOL COH_SP:def 21 :
for X being set holds TOL X = { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ;
theorem
theorem Th36:
theorem Th37:
theorem
theorem
:: deftheorem defines FuncsT COH_SP:def 22 :
for X being set holds FuncsT X = union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;
theorem Th40:
definition
let X be
set ;
func MapsT X -> set equals
{ [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) ) } ;
coherence
{ [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) ) } is set
;
end;
:: deftheorem defines MapsT COH_SP:def 23 :
for X being set holds MapsT X = { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) ) } ;
theorem Th41:
theorem Th42:
:: deftheorem COH_SP:def 24 :
canceled;
:: deftheorem defines dom COH_SP:def 25 :
for X being set
for m being Element of MapsT X holds dom m = (m `1) `1 ;
:: deftheorem defines cod COH_SP:def 26 :
for X being set
for m being Element of MapsT X holds cod m = (m `1) `2 ;
theorem Th43:
Lm3:
for X being set
for m, m1 being Element of MapsT X st m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 holds
m = m1
:: deftheorem defines id$ COH_SP:def 27 :
for X being set
for T being Element of TOL X holds id$ T = [[T,T],(id (T `2))];
theorem Th44:
:: deftheorem Def28 defines * COH_SP:def 28 :
for X being set
for m1, m2 being Element of MapsT X st cod m1 = dom m2 holds
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
definition
let X be
set ;
func fDom X -> Function of
(MapsT X),
(TOL X) means :
Def29:
for
m being
Element of
MapsT X holds
it . m = dom m;
existence
ex b1 being Function of (MapsT X),(TOL X) st
for m being Element of MapsT X holds b1 . m = dom m
uniqueness
for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = dom m ) & ( for m being Element of MapsT X holds b2 . m = dom m ) holds
b1 = b2
func fCod X -> Function of
(MapsT X),
(TOL X) means :
Def30:
for
m being
Element of
MapsT X holds
it . m = cod m;
existence
ex b1 being Function of (MapsT X),(TOL X) st
for m being Element of MapsT X holds b1 . m = cod m
uniqueness
for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = cod m ) & ( for m being Element of MapsT X holds b2 . m = cod m ) holds
b1 = b2
func fComp X -> PartFunc of
[:(MapsT X),(MapsT X):],
(MapsT X) means :
Def31:
( ( for
m2,
m1 being
Element of
MapsT X holds
(
[m2,m1] in dom it iff
dom m2 = cod m1 ) ) & ( for
m2,
m1 being
Element of
MapsT X st
dom m2 = cod m1 holds
it . [m2,m1] = m2 * m1 ) );
existence
ex b1 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st
( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) )
uniqueness
for b1, b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) holds
b1 = b2
func fId X -> Function of
(TOL X),
(MapsT X) means :
Def32:
for
T being
Element of
TOL X holds
it . T = id$ T;
existence
ex b1 being Function of (TOL X),(MapsT X) st
for T being Element of TOL X holds b1 . T = id$ T
uniqueness
for b1, b2 being Function of (TOL X),(MapsT X) st ( for T being Element of TOL X holds b1 . T = id$ T ) & ( for T being Element of TOL X holds b2 . T = id$ T ) holds
b1 = b2
end;
:: deftheorem Def29 defines fDom COH_SP:def 29 :
for X being set
for b2 being Function of (MapsT X),(TOL X) holds
( b2 = fDom X iff for m being Element of MapsT X holds b2 . m = dom m );
:: deftheorem Def30 defines fCod COH_SP:def 30 :
for X being set
for b2 being Function of (MapsT X),(TOL X) holds
( b2 = fCod X iff for m being Element of MapsT X holds b2 . m = cod m );
:: deftheorem Def31 defines fComp COH_SP:def 31 :
for X being set
for b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) holds
( b2 = fComp X iff ( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) ) );
:: deftheorem Def32 defines fId COH_SP:def 32 :
for X being set
for b2 being Function of (TOL X),(MapsT X) holds
( b2 = fId X iff for T being Element of TOL X holds b2 . T = id$ T );
theorem Th49:
definition
let X be
set ;
func TolCat X -> Category equals
CatStr(#
(TOL X),
(MapsT X),
(fDom X),
(fCod X),
(fComp X),
(fId X) #);
coherence
CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X),(fId X) #) is Category
by Th49;
end;
:: deftheorem defines TolCat COH_SP:def 33 :
for X being set holds TolCat X = CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X),(fId X) #);