:: COH_SP semantic presentation

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 :

:: deftheorem Def2 defines binary_complete COH_SP:def 2 :

registration

cluster non empty subset-closed binary_complete set ;
existence

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

proof end;

uniqueness by TOLER_1:52;

end;

:: deftheorem Def3 defines Web COH_SP:def 3 :

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 set 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 :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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines CohSp COH_SP:def 4 :

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

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 ;

end;

:: deftheorem defines CSp COH_SP:def 5 :

registration

let X be set ;
cluster CSp X -> non empty ;
coherence

proof end;

end;

registration

let X be set ;
cluster -> non empty subset-closed binary_complete Element of CSp X;
coherence

proof end;

end;

theorem Th16: :: COH_SP:16

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 ;

end;

:: deftheorem COH_SP:def 6 :

:: deftheorem defines FuncsC COH_SP:def 7 :

registration

let X be set ;
cluster FuncsC X -> non empty functional ;
coherence

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

end;

:: deftheorem defines MapsC COH_SP:def 8 :

registration

let X be set ;
cluster MapsC X -> non empty ;
coherence

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

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

proof end;

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

proof end;

end;

:: deftheorem COH_SP:def 9 :

:: deftheorem defines dom COH_SP:def 10 :

:: deftheorem defines cod COH_SP:def 11 :

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

proof end;

end;

:: deftheorem defines id$ COH_SP:def 12 :

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

proof end;

end;

:: deftheorem Def13 defines * COH_SP:def 13 :

theorem Th22: :: COH_SP:22

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

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

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

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

proof end;

uniqueness

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

proof end;

uniqueness

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

proof end;

uniqueness

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines CDom COH_SP:def 14 :

:: deftheorem Def15 defines CCod COH_SP:def 15 :

:: deftheorem Def16 defines CComp COH_SP:def 16 :

:: deftheorem Def17 defines CId COH_SP:def 17 :

theorem Th26: :: COH_SP:26

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 by Th26;

end;

:: deftheorem defines CohCat COH_SP:def 18 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines Toler COH_SP:def 19 :

registration

let X be set ;
cluster Toler X -> non empty ;
coherence

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 ;

end;

:: deftheorem defines Toler_on_subsets COH_SP:def 20 :

registration

let X be set ;
cluster Toler_on_subsets X -> non empty ;
coherence

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

theorem :: COH_SP:29

canceled;

theorem Th30: :: COH_SP:30

for X being set holds {} in Toler_on_subsets X

proof end;

theorem Th31: :: COH_SP:31

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

proof end;

theorem Th32: :: COH_SP:32

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

proof end;

theorem :: COH_SP:33

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

theorem :: COH_SP:34

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 ;

end;

:: deftheorem defines TOL COH_SP:def 21 :

registration

let X be set ;
cluster TOL X -> non empty ;
coherence

proof end;

end;

theorem :: COH_SP:35

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

proof end;

theorem Th36: :: COH_SP:36

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

proof end;

theorem Th37: :: COH_SP:37

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

proof end;

theorem :: COH_SP:38

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

theorem :: COH_SP:39

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

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 22
union { (Funcs (T `2 ),(TT `2 )) where T, TT is Element of TOL X : verum } ;
coherence ;

end;

:: deftheorem defines FuncsT COH_SP:def 22 :

registration

let X be set ;
cluster FuncsT X -> non empty functional ;
coherence

proof end;

end;

theorem Th40: :: COH_SP:40

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 ;

end;

:: deftheorem defines MapsT COH_SP:def 23 :

registration

let X be set ;
cluster MapsT X -> non empty ;
coherence

proof end;

end;

theorem Th41: :: COH_SP:41

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

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

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

proof end;

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

proof end;

end;

:: deftheorem COH_SP:def 24 :

:: deftheorem defines dom COH_SP:def 25 :

:: deftheorem defines cod COH_SP:def 26 :

theorem Th43: :: COH_SP:43

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

proof end;

end;

:: deftheorem defines id$ COH_SP:def 27 :

theorem Th44: :: COH_SP:44

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

proof end;

end;

:: deftheorem Def28 defines * COH_SP:def 28 :

theorem Th45: :: COH_SP:45

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

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

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

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

proof end;

uniqueness

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

proof end;

uniqueness

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

proof end;

uniqueness

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines fDom COH_SP:def 29 :

:: deftheorem Def30 defines fCod COH_SP:def 30 :

:: deftheorem Def31 defines fComp COH_SP:def 31 :

:: deftheorem Def32 defines fId COH_SP:def 32 :

theorem Th49: :: COH_SP:49

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 by Th49;

end;

:: deftheorem defines TolCat COH_SP:def 33 :