:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski

::

:: Received December 29, 1992

:: Copyright (c) 1992-2019 Association of Mizar Users

:: Coherent Space and Web of Coherent Space

:: deftheorem Def1 defines binary_complete COH_SP:def 1 :

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

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

existence

ex b_{1} being set st

( b_{1} is subset-closed & b_{1} is binary_complete & not b_{1} is empty )

end;
ex b

( b

proof end;

definition

let C be Coherence_Space;

ex b_{1} being Tolerance of (union C) st

for x, y being object holds

( [x,y] in b_{1} iff ex X being set st

( X in C & x in X & y in X ) )

for b_{1}, b_{2} being Tolerance of (union C) st ( for x, y being object holds

( [x,y] in b_{1} iff ex X being set st

( X in C & x in X & y in X ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} iff ex X being set st

( X in C & x in X & y in X ) ) ) holds

b_{1} = b_{2}
by TOLER_1:25;

end;
func Web C -> Tolerance of (union C) means :Def2: :: COH_SP:def 2

for x, y being object holds

( [x,y] in it iff ex X being set st

( X in C & x in X & y in X ) );

existence for x, y being object holds

( [x,y] in it iff ex X being set st

( X in C & x in X & y in X ) );

ex b

for x, y being object holds

( [x,y] in b

( X in C & x in X & y in X ) )

proof end;

uniqueness for b

( [x,y] in b

( X in C & x in X & y in X ) ) ) & ( for x, y being object holds

( [x,y] in b

( X in C & x in X & y in X ) ) ) holds

b

:: deftheorem Def2 defines Web COH_SP:def 2 :

for C being Coherence_Space

for b_{2} being Tolerance of (union C) holds

( b_{2} = Web C iff for x, y being object holds

( [x,y] in b_{2} iff ex X being set st

( X in C & x in X & y in X ) ) );

for C being Coherence_Space

for b

( b

( [x,y] in b

( X in C & x in X & y in X ) ) );

theorem Th5: :: COH_SP:5

for C being Coherence_Space

for T being Tolerance of (union C) holds

( T = Web C iff for x, y being object holds

( [x,y] in T iff {x,y} in C ) )

for T being Tolerance of (union C) holds

( T = Web C iff for x, y being object holds

( [x,y] in T iff {x,y} in C ) )

proof end;

theorem Th6: :: COH_SP:6

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 )

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

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 )

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

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

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;

definition

let X be set ;

let E be Tolerance of X;

ex b_{1} being Coherence_Space st

for a being set holds

( a in b_{1} iff for x, y being set st x in a & y in a holds

[x,y] in E )

for b_{1}, b_{2} being Coherence_Space st ( for a being set holds

( a in b_{1} 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 b_{2} iff for x, y being set st x in a & y in a holds

[x,y] in E ) ) holds

b_{1} = b_{2}

end;
let E be Tolerance of X;

func CohSp E -> Coherence_Space means :Def3: :: COH_SP:def 3

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

ex b

for a being set holds

( a in b

[x,y] in E )

proof end;

uniqueness for b

( a in b

[x,y] in E ) ) & ( for a being set holds

( a in b

[x,y] in E ) ) holds

b

proof end;

:: deftheorem Def3 defines CohSp COH_SP:def 3 :

for X being set

for E being Tolerance of X

for b_{3} being Coherence_Space holds

( b_{3} = CohSp E iff for a being set holds

( a in b_{3} iff for x, y being set st x in a & y in a holds

[x,y] in E ) );

for X being set

for E being Tolerance of X

for b

( b

( a in b

[x,y] in E ) );

definition

let X be set ;

{ x where x is Subset-Family of X : x is Coherence_Space } is set ;

end;
func CSp X -> set equals :: COH_SP:def 4

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

{ x where x is Subset-Family of X : x is Coherence_Space } is set ;

:: deftheorem defines CSp COH_SP:def 4 :

for X being set holds CSp X = { x where x is Subset-Family of X : x is Coherence_Space } ;

for X being set holds CSp X = { x where x is Subset-Family of X : x is Coherence_Space } ;

registration
end;

registration

let X be set ;

coherence

for b_{1} being Element of CSp X holds

( b_{1} is subset-closed & b_{1} is binary_complete & not b_{1} is empty )

end;
coherence

for b

( b

proof end;

theorem Th16: :: COH_SP:16

for x, y, X being set

for C being Element of CSp X st {x,y} in C holds

( x in union C & y in union C )

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 ;

union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } is set ;

end;
func FuncsC X -> set equals :: COH_SP:def 5

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

union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } is set ;

:: deftheorem defines FuncsC COH_SP:def 5 :

for X being set holds FuncsC X = union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ;

for X being set holds FuncsC X = union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ;

registration
end;

theorem Th17: :: COH_SP:17

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

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

{ [[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;
func MapsC X -> set equals :: COH_SP:def 6

{ [[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 ) ) } ;

{ [[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 ;

:: deftheorem defines MapsC COH_SP:def 6 :

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

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

theorem Th18: :: COH_SP:18

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

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

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

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;

coherence

for b_{1} being set st b_{1} = l `2 holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
let l be Element of MapsC X;

coherence

for b

( b

proof end;

definition

let X be set ;

let l be Element of MapsC X;

coherence

(l `1) `1 is Element of CSp X

(l `1) `2 is Element of CSp X

end;
let l be Element of MapsC X;

coherence

(l `1) `1 is Element of CSp X

proof end;

coherence (l `1) `2 is Element of CSp X

proof end;

:: deftheorem defines dom COH_SP:def 7 :

for X being set

for l being Element of MapsC X holds dom l = (l `1) `1 ;

for X being set

for l being Element of MapsC X holds dom l = (l `1) `1 ;

:: deftheorem defines cod COH_SP:def 8 :

for X being set

for l being Element of MapsC X holds cod l = (l `1) `2 ;

for X being set

for l being Element of MapsC X holds cod l = (l `1) `2 ;

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;

coherence

[[C,C],(id (union C))] is Element of MapsC X

end;
let C be Element of CSp X;

coherence

[[C,C],(id (union C))] is Element of MapsC X

proof end;

:: deftheorem defines id$ COH_SP:def 9 :

for X being set

for C being Element of CSp X holds id$ C = [[C,C],(id (union C))];

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

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

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 ;

[[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] is Element of MapsC X

end;
let l1, l2 be Element of MapsC X;

assume A1: cod l1 = dom l2 ;

func l2 * l1 -> Element of MapsC X equals :Def10: :: COH_SP:def 10

[[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];

coherence [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];

[[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] is Element of MapsC X

proof end;

:: deftheorem Def10 defines * COH_SP:def 10 :

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

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

for X being set

for l1, l2 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 )

for l1, l2 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

for X being set

for l1, l2, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds

l3 * (l2 * l1) = (l3 * l2) * l1

for l1, l2, 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 :: COH_SP:24

theorem Th25: :: COH_SP:25

for X being set

for l being Element of MapsC X holds

( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )

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 ;

ex b_{1} being Function of (MapsC X),(CSp X) st

for l being Element of MapsC X holds b_{1} . l = dom l

for b_{1}, b_{2} being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b_{1} . l = dom l ) & ( for l being Element of MapsC X holds b_{2} . l = dom l ) holds

b_{1} = b_{2}

ex b_{1} being Function of (MapsC X),(CSp X) st

for l being Element of MapsC X holds b_{1} . l = cod l

for b_{1}, b_{2} being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b_{1} . l = cod l ) & ( for l being Element of MapsC X holds b_{2} . l = cod l ) holds

b_{1} = b_{2}

ex b_{1} being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st

( ( for l2, l1 being Element of MapsC X holds

( [l2,l1] in dom b_{1} iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds

b_{1} . [l2,l1] = l2 * l1 ) )

for b_{1}, b_{2} being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st ( for l2, l1 being Element of MapsC X holds

( [l2,l1] in dom b_{1} iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds

b_{1} . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds

( [l2,l1] in dom b_{2} iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds

b_{2} . [l2,l1] = l2 * l1 ) holds

b_{1} = b_{2}

end;
func CDom X -> Function of (MapsC X),(CSp X) means :Def11: :: COH_SP:def 11

for l being Element of MapsC X holds it . l = dom l;

existence for l being Element of MapsC X holds it . l = dom l;

ex b

for l being Element of MapsC X holds b

proof end;

uniqueness for b

b

proof end;

func CCod X -> Function of (MapsC X),(CSp X) means :Def12: :: COH_SP:def 12

for l being Element of MapsC X holds it . l = cod l;

existence for l being Element of MapsC X holds it . l = cod l;

ex b

for l being Element of MapsC X holds b

proof end;

uniqueness for b

b

proof end;

func CComp X -> PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) means :Def13: :: COH_SP:def 13

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

ex b

( ( for l2, l1 being Element of MapsC X holds

( [l2,l1] in dom b

b

proof end;

uniqueness for b

( [l2,l1] in dom b

b

( [l2,l1] in dom b

b

b

proof end;

:: deftheorem Def11 defines CDom COH_SP:def 11 :

for X being set

for b_{2} being Function of (MapsC X),(CSp X) holds

( b_{2} = CDom X iff for l being Element of MapsC X holds b_{2} . l = dom l );

for X being set

for b

( b

:: deftheorem Def12 defines CCod COH_SP:def 12 :

for X being set

for b_{2} being Function of (MapsC X),(CSp X) holds

( b_{2} = CCod X iff for l being Element of MapsC X holds b_{2} . l = cod l );

for X being set

for b

( b

:: deftheorem Def13 defines CComp COH_SP:def 13 :

for X being set

for b_{2} being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) holds

( b_{2} = CComp X iff ( ( for l2, l1 being Element of MapsC X holds

( [l2,l1] in dom b_{2} iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds

b_{2} . [l2,l1] = l2 * l1 ) ) );

for X being set

for b

( b

( [l2,l1] in dom b

b

::$CT

definition

let X be set ;

CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #) is non empty non void strict CatStr ;

end;
func CohCat X -> non empty non void strict CatStr equals :: COH_SP:def 15

CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);

coherence CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);

CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #) is non empty non void strict CatStr ;

:: deftheorem defines CohCat COH_SP:def 15 :

for X being set holds CohCat X = CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);

for X being set holds CohCat X = CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);

registration

let X be set ;

coherence

( CohCat X is Category-like & CohCat X is transitive & CohCat X is associative & CohCat X is reflexive )

end;
coherence

( CohCat X is Category-like & CohCat X is transitive & CohCat X is associative & CohCat X is reflexive )

proof end;

Lm3: for X being set

for a being Element of (CohCat X)

for aa being Element of CSp X st a = aa holds

for i being Morphism of a,a st i = id$ aa holds

for b being Element of (CohCat X) holds

( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )

proof end;

definition

let X be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is Tolerance of X )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is Tolerance of X ) ) & ( for x being set holds

( x in b_{2} iff x is Tolerance of X ) ) holds

b_{1} = b_{2}

end;
func Toler X -> set means :Def15: :: COH_SP:def 16

for x being set holds

( x in it iff x is Tolerance of X );

existence for x being set holds

( x in it iff x is Tolerance of X );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def15 defines Toler COH_SP:def 16 :

for X, b_{2} being set holds

( b_{2} = Toler X iff for x being set holds

( x in b_{2} iff x is Tolerance of X ) );

for X, b

( b

( x in b

registration
end;

definition

let X be set ;

union { (Toler Y) where Y is Subset of X : verum } is set ;

end;
func Toler_on_subsets X -> set equals :: COH_SP:def 17

union { (Toler Y) where Y is Subset of X : verum } ;

coherence union { (Toler Y) where Y is Subset of X : verum } ;

union { (Toler Y) where Y is Subset of X : verum } is set ;

:: deftheorem defines Toler_on_subsets COH_SP:def 17 :

for X being set holds Toler_on_subsets X = union { (Toler Y) where Y is Subset of X : verum } ;

for X being set holds Toler_on_subsets X = union { (Toler Y) where Y is Subset of X : verum } ;

theorem :: COH_SP:27

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

( x in Toler_on_subsets X iff ex A being set st

( A c= X & x is Tolerance of A ) )

proof end;

definition

let X be set ;

{ [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } is set ;

end;
func TOL X -> set equals :: COH_SP:def 18

{ [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 } ;

{ [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } is set ;

:: deftheorem defines TOL COH_SP:def 18 :

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

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

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

redefine func T `1 -> Tolerance of (T `2);

coherence

T `1 is Tolerance of (T `2)

end;
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: `1redefine func T `1 -> Tolerance of (T `2);

coherence

T `1 is Tolerance of (T `2)

proof end;

definition

let X be set ;

union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } is set ;

end;
func FuncsT X -> set equals :: COH_SP:def 19

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

union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } is set ;

:: deftheorem defines FuncsT COH_SP:def 19 :

for X being set holds FuncsT X = union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;

for X being set holds FuncsT X = union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;

registration
end;

theorem Th38: :: COH_SP:39

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

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

{ [[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;
func MapsT X -> set equals :: COH_SP:def 20

{ [[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 ) ) } ;

{ [[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 ;

:: deftheorem defines MapsT COH_SP:def 20 :

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

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

theorem Th39: :: COH_SP:40

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

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 Th40: :: COH_SP:41

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

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;

coherence

for b_{1} being set st b_{1} = m `2 holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
let m be Element of MapsT X;

coherence

for b

( b

proof end;

definition

let X be set ;

let m be Element of MapsT X;

coherence

(m `1) `1 is Element of TOL X

(m `1) `2 is Element of TOL X

end;
let m be Element of MapsT X;

coherence

(m `1) `1 is Element of TOL X

proof end;

coherence (m `1) `2 is Element of TOL X

proof end;

:: deftheorem defines dom COH_SP:def 21 :

for X being set

for m being Element of MapsT X holds dom m = (m `1) `1 ;

for X being set

for m being Element of MapsT X holds dom m = (m `1) `1 ;

:: deftheorem defines cod COH_SP:def 22 :

for X being set

for m being Element of MapsT X holds cod m = (m `1) `2 ;

for X being set

for m being Element of MapsT X holds cod m = (m `1) `2 ;

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

coherence

[[T,T],(id (T `2))] is Element of MapsT X

end;
let T be Element of TOL X;

coherence

[[T,T],(id (T `2))] is Element of MapsT X

proof end;

:: deftheorem defines id$ COH_SP:def 23 :

for X being set

for T being Element of TOL X holds id$ T = [[T,T],(id (T `2))];

for X being set

for T being Element of TOL X holds id$ T = [[T,T],(id (T `2))];

theorem Th42: :: COH_SP:43

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

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 ;

[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of MapsT X

end;
let m1, m2 be Element of MapsT X;

assume A1: cod m1 = dom m2 ;

func m2 * m1 -> Element of MapsT X equals :Def23: :: COH_SP:def 24

[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];

coherence [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];

[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of MapsT X

proof end;

:: deftheorem Def23 defines * COH_SP:def 24 :

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

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

for X being set

for m1, m2 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 )

for m1, m2 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 Th44: :: COH_SP:45

for X being set

for m1, m2, m3 being Element of MapsT X st dom m2 = cod m1 & dom m3 = cod m2 holds

m3 * (m2 * m1) = (m3 * m2) * m1

for m1, m2, 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 :: COH_SP:46

theorem Th46: :: COH_SP:47

for X being set

for m being Element of MapsT X holds

( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )

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 ;

ex b_{1} being Function of (MapsT X),(TOL X) st

for m being Element of MapsT X holds b_{1} . m = dom m

for b_{1}, b_{2} being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b_{1} . m = dom m ) & ( for m being Element of MapsT X holds b_{2} . m = dom m ) holds

b_{1} = b_{2}

ex b_{1} being Function of (MapsT X),(TOL X) st

for m being Element of MapsT X holds b_{1} . m = cod m

for b_{1}, b_{2} being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b_{1} . m = cod m ) & ( for m being Element of MapsT X holds b_{2} . m = cod m ) holds

b_{1} = b_{2}

ex b_{1} being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st

( ( for m2, m1 being Element of MapsT X holds

( [m2,m1] in dom b_{1} iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds

b_{1} . [m2,m1] = m2 * m1 ) )

for b_{1}, b_{2} being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st ( for m2, m1 being Element of MapsT X holds

( [m2,m1] in dom b_{1} iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds

b_{1} . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of MapsT X holds

( [m2,m1] in dom b_{2} iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds

b_{2} . [m2,m1] = m2 * m1 ) holds

b_{1} = b_{2}

end;
func fDom X -> Function of (MapsT X),(TOL X) means :Def24: :: COH_SP:def 25

for m being Element of MapsT X holds it . m = dom m;

existence for m being Element of MapsT X holds it . m = dom m;

ex b

for m being Element of MapsT X holds b

proof end;

uniqueness for b

b

proof end;

func fCod X -> Function of (MapsT X),(TOL X) means :Def25: :: COH_SP:def 26

for m being Element of MapsT X holds it . m = cod m;

existence for m being Element of MapsT X holds it . m = cod m;

ex b

for m being Element of MapsT X holds b

proof end;

uniqueness for b

b

proof end;

func fComp X -> PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) means :Def26: :: COH_SP:def 27

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

ex b

( ( for m2, m1 being Element of MapsT X holds

( [m2,m1] in dom b

b

proof end;

uniqueness for b

( [m2,m1] in dom b

b

( [m2,m1] in dom b

b

b

proof end;

:: deftheorem Def24 defines fDom COH_SP:def 25 :

for X being set

for b_{2} being Function of (MapsT X),(TOL X) holds

( b_{2} = fDom X iff for m being Element of MapsT X holds b_{2} . m = dom m );

for X being set

for b

( b

:: deftheorem Def25 defines fCod COH_SP:def 26 :

for X being set

for b_{2} being Function of (MapsT X),(TOL X) holds

( b_{2} = fCod X iff for m being Element of MapsT X holds b_{2} . m = cod m );

for X being set

for b

( b

:: deftheorem Def26 defines fComp COH_SP:def 27 :

for X being set

for b_{2} being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) holds

( b_{2} = fComp X iff ( ( for m2, m1 being Element of MapsT X holds

( [m2,m1] in dom b_{2} iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds

b_{2} . [m2,m1] = m2 * m1 ) ) );

for X being set

for b

( b

( [m2,m1] in dom b

b

definition

let X be set ;

CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #) is non empty non void strict CatStr ;

end;
func TolCat X -> non empty non void strict CatStr equals :: COH_SP:def 29

CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);

coherence CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);

CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #) is non empty non void strict CatStr ;

:: deftheorem defines TolCat COH_SP:def 29 :

for X being set holds TolCat X = CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);

for X being set holds TolCat X = CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);

registration

let X be set ;

coherence

( TolCat X is Category-like & TolCat X is transitive & TolCat X is associative & TolCat X is reflexive )

end;
coherence

( TolCat X is Category-like & TolCat X is transitive & TolCat X is associative & TolCat X is reflexive )

proof end;

Lm5: for X being set

for a being Element of (TolCat X)

for aa being Element of TOL X st a = aa holds

for i being Morphism of a,a st i = id$ aa holds

for b being Element of (TolCat X) holds

( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )

proof end;