:: COH_SP semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let IT be set ;
canceled;
attr IT is binary_complete means :Def2: :: COH_SP:def 2
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;
end;

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

registration
cluster non empty subset-closed binary_complete set ;
existence
ex b1 being set st
( b1 is subset-closed & b1 is binary_complete & not b1 is empty )
proof end;
end;

definition
mode Coherence_Space is non empty subset-closed binary_complete set ;
end;

theorem :: COH_SP:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Coherence_Space holds {} in C
proof end;

theorem Th2: :: COH_SP:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds bool X is Coherence_Space
proof end;

theorem :: COH_SP:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{{} } is Coherence_Space by Th2, ZFMISC_1:1;

theorem Th4: :: COH_SP:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for C being Coherence_Space st x in union C holds
{x} in C
proof end;

definition
let C be Coherence_Space;
func Web C -> Tolerance of union C means :Def3: :: COH_SP:def 3
for x, y being set holds
( [x,y] in it iff ex X being set st
( X in C & x in X & y in X ) );
existence
ex b1 being Tolerance of union C st
for x, y being set holds
( [x,y] in b1 iff ex X being set st
( X in C & x in X & y in X ) )
proof end;
uniqueness
for b1, b2 being Tolerance of union C st ( for x, y being set holds
( [x,y] in b1 iff ex X being set st
( X in C & x in X & y in X ) ) ) & ( 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 ) ) ) holds
b1 = b2
by TOLER_1:52;
end;

:: 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: :: COH_SP:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Coherence_Space
for T being Tolerance of union C holds
( T = Web C iff for x, y being set holds
( [x,y] in T iff {x,y} in C ) )
proof end;

theorem Th6: :: COH_SP:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set
for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
{x,y} in C )
proof end;

theorem Th7: :: COH_SP:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set
for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in Web C )
proof end;

theorem :: COH_SP:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set
for C being Coherence_Space st ( for x, y being set st x in a & y in a holds
{x,y} in C ) holds
a c= union C
proof end;

theorem :: COH_SP:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being Coherence_Space st Web C = Web D holds
C = D
proof end;

theorem :: COH_SP:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Coherence_Space st union C in C holds
C = bool (union C)
proof end;

theorem :: COH_SP:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Coherence_Space st C = bool (union C) holds
Web C = Total (union C)
proof end;

definition
let X be set ;
let E be Tolerance of X;
func CohSp E -> Coherence_Space means :Def4: :: COH_SP:def 4
for a being set holds
( a in it iff for x, y being set st x in a & y in a holds
[x,y] in E );
existence
ex b1 being Coherence_Space st
for a being set holds
( a in b1 iff for x, y being set st x in a & y in a holds
[x,y] in E )
proof end;
uniqueness
for b1, b2 being Coherence_Space st ( for a being set holds
( a in b1 iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) & ( for a being set holds
( a in b2 iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) holds
b1 = b2
proof end;
end;

:: 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 :: COH_SP:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for E being Tolerance of X holds Web (CohSp E) = E
proof end;

theorem :: COH_SP:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Coherence_Space holds CohSp (Web C) = C
proof end;

theorem Th14: :: COH_SP:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, a being set
for E being Tolerance of X holds
( a in CohSp E iff a is TolSet of E )
proof end;

theorem :: COH_SP:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for E being Tolerance of X holds CohSp E = TolSets E
proof end;

definition
let X be set ;
func CSp X -> set equals :: COH_SP:def 5
{ x where x is Subset-Family of X : x is Coherence_Space } ;
coherence
{ x where x is Subset-Family of X : x is Coherence_Space } is set
;
end;

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

registration
let X be set ;
cluster CSp X -> non empty ;
coherence
not CSp X is empty
proof end;
end;

registration
let X be set ;
cluster -> non empty subset-closed binary_complete Element of CSp X;
coherence
for b1 being Element of CSp X holds
( b1 is subset-closed & b1 is binary_complete & not b1 is empty )
proof end;
end;

theorem Th16: :: COH_SP:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x, y being set
for C being Element of CSp X st {x,y} in C holds
( x in union C & y in union C )
proof end;

definition
let X be set ;
canceled;
func FuncsC X -> set equals :: COH_SP:def 7
union { (Funcs (union x),(union y)) where x, y is Element of CSp X : verum } ;
coherence
union { (Funcs (union x),(union y)) where x, y is Element of CSp X : verum } is set
;
end;

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

registration
let X be set ;
cluster FuncsC X -> non empty functional ;
coherence
( not FuncsC X is empty & FuncsC X is functional )
proof end;
end;

theorem Th17: :: COH_SP:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set holds
( x in FuncsC X iff ex C1, C2 being Element of CSp X st
( ( union C2 = {} implies union C1 = {} ) & x is Function of union C1, union C2 ) )
proof end;

definition
let X be set ;
func MapsC X -> set equals :: COH_SP:def 8
{ [[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 ) )
}
;

registration
let X be set ;
cluster MapsC X -> non empty ;
coherence
not MapsC X is empty
proof end;
end;

theorem Th18: :: COH_SP:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for l being Element of MapsC X ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st
( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of union C1, union C2 & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) )
proof end;

theorem Th19: :: COH_SP:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C1, C2 being Element of CSp X
for f being Function of union C1, union C2 st ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds
{(f . x),(f . y)} in C2 ) holds
[[C1,C2],f] in MapsC X
proof end;

registration
let X be set ;
let l be Element of MapsC X;
cluster l `2 -> Relation-like Function-like ;
coherence
( l `2 is Function-like & l `2 is Relation-like )
proof end;
end;

definition
let X be set ;
let l be Element of MapsC X;
canceled;
func dom l -> Element of CSp X equals :: COH_SP:def 10
(l `1 ) `1 ;
coherence
(l `1 ) `1 is Element of CSp X
proof end;
func cod l -> Element of CSp X equals :: COH_SP:def 11
(l `1 ) `2 ;
coherence
(l `1 ) `2 is Element of CSp X
proof end;
end;

:: 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: :: COH_SP:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for l being Element of MapsC X holds l = [[(dom l),(cod l)],(l `2 )]
proof end;

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

definition
let X be set ;
let C be Element of CSp X;
func id$ C -> Element of MapsC X equals :: COH_SP:def 12
[[C,C],(id (union C))];
coherence
[[C,C],(id (union C))] is Element of MapsC X
proof end;
end;

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

theorem Th21: :: COH_SP:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for l being Element of MapsC X holds
( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of union (dom l), union (cod l) & ( for x, y being set st {x,y} in dom l holds
{((l `2 ) . x),((l `2 ) . y)} in cod l ) )
proof end;

definition
let X be set ;
let l1, l2 be Element of MapsC X;
assume A1: cod l1 = dom l2 ;
func l2 * l1 -> Element of MapsC X equals :Def13: :: COH_SP:def 13
[[(dom l1),(cod l2)],((l2 `2 ) * (l1 `2 ))];
coherence
[[(dom l1),(cod l2)],((l2 `2 ) * (l1 `2 ))] is Element of MapsC X
proof end;
end;

:: 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: :: COH_SP:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
( (l2 * l1) `2 = (l2 `2 ) * (l1 `2 ) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 )
proof end;

theorem Th23: :: COH_SP:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for l2, l1, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds
l3 * (l2 * l1) = (l3 * l2) * l1
proof end;

theorem Th24: :: COH_SP:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C being Element of CSp X holds
( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C )
proof end;

theorem Th25: :: COH_SP:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for l being Element of MapsC X holds
( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )
proof end;

definition
let X be set ;
func CDom X -> Function of MapsC X, CSp X means :Def14: :: COH_SP:def 14
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
proof end;
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
proof end;
func CCod X -> Function of MapsC X, CSp X means :Def15: :: COH_SP:def 15
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
proof end;
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
proof end;
func CComp X -> PartFunc of [:(MapsC X),(MapsC X):], MapsC X means :Def16: :: COH_SP:def 16
( ( 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 ) )
proof end;
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
proof end;
func CId X -> Function of CSp X, MapsC X means :Def17: :: COH_SP:def 17
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
proof end;
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
proof end;
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: :: COH_SP:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X),(CId X) #) is Category
proof end;

definition
let X be set ;
func CohCat X -> Category equals :: COH_SP:def 18
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) #);

definition
let X be set ;
func Toler X -> set means :Def19: :: COH_SP:def 19
for x being set holds
( x in it iff x is Tolerance of X );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Tolerance of X )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Tolerance of X ) ) & ( for x being set holds
( x in b2 iff x is Tolerance of X ) ) holds
b1 = b2
proof end;
end;

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

registration
let X be set ;
cluster Toler X -> non empty ;
coherence
not Toler X is empty
proof end;
end;

definition
let X be set ;
func Toler_on_subsets X -> set equals :: COH_SP:def 20
union { (Toler Y) where Y is Subset of X : verum } ;
coherence
union { (Toler Y) where Y is Subset of X : verum } is set
;
end;

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

registration
let X be set ;
cluster Toler_on_subsets X -> non empty ;
coherence
not Toler_on_subsets X is empty
proof end;
end;

theorem :: COH_SP:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set holds
( x in Toler_on_subsets X iff ex A being set st
( A c= X & x is Tolerance of A ) )
proof end;

theorem :: COH_SP:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds Total a in Toler a by Def19;

theorem :: COH_SP:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th30: :: COH_SP:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds {} in Toler_on_subsets X
proof end;

theorem Th31: :: COH_SP:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, X being set st a c= X holds
Total a in Toler_on_subsets X
proof end;

theorem Th32: :: COH_SP:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, X being set st a c= X holds
id a in Toler_on_subsets X
proof end;

theorem :: COH_SP:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Total X in Toler_on_subsets X by Th31;

theorem :: COH_SP:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds id X in Toler_on_subsets X by Th32;

definition
let X be set ;
func TOL X -> set equals :: COH_SP:def 21
{ [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ;
coherence
{ [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } is set
;
end;

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

registration
let X be set ;
cluster TOL X -> non empty ;
coherence
not TOL X is empty
proof end;
end;

theorem :: COH_SP:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds [{} ,{} ] in TOL X
proof end;

theorem Th36: :: COH_SP:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, X being set st a c= X holds
[(id a),a] in TOL X
proof end;

theorem Th37: :: COH_SP:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, X being set st a c= X holds
[(Total a),a] in TOL X
proof end;

theorem :: COH_SP:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds [(id X),X] in TOL X by Th36;

theorem :: COH_SP:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds [(Total X),X] in TOL X by Th37;

definition
let X be set ;
let T be Element of TOL X;
:: original: `2
redefine func T `2 -> Subset of X;
coherence
T `2 is Subset of X
proof end;
:: original: `1
redefine func T `1 -> Tolerance of T `2 ;
coherence
T `1 is Tolerance of T `2
proof end;
end;

definition
let X be set ;
func FuncsT X -> set equals :: COH_SP:def 22
union { (Funcs (T `2 ),(TT `2 )) where T, TT is Element of TOL X : verum } ;
coherence
union { (Funcs (T `2 ),(TT `2 )) where T, TT is Element of TOL X : verum } is set
;
end;

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

registration
let X be set ;
cluster FuncsT X -> non empty functional ;
coherence
( not FuncsT X is empty & FuncsT X is functional )
proof end;
end;

theorem Th40: :: COH_SP:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set holds
( x in FuncsT X iff ex T1, T2 being Element of TOL X st
( ( T2 `2 = {} implies T1 `2 = {} ) & x is Function of T1 `2 ,T2 `2 ) )
proof end;

definition
let X be set ;
func MapsT X -> set equals :: COH_SP:def 23
{ [[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 ) )
}
;

registration
let X be set ;
cluster MapsT X -> non empty ;
coherence
not MapsT X is empty
proof end;
end;

theorem Th41: :: COH_SP:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for m being Element of MapsT X ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of T1 `2 ,T2 `2 & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) )
proof end;

theorem Th42: :: COH_SP:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T1, T2 being Element of TOL X
for f being Function of T1 `2 ,T2 `2 st ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) holds
[[T1,T2],f] in MapsT X
proof end;

registration
let X be set ;
let m be Element of MapsT X;
cluster m `2 -> Relation-like Function-like ;
coherence
( m `2 is Function-like & m `2 is Relation-like )
proof end;
end;

definition
let X be set ;
let m be Element of MapsT X;
canceled;
func dom m -> Element of TOL X equals :: COH_SP:def 25
(m `1 ) `1 ;
coherence
(m `1 ) `1 is Element of TOL X
proof end;
func cod m -> Element of TOL X equals :: COH_SP:def 26
(m `1 ) `2 ;
coherence
(m `1 ) `2 is Element of TOL X
proof end;
end;

:: 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: :: COH_SP:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2 )]
proof end;

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

definition
let X be set ;
let T be Element of TOL X;
func id$ T -> Element of MapsT X equals :: COH_SP:def 27
[[T,T],(id (T `2 ))];
coherence
[[T,T],(id (T `2 ))] is Element of MapsT X
proof end;
end;

:: 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: :: COH_SP:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for m being Element of MapsT X holds
( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of (dom m) `2 ,(cod m) `2 & ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2 ) . x),((m `2 ) . y)] in (cod m) `1 ) )
proof end;

definition
let X be set ;
let m1, m2 be Element of MapsT X;
assume A1: cod m1 = dom m2 ;
func m2 * m1 -> Element of MapsT X equals :Def28: :: COH_SP:def 28
[[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))];
coherence
[[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))] is Element of MapsT X
proof end;
end;

:: 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: :: COH_SP:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2 ) * (m1 `2 ) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
proof end;

theorem Th46: :: COH_SP:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for m2, m1, m3 being Element of MapsT X st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1
proof end;

theorem Th47: :: COH_SP:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Element of TOL X holds
( (id$ T) `2 = id (T `2 ) & dom (id$ T) = T & cod (id$ T) = T )
proof end;

theorem Th48: :: COH_SP:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for m being Element of MapsT X holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
proof end;

definition
let X be set ;
func fDom X -> Function of MapsT X, TOL X means :Def29: :: COH_SP:def 29
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
proof end;
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
proof end;
func fCod X -> Function of MapsT X, TOL X means :Def30: :: COH_SP:def 30
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
proof end;
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
proof end;
func fComp X -> PartFunc of [:(MapsT X),(MapsT X):], MapsT X means :Def31: :: COH_SP:def 31
( ( 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 ) )
proof end;
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
proof end;
func fId X -> Function of TOL X, MapsT X means :Def32: :: COH_SP:def 32
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
proof end;
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
proof end;
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: :: COH_SP:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X),(fId X) #) is Category
proof end;

definition
let X be set ;
func TolCat X -> Category equals :: COH_SP:def 33
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) #);