COH_SP: Coherent Space

proof end;

end;

definition

mode Coherence_Space is non empty subset-closed binary_complete set ;

end;

theorem :: COH_SP:1

for C being Coherence_Space holds {} in C

proof end;

theorem Th2: :: COH_SP:2

for X being set holds bool X is Coherence_Space

proof end;

theorem :: COH_SP:3

{{}} is Coherence_Space by Th2, ZFMISC_1:1;

theorem Th4: :: COH_SP:4

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

proof end;

uniqueness by TOLER_1:25;

end;

:: deftheorem Def2 defines Web COH_SP:def 2 :

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

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 )

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 )

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

proof end;

theorem :: COH_SP:9

for C, D being Coherence_Space st Web C = Web D holds
C = D

proof end;

theorem :: COH_SP:10

for C being Coherence_Space st union C in C holds
C = bool (union C)

proof end;

theorem :: COH_SP:11

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

proof end;

proof end;

end;

:: deftheorem Def3 defines CohSp COH_SP:def 3 :

theorem :: COH_SP:12

for X being set
for E being Tolerance of X holds Web (CohSp E) = E

proof end;

theorem :: COH_SP:13

for C being Coherence_Space holds CohSp (Web C) = C

proof end;

theorem Th14: :: COH_SP:14

for a, X 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

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 4
{ x where x is Subset-Family of X : x is Coherence_Space } ;

end;

:: deftheorem defines CSp COH_SP:def 4 :

registration

let X be set ;

cluster CSp X -> non empty ;

proof end;

end;

registration

let X be set ;

cluster -> non empty subset-closed binary_complete for Element of CSp X;

proof end;

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 )

proof end;

definition

let X be set ;

func FuncsC X -> set equals :: COH_SP:def 5
union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ;

end;

:: deftheorem defines FuncsC COH_SP:def 5 :

registration

let X be set ;

cluster FuncsC X -> functional non empty ;

proof end;

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

proof end;

definition

let X be set ;

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

end;

:: deftheorem defines MapsC COH_SP:def 6 :

registration

let X be set ;

cluster MapsC X -> non empty ;

proof end;

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

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

proof end;

registration

let X be set ;
let l be Element of MapsC X;

cluster l `2 -> Relation-like Function-like for set ;

proof end;

end;

definition

let X be set ;
let l be Element of MapsC X;

func dom l -> Element of CSp X equals :: COH_SP:def 7
(l `1) `1 ;

proof end;

func cod l -> Element of CSp X equals :: COH_SP:def 8
(l `1) `2 ;

proof end;

end;

:: deftheorem defines dom COH_SP:def 7 :

:: deftheorem defines cod COH_SP:def 8 :

theorem Th20: :: COH_SP:20

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 9
[[C,C],(id (union C))];

proof end;

end;

:: deftheorem defines id$ COH_SP:def 9 :

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

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 :Def10: :: COH_SP:def 10
[[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];

proof end;

end;

:: deftheorem Def10 defines * COH_SP:def 10 :

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 )

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

proof end;

theorem :: COH_SP:24

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

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 )

proof end;

definition

let X be set ;

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;

proof end;

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;

proof end;

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

proof end;

proof end;

end;

:: deftheorem Def11 defines CDom COH_SP:def 11 :

:: deftheorem Def12 defines CCod COH_SP:def 12 :

:: deftheorem Def13 defines CComp COH_SP:def 13 :

theorem :: COH_SP:26

canceled;

::$CT

definition

let X be set ;

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

end;

:: deftheorem COH_SP:def 14 :

:: deftheorem defines CohCat COH_SP:def 15 :

registration

let X be set ;

cluster CohCat X -> non empty non void strict Category-like transitive associative reflexive ;

proof end;

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;

registration

let X be set ;

cluster CohCat X -> non empty non void strict with_identities ;

proof end;

end;

definition

let X be set ;

func Toler X -> set means :Def15: :: COH_SP:def 16
for x being set holds
( x in it iff x is Tolerance of X );

proof end;

proof end;

end;

:: deftheorem Def15 defines Toler COH_SP:def 16 :

registration

let X be set ;

cluster Toler X -> non empty ;

proof end;

end;

definition

let X be set ;

func Toler_on_subsets X -> set equals :: COH_SP:def 17
union { (Toler Y) where Y is Subset of X : verum } ;

end;

:: deftheorem defines Toler_on_subsets COH_SP:def 17 :

registration

let X be set ;

cluster Toler_on_subsets X -> non empty ;

proof end;

end;

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

proof end;

theorem :: COH_SP:28

for a being set holds Total a in Toler a by Def15;

theorem Th28: :: COH_SP:29

for X being set holds {} in Toler_on_subsets X

proof end;

theorem Th29: :: COH_SP:30

for a, X being set st a c= X holds
Total a in Toler_on_subsets X

proof end;

theorem Th30: :: COH_SP:31

for a, X being set st a c= X holds
id a in Toler_on_subsets X

proof end;

theorem :: COH_SP:32

for X being set holds Total X in Toler_on_subsets X by Th29;

theorem :: COH_SP:33

for X being set holds id X in Toler_on_subsets X by Th30;

definition

let X be set ;

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

end;

:: deftheorem defines TOL COH_SP:def 18 :

registration

let X be set ;

cluster TOL X -> non empty ;

proof end;

end;

theorem :: COH_SP:34

for X being set holds [{},{}] in TOL X

proof end;

theorem Th34: :: COH_SP:35

for a, X being set st a c= X holds
[(id a),a] in TOL X

proof end;

theorem Th35: :: COH_SP:36

for a, X being set st a c= X holds
[(Total a),a] in TOL X

proof end;

theorem :: COH_SP:37

for X being set holds [(id X),X] in TOL X by Th34;

theorem :: COH_SP:38

for X being set holds [(Total X),X] in TOL X by Th35;

definition

let X be set ;
let T be Element of TOL X;
:: original: `2
redefine func T `2 -> Subset of X;
coherence

proof end;

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

proof end;

end;

definition

let X be set ;

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

end;

:: deftheorem defines FuncsT COH_SP:def 19 :

registration

let X be set ;

cluster FuncsT X -> functional non empty ;

proof end;

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

proof end;

definition

let X be set ;

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

end;

:: deftheorem defines MapsT COH_SP:def 20 :

registration

let X be set ;

cluster MapsT X -> non empty ;

proof end;

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

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

proof end;

registration

let X be set ;
let m be Element of MapsT X;

cluster m `2 -> Relation-like Function-like for set ;

proof end;

end;

definition

let X be set ;
let m be Element of MapsT X;

func dom m -> Element of TOL X equals :: COH_SP:def 21
(m `1) `1 ;

proof end;

func cod m -> Element of TOL X equals :: COH_SP:def 22
(m `1) `2 ;

proof end;

end;

:: deftheorem defines dom COH_SP:def 21 :

:: deftheorem defines cod COH_SP:def 22 :

theorem Th41: :: COH_SP:42

for X being set
for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2)]

proof end;

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;

func id$ T -> Element of MapsT X equals :: COH_SP:def 23
[[T,T],(id (T `2))];

proof end;

end;

:: deftheorem defines id$ COH_SP:def 23 :

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

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 :Def23: :: COH_SP:def 24
[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];

proof end;

end;

:: deftheorem Def23 defines * COH_SP:def 24 :

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 )

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

proof end;

theorem :: COH_SP:46

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

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 )

proof end;

definition

let X be set ;

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;

proof end;

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;

proof end;

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

proof end;

proof end;

end;

:: deftheorem Def24 defines fDom COH_SP:def 25 :

:: deftheorem Def25 defines fCod COH_SP:def 26 :

:: deftheorem Def26 defines fComp COH_SP:def 27 :

definition

let X be set ;

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

end;

:: deftheorem COH_SP:def 28 :

:: deftheorem defines TolCat COH_SP:def 29 :

registration

let X be set ;

cluster TolCat X -> non empty non void strict Category-like transitive associative reflexive ;

proof end;

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;

registration

let X be set ;

cluster TolCat X -> non empty non void strict with_identities ;