:: COHSP_1 semantic presentation

Lm1: for X, Y being non empty set
for f being Function of X,Y
for x being Element of X
for y being set st y in f . x holds
y in union Y
by TARSKI:def 4;

definition

let X be set ;
redefine attr X is binary_complete means :Def1: :: COHSP_1:def 1
for A being set st ( for a, b being set st a in A & b in A holds
a \/ b in X ) holds
union A in X;
compatibility

proof end;

end;

:: deftheorem Def1 defines binary_complete COHSP_1:def 1 :

registration

cluster finite set ;
existence by COH_SP:3;

end;

definition

let X be set ;
func FlatCoh X -> set equals :: COHSP_1:def 2
CohSp (id X);
correctness ;
func Sub_of_Fin X -> Subset of X means :Def3: :: COHSP_1:def 3
for x being set holds
( x in it iff ( x in X & x is finite ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem defines FlatCoh COHSP_1:def 2 :

:: deftheorem Def3 defines Sub_of_Fin COHSP_1:def 3 :

theorem Th1: :: COHSP_1:1

for X, x being set holds
( x in FlatCoh X iff ( x = {} or ex y being set st
( x = {y} & y in X ) ) )

proof end;

theorem Th2: :: COHSP_1:2

for X being set holds union (FlatCoh X) = X

proof end;

theorem :: COHSP_1:3

for X being subset-closed finite set holds Sub_of_Fin X = X

proof end;

registration

cluster {{} } -> subset-closed binary_complete ;
coherence by COH_SP:3;
let X be set ;
cluster bool X -> subset-closed binary_complete ;
coherence by COH_SP:2;
cluster FlatCoh X -> non empty subset-closed binary_complete ;
coherence ;

end;

registration

let C be non empty subset-closed set ;
cluster Sub_of_Fin C -> non empty subset-closed ;
coherence

proof end;

end;

theorem :: COHSP_1:4

Web {{} } = {}

proof end;

scheme :: COHSP_1:sch 1
MinimalElementwrtIncl{ F₁() -> set , F₂() -> set , P₁[ set ] } :

ex a being set st
( a in F₂() & P₁[a] & ( for b being set st b in F₂() & P₁[b] & b c= a holds
b = a ) )

provided

A1: F₁() in F₂() and
A2: P₁[F₁()] and
A3: F₁() is finite

proof end;

registration

let C be Coherence_Space;
cluster finite Element of C;
existence

proof end;

end;

definition

let X be set ;
attr X is c=directed means :: COHSP_1:def 4
for Y being finite Subset of X ex a being set st
( union Y c= a & a in X );
attr X is c=filtered means :: COHSP_1:def 5
for Y being finite Subset of X ex a being set st
( ( for y being set st y in Y holds
a c= y ) & a in X );

end;

:: deftheorem defines c=directed COHSP_1:def 4 :

:: deftheorem defines c=filtered COHSP_1:def 5 :

registration

cluster c=directed -> non empty set ;
coherence

proof end;

cluster c=filtered -> non empty set ;
coherence

proof end;

end;

theorem Th5: :: COHSP_1:5

for X being set st X is c=directed holds
for a, b being set st a in X & b in X holds
ex c being set st
( a \/ b c= c & c in X )

proof end;

theorem Th6: :: COHSP_1:6

for X being non empty set st ( for a, b being set st a in X & b in X holds
ex c being set st
( a \/ b c= c & c in X ) ) holds
X is c=directed

proof end;

theorem :: COHSP_1:7

for X being set st X is c=filtered holds
for a, b being set st a in X & b in X holds
ex c being set st
( c c= a /\ b & c in X )

proof end;

theorem Th8: :: COHSP_1:8

for X being non empty set st ( for a, b being set st a in X & b in X holds
ex c being set st
( c c= a /\ b & c in X ) ) holds
X is c=filtered

proof end;

theorem Th9: :: COHSP_1:9

for x being set holds
( {x} is c=directed & {x} is c=filtered )

proof end;

Lm2: now

let x, y be set ; :: thesis:
thus union {x,y,(x \/ y)} = union ({x,y} \/ {(x \/ y)}) by ENUMSET1:43
.= (union {x,y}) \/ (union {(x \/ y)}) by ZFMISC_1:96
.= (x \/ y) \/ (union {(x \/ y)}) by ZFMISC_1:93
.= (x \/ y) \/ (x \/ y) by ZFMISC_1:31
.= x \/ y ; :: thesis:

end;

theorem :: COHSP_1:10

for x, y being set holds {x,y,(x \/ y)} is c=directed

proof end;

theorem :: COHSP_1:11

for x, y being set holds {x,y,(x /\ y)} is c=filtered

proof end;

registration

cluster non empty finite c=directed c=filtered set ;
existence

proof end;

end;

registration

let C be non empty set ;
cluster non empty finite c=directed c=filtered Element of bool C;
existence

proof end;

end;

theorem Th12: :: COHSP_1:12

for X being set holds
( Fin X is c=directed & Fin X is c=filtered )

proof end;

registration

let X be set ;
cluster Fin X -> c=directed c=filtered ;
coherence by Th12;

end;

Lm3: now

let C be non empty subset-closed set ; :: thesis:
let a be Element of C; :: thesis:
thus Fin a c= C :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Fin a ; :: thesis:
then x c= a by FINSUB_1:def 5;
hence x in C by CLASSES1:def 1; :: thesis:

end;

registration

let C be non empty subset-closed set ;
cluster non empty preBoolean Element of bool C;
existence

proof end;

end;

definition

let C be non empty subset-closed set ;
let a be Element of C;
:: original: Fin
redefine func Fin a -> non empty preBoolean Subset of C;
coherence

proof end;

end;

theorem Th13: :: COHSP_1:13

for X being non empty set
for Y being set st X is c=directed & Y c= union X & Y is finite holds
ex Z being set st
( Z in X & Y c= Z )

proof end;

notation

let X be set ;
synonym multiplicative X for cap-closed X;

end;

definition

let X be set ;
canceled;
attr X is d.union-closed means :Def7: :: COHSP_1:def 7
for A being Subset of X st A is c=directed holds
union A in X;

end;

:: deftheorem COHSP_1:def 6 :

:: deftheorem Def7 defines d.union-closed COHSP_1:def 7 :

registration

cluster subset-closed -> multiplicative set ;
coherence

proof end;

end;

theorem :: COHSP_1:14

canceled;

theorem Th15: :: COHSP_1:15

for C being Coherence_Space
for A being c=directed Subset of C holds union A in C

proof end;

registration

cluster -> multiplicative d.union-closed set ;
coherence

proof end;

end;

registration

cluster multiplicative d.union-closed set ;
existence

proof end;

end;

definition

let C be non empty d.union-closed set ;
let A be c=directed Subset of C;
:: original: union
redefine func union A -> Element of C;
coherence by Def7;

end;

definition

let X, Y be set ;
pred X includes_lattice_of Y means :: COHSP_1:def 8
for a, b being set st a in Y & b in Y holds
( a /\ b in X & a \/ b in X );

end;

:: deftheorem defines includes_lattice_of COHSP_1:def 8 :

theorem :: COHSP_1:16

for X being non empty set st X includes_lattice_of X holds
( X is c=directed & X is c=filtered )

proof end;

definition

let X, x, y be set ;
pred X includes_lattice_of x,y means :: COHSP_1:def 9
X includes_lattice_of {x,y};

end;

:: deftheorem defines includes_lattice_of COHSP_1:def 9 :

theorem Th17: :: COHSP_1:17

for X, x, y being set holds
( X includes_lattice_of x,y iff ( x in X & y in X & x /\ y in X & x \/ y in X ) )

proof end;

definition

let f be Function;
attr f is union-distributive means :Def10: :: COHSP_1:def 10
for A being Subset of (dom f) st union A in dom f holds
f . (union A) = union (f .: A);
attr f is d.union-distributive means :Def11: :: COHSP_1:def 11
for A being Subset of (dom f) st A is c=directed & union A in dom f holds
f . (union A) = union (f .: A);

end;

:: deftheorem Def10 defines union-distributive COHSP_1:def 10 :

:: deftheorem Def11 defines d.union-distributive COHSP_1:def 11 :

definition

let f be Function;
attr f is c=-monotone means :Def12: :: COHSP_1:def 12
for a, b being set st a in dom f & b in dom f & a c= b holds
f . a c= f . b;
attr f is cap-distributive means :Def13: :: COHSP_1:def 13
for a, b being set st dom f includes_lattice_of a,b holds
f . (a /\ b) = (f . a) /\ (f . b);

end;

:: deftheorem Def12 defines c=-monotone COHSP_1:def 12 :

:: deftheorem Def13 defines cap-distributive COHSP_1:def 13 :

registration

cluster d.union-distributive -> c=-monotone set ;
coherence

proof end;

cluster union-distributive -> d.union-distributive set ;
coherence

proof end;

end;

theorem :: COHSP_1:18

for f being Function st f is union-distributive holds
for x, y being set st x in dom f & y in dom f & x \/ y in dom f holds
f . (x \/ y) = (f . x) \/ (f . y)

proof end;

theorem Th19: :: COHSP_1:19

for f being Function st f is union-distributive holds
f . {} = {}

proof end;

registration

let C1, C2 be Coherence_Space;
cluster union-distributive d.union-distributive c=-monotone cap-distributive M5(C1,C2);
existence

proof end;

end;

registration

let C be Coherence_Space;
cluster union-distributive d.union-distributive c=-monotone cap-distributive ManySortedSet of C;
existence

proof end;

end;

definition

let f be Function;
attr f is U-continuous means :Def14: :: COHSP_1:def 14
( dom f is d.union-closed & f is d.union-distributive );

end;

:: deftheorem Def14 defines U-continuous COHSP_1:def 14 :

definition

let f be Function;
attr f is U-stable means :Def15: :: COHSP_1:def 15
( dom f is multiplicative & f is U-continuous & f is cap-distributive );

end;

:: deftheorem Def15 defines U-stable COHSP_1:def 15 :

definition

let f be Function;
attr f is U-linear means :Def16: :: COHSP_1:def 16
( f is U-stable & f is union-distributive );

end;

:: deftheorem Def16 defines U-linear COHSP_1:def 16 :

registration

cluster U-continuous -> d.union-distributive c=-monotone set ;
coherence by Def14;
cluster U-stable -> cap-distributive U-continuous set ;
coherence by Def15;
cluster U-linear -> union-distributive d.union-distributive c=-monotone U-stable set ;
coherence by Def16;

end;

registration

let X be d.union-closed set ;
cluster d.union-distributive -> U-continuous ManySortedSet of X;
coherence

proof end;

end;

registration

let X be multiplicative set ;
cluster cap-distributive U-continuous -> U-stable ManySortedSet of X;
coherence

proof end;

end;

registration

cluster union-distributive U-stable -> union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear set ;
coherence by Def16;

end;

registration

cluster union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear set ;
existence

proof end;

let C be Coherence_Space;
cluster union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear ManySortedSet of C;
existence

proof end;

let B be Coherence_Space;
cluster union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear M5(B,C);
existence

proof end;

end;

registration

let f be U-continuous Function;
cluster dom f -> d.union-closed ;
coherence by Def14;

end;

registration

let f be U-stable Function;
cluster dom f -> multiplicative d.union-closed ;
coherence by Def15;

end;

theorem Th20: :: COHSP_1:20

for X being set holds union (Fin X) = X

proof end;

theorem Th21: :: COHSP_1:21

for f being U-continuous Function st dom f is subset-closed holds
for a being set st a in dom f holds
f . a = union (f .: (Fin a))

proof end;

theorem Th22: :: COHSP_1:22

for f being Function st dom f is subset-closed holds
( f is U-continuous iff ( dom f is d.union-closed & f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b ) ) ) )

proof end;

theorem Th23: :: COHSP_1:23

for f being Function st dom f is subset-closed & dom f is d.union-closed holds
( f is U-stable iff ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) ) ) )

proof end;

theorem Th24: :: COHSP_1:24

for f being Function st dom f is subset-closed & dom f is d.union-closed holds
( f is U-linear iff ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x in a & y in f . {x} & ( for b being set st b c= a & y in f . b holds
x in b ) ) ) ) )

proof end;

definition

let f be Function;
func graph f -> set means :Def17: :: COHSP_1:def 17
for x being set holds
( x in it iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines graph COHSP_1:def 17 :

definition

let C1, C2 be non empty set ;
let f be Function of C1,C2;
:: original: graph
redefine func graph f -> Subset of [:C1,(union C2):];
coherence

proof end;

end;

registration

let f be Function;
cluster graph f -> Relation-like ;
coherence

proof end;

end;

theorem Th25: :: COHSP_1:25

for f being Function
for x, y being set holds
( [x,y] in graph f iff ( x is finite & x in dom f & y in f . x ) )

proof end;

theorem Th26: :: COHSP_1:26

for f being c=-monotone Function
for a, b being set st b in dom f & a c= b & b is finite holds
for y being set st [a,y] in graph f holds
[b,y] in graph f

proof end;

theorem Th27: :: COHSP_1:27

for C1, C2 being Coherence_Space
for f being Function of C1,C2
for a being Element of C1
for y1, y2 being set st [a,y1] in graph f & [a,y2] in graph f holds
{y1,y2} in C2

proof end;

theorem :: COHSP_1:28

for C1, C2 being Coherence_Space
for f being c=-monotone Function of C1,C2
for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being set st [a,y1] in graph f & [b,y2] in graph f holds
{y1,y2} in C2

proof end;

theorem Th29: :: COHSP_1:29

for C1, C2 being Coherence_Space
for f, g being U-continuous Function of C1,C2 st graph f = graph g holds
f = g

proof end;

Lm4: for C1, C2 being Coherence_Space
for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in X holds
[b,y] in X ) & ( for a being finite Element of C1
for y1, y2 being set st [a,y1] in X & [a,y2] in X holds
{y1,y2} in C2 ) holds
ex f being U-continuous Function of C1,C2 st
( X = graph f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )

proof end;

theorem :: COHSP_1:30

for C1, C2 being Coherence_Space
for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in X holds
[b,y] in X ) & ( for a being finite Element of C1
for y1, y2 being set st [a,y1] in X & [a,y2] in X holds
{y1,y2} in C2 ) holds
ex f being U-continuous Function of C1,C2 st X = graph f

proof end;

theorem :: COHSP_1:31

for C1, C2 being Coherence_Space
for f being U-continuous Function of C1,C2
for a being Element of C1 holds f . a = (graph f) .: (Fin a)

proof end;

definition

let f be Function;
func Trace f -> set means :Def18: :: COHSP_1:def 18
for x being set holds
( x in it iff ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines Trace COHSP_1:def 18 :

theorem Th32: :: COHSP_1:32

for f being Function
for a, y being set holds
( [a,y] in Trace f iff ( a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) )

proof end;

definition

let C1, C2 be non empty set ;
let f be Function of C1,C2;
:: original: Trace
redefine func Trace f -> Subset of [:C1,(union C2):];
coherence

proof end;

end;

registration

let f be Function;
cluster Trace f -> Relation-like ;
coherence

proof end;

end;

theorem :: COHSP_1:33

for f being U-continuous Function st dom f is subset-closed holds
Trace f c= graph f

proof end;

theorem Th34: :: COHSP_1:34

for f being U-continuous Function st dom f is subset-closed holds
for a, y being set st [a,y] in Trace f holds
a is finite

proof end;

theorem Th35: :: COHSP_1:35

for C1, C2 being Coherence_Space
for f being c=-monotone Function of C1,C2
for a1, a2 being set st a1 \/ a2 in C1 holds
for y1, y2 being set st [a1,y1] in Trace f & [a2,y2] in Trace f holds
{y1,y2} in C2

proof end;

theorem Th36: :: COHSP_1:36

for C1, C2 being Coherence_Space
for f being cap-distributive Function of C1,C2
for a1, a2 being set st a1 \/ a2 in C1 holds
for y being set st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2

proof end;

theorem Th37: :: COHSP_1:37

for C1, C2 being Coherence_Space
for f, g being U-stable Function of C1,C2 st Trace f c= Trace g holds
for a being Element of C1 holds f . a c= g . a

proof end;

theorem Th38: :: COHSP_1:38

for C1, C2 being Coherence_Space
for f, g being U-stable Function of C1,C2 st Trace f = Trace g holds
f = g

proof end;

Lm5: for C1, C2 being Coherence_Space
for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being set st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y being set st [a,y] in X & [b,y] in X holds
a = b ) holds
ex f being U-stable Function of C1,C2 st
( X = Trace f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )

proof end;

theorem Th39: :: COHSP_1:39

for C1, C2 being Coherence_Space
for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being set st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y being set st [a,y] in X & [b,y] in X holds
a = b ) holds
ex f being U-stable Function of C1,C2 st X = Trace f

proof end;

theorem :: COHSP_1:40

for C1, C2 being Coherence_Space
for f being U-stable Function of C1,C2
for a being Element of C1 holds f . a = (Trace f) .: (Fin a)

proof end;

theorem Th41: :: COHSP_1:41

for C1, C2 being Coherence_Space
for f being U-stable Function of C1,C2
for a being Element of C1
for y being set holds
( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )

proof end;

theorem :: COHSP_1:42

for C1, C2 being Coherence_Space ex f being U-stable Function of C1,C2 st Trace f = {}

proof end;

theorem Th43: :: COHSP_1:43

for C1, C2 being Coherence_Space
for a being finite Element of C1
for y being set st y in union C2 holds
ex f being U-stable Function of C1,C2 st Trace f = {[a,y]}

proof end;

theorem :: COHSP_1:44

for C1, C2 being Coherence_Space
for a being Element of C1
for y being set
for f being U-stable Function of C1,C2 st Trace f = {[a,y]} holds
for b being Element of C1 holds
( ( a c= b implies f . b = {y} ) & ( not a c= b implies f . b = {} ) )

proof end;

theorem Th45: :: COHSP_1:45

for C1, C2 being Coherence_Space
for f being U-stable Function of C1,C2
for X being Subset of (Trace f) ex g being U-stable Function of C1,C2 st Trace g = X

proof end;

theorem Th46: :: COHSP_1:46

for C1, C2 being Coherence_Space
for A being set st ( for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f ) holds
ex f being U-stable Function of C1,C2 st union A = Trace f

proof end;

definition

let C1, C2 be Coherence_Space;
func StabCoh C1,C2 -> set means :Def19: :: COHSP_1:def 19
for x being set holds
( x in it iff ex f being U-stable Function of C1,C2 st x = Trace f );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def19 defines StabCoh COHSP_1:def 19 :

registration

let C1, C2 be Coherence_Space;
cluster StabCoh C1,C2 -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem Th47: :: COHSP_1:47

for C1, C2 being Coherence_Space
for f being U-stable Function of C1,C2 holds Trace f c= [:(Sub_of_Fin C1),(union C2):]

proof end;

theorem :: COHSP_1:48

for C1, C2 being Coherence_Space holds union (StabCoh C1,C2) = [:(Sub_of_Fin C1),(union C2):]

proof end;

theorem Th49: :: COHSP_1:49

for C1, C2 being Coherence_Space
for a, b being finite Element of C1
for y1, y2 being set holds
( [[a,y1],[b,y2]] in Web (StabCoh C1,C2) iff ( ( not a \/ b in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) )

proof end;

theorem Th50: :: COHSP_1:50

for C1, C2 being Coherence_Space
for f being U-stable Function of C1,C2 holds
( f is U-linear iff for a, y being set st [a,y] in Trace f holds
ex x being set st a = {x} )

proof end;

definition

let f be Function;
func LinTrace f -> set means :Def20: :: COHSP_1:def 20
for x being set holds
( x in it iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def20 defines LinTrace COHSP_1:def 20 :

theorem Th51: :: COHSP_1:51

for f being Function
for x, y being set holds
( [x,y] in LinTrace f iff [{x},y] in Trace f )

proof end;

theorem Th52: :: COHSP_1:52

for f being Function st f . {} = {} holds
for x, y being set st {x} in dom f & y in f . {x} holds
[x,y] in LinTrace f

proof end;

theorem Th53: :: COHSP_1:53

for f being Function
for x, y being set st [x,y] in LinTrace f holds
( {x} in dom f & y in f . {x} )

proof end;

definition

let C1, C2 be non empty set ;
let f be Function of C1,C2;
:: original: LinTrace
redefine func LinTrace f -> Subset of [:(union C1),(union C2):];
coherence

proof end;

end;

registration

let f be Function;
cluster LinTrace f -> Relation-like ;
coherence

proof end;

end;

definition

let C1, C2 be Coherence_Space;
func LinCoh C1,C2 -> set means :Def21: :: COHSP_1:def 21
for x being set holds
( x in it iff ex f being U-linear Function of C1,C2 st x = LinTrace f );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def21 defines LinCoh COHSP_1:def 21 :

theorem Th54: :: COHSP_1:54

for C1, C2 being Coherence_Space
for f being c=-monotone Function of C1,C2
for x1, x2 being set st {x1,x2} in C1 holds
for y1, y2 being set st [x1,y1] in LinTrace f & [x2,y2] in LinTrace f holds
{y1,y2} in C2

proof end;

theorem Th55: :: COHSP_1:55

for C1, C2 being Coherence_Space
for f being cap-distributive Function of C1,C2
for x1, x2 being set st {x1,x2} in C1 holds
for y being set st [x1,y] in LinTrace f & [x2,y] in LinTrace f holds
x1 = x2

proof end;

theorem Th56: :: COHSP_1:56

for C1, C2 being Coherence_Space
for f, g being U-linear Function of C1,C2 st LinTrace f = LinTrace g holds
f = g

proof end;

Lm6: for C1, C2 being Coherence_Space
for X being Subset of [:(union C1),(union C2):] st ( for a, b being set st {a,b} in C1 holds
for y1, y2 being set st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds
for y being set st [a,y] in X & [b,y] in X holds
a = b ) holds
ex f being U-linear Function of C1,C2 st
( X = LinTrace f & ( for a being Element of C1 holds f . a = X .: a ) )

proof end;

theorem Th57: :: COHSP_1:57

for C1, C2 being Coherence_Space
for X being Subset of [:(union C1),(union C2):] st ( for a, b being set st {a,b} in C1 holds
for y1, y2 being set st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds
for y being set st [a,y] in X & [b,y] in X holds
a = b ) holds
ex f being U-linear Function of C1,C2 st X = LinTrace f

proof end;

theorem :: COHSP_1:58

for C1, C2 being Coherence_Space
for f being U-linear Function of C1,C2
for a being Element of C1 holds f . a = (LinTrace f) .: a

proof end;

theorem :: COHSP_1:59

for C1, C2 being Coherence_Space ex f being U-linear Function of C1,C2 st LinTrace f = {}

proof end;

theorem Th60: :: COHSP_1:60

for C1, C2 being Coherence_Space
for x, y being set st x in union C1 & y in union C2 holds
ex f being U-linear Function of C1,C2 st LinTrace f = {[x,y]}

proof end;

theorem :: COHSP_1:61

for C1, C2 being Coherence_Space
for x, y being set st x in union C1 & y in union C2 holds
for f being U-linear Function of C1,C2 st LinTrace f = {[x,y]} holds
for a being Element of C1 holds
( ( x in a implies f . a = {y} ) & ( not x in a implies f . a = {} ) )

proof end;

theorem Th62: :: COHSP_1:62

for C1, C2 being Coherence_Space
for f being U-linear Function of C1,C2
for X being Subset of (LinTrace f) ex g being U-linear Function of C1,C2 st LinTrace g = X

proof end;

theorem Th63: :: COHSP_1:63

for C1, C2 being Coherence_Space
for A being set st ( for x, y being set st x in A & y in A holds
ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f ) holds
ex f being U-linear Function of C1,C2 st union A = LinTrace f

proof end;

registration

let C1, C2 be Coherence_Space;
cluster LinCoh C1,C2 -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem :: COHSP_1:64

for C1, C2 being Coherence_Space holds union (LinCoh C1,C2) = [:(union C1),(union C2):]

proof end;

theorem :: COHSP_1:65

for C1, C2 being Coherence_Space
for x1, x2, y1, y2 being set holds
( [[x1,y1],[x2,y2]] in Web (LinCoh C1,C2) iff ( x1 in union C1 & x2 in union C1 & ( ( not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies x1 = x2 ) ) ) ) )

proof end;

definition

let C be Coherence_Space;
func 'not' C -> set equals :: COHSP_1:def 22
{ a where a is Subset of (union C) : for b being Element of C ex x being set st a /\ b c= {x} } ;
correctness ;

end;

:: deftheorem defines 'not' COHSP_1:def 22 :

theorem Th66: :: COHSP_1:66

for C being Coherence_Space
for x being set holds
( x in 'not' C iff ( x c= union C & ( for a being Element of C ex z being set st x /\ a c= {z} ) ) )

proof end;

registration

let C be Coherence_Space;
cluster 'not' C -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem Th67: :: COHSP_1:67

for C being Coherence_Space holds union ('not' C) = union C

proof end;

theorem Th68: :: COHSP_1:68

for C being Coherence_Space
for x, y being set st x <> y & {x,y} in C holds
not {x,y} in 'not' C

proof end;

theorem Th69: :: COHSP_1:69

for C being Coherence_Space
for x, y being set st {x,y} c= union C & not {x,y} in C holds
{x,y} in 'not' C

proof end;

theorem :: COHSP_1:70

for C being Coherence_Space
for x, y being set holds
( [x,y] in Web ('not' C) iff ( x in union C & y in union C & ( x = y or not [x,y] in Web C ) ) )

proof end;

Lm7: for C being Coherence_Space holds 'not' ('not' C) c= C

proof end;

theorem Th71: :: COHSP_1:71

for C being Coherence_Space holds 'not' ('not' C) = C

proof end;

theorem :: COHSP_1:72

'not' {{} } = {{} }

proof end;

theorem :: COHSP_1:73

for X being set holds
( 'not' (FlatCoh X) = bool X & 'not' (bool X) = FlatCoh X )

proof end;

definition

let x, y be set ;
func x U+ y -> set equals :: COHSP_1:def 23
Union (disjoin <*x,y*>);
correctness ;

end;

:: deftheorem defines U+ COHSP_1:def 23 :

theorem Th74: :: COHSP_1:74

for x, y being set holds x U+ y = [:x,{1}:] \/ [:y,{2}:]

proof end;

theorem Th75: :: COHSP_1:75

for x being set holds
( x U+ {} = [:x,{1}:] & {} U+ x = [:x,{2}:] )

proof end;

theorem Th76: :: COHSP_1:76

for x, y, z being set st z in x U+ y holds
( z = [(z `1 ),(z `2 )] & ( ( z `2 = 1 & z `1 in x ) or ( z `2 = 2 & z `1 in y ) ) )

proof end;

theorem Th77: :: COHSP_1:77

for x, y, z being set holds
( [z,1] in x U+ y iff z in x )

proof end;

theorem Th78: :: COHSP_1:78

for x, y, z being set holds
( [z,2] in x U+ y iff z in y )

proof end;

theorem Th79: :: COHSP_1:79

for x1, y1, x2, y2 being set holds
( x1 U+ y1 c= x2 U+ y2 iff ( x1 c= x2 & y1 c= y2 ) )

proof end;

theorem Th80: :: COHSP_1:80

for x, y, z being set st z c= x U+ y holds
ex x1, y1 being set st
( z = x1 U+ y1 & x1 c= x & y1 c= y )

proof end;

theorem Th81: :: COHSP_1:81

for x1, y1, x2, y2 being set holds
( x1 U+ y1 = x2 U+ y2 iff ( x1 = x2 & y1 = y2 ) )

proof end;

theorem Th82: :: COHSP_1:82

for x1, y1, x2, y2 being set holds (x1 U+ y1) \/ (x2 U+ y2) = (x1 \/ x2) U+ (y1 \/ y2)

proof end;

theorem Th83: :: COHSP_1:83

for x1, y1, x2, y2 being set holds (x1 U+ y1) /\ (x2 U+ y2) = (x1 /\ x2) U+ (y1 /\ y2)

proof end;

definition

let C1, C2 be Coherence_Space;
func C1 "/\" C2 -> set equals :: COHSP_1:def 24
{ (a U+ b) where a is Element of C1, b is Element of C2 : verum } ;
correctness ;
func C1 "\/" C2 -> set equals :: COHSP_1:def 25
{ (a U+ {} ) where a is Element of C1 : verum } \/ { ({} U+ b) where b is Element of C2 : verum } ;
correctness ;

end;

:: deftheorem defines "/\" COHSP_1:def 24 :

:: deftheorem defines "\/" COHSP_1:def 25 :

theorem Th84: :: COHSP_1:84

for C1, C2 being Coherence_Space
for x being set holds
( x in C1 "/\" C2 iff ex a being Element of C1 ex b being Element of C2 st x = a U+ b ) ;

theorem Th85: :: COHSP_1:85

for C1, C2 being Coherence_Space
for x, y being set holds
( x U+ y in C1 "/\" C2 iff ( x in C1 & y in C2 ) )

proof end;

theorem Th86: :: COHSP_1:86

for C1, C2 being Coherence_Space holds union (C1 "/\" C2) = (union C1) U+ (union C2)

proof end;

theorem Th87: :: COHSP_1:87

for C1, C2 being Coherence_Space
for x, y being set holds
( x U+ y in C1 "\/" C2 iff ( ( x in C1 & y = {} ) or ( x = {} & y in C2 ) ) )

proof end;

theorem Th88: :: COHSP_1:88

for C1, C2 being Coherence_Space
for x being set st x in C1 "\/" C2 holds
ex a being Element of C1 ex b being Element of C2 st
( x = a U+ b & ( a = {} or b = {} ) )

proof end;

theorem :: COHSP_1:89

for C1, C2 being Coherence_Space holds union (C1 "\/" C2) = (union C1) U+ (union C2)

proof end;

registration

let C1, C2 be Coherence_Space;
cluster C1 "/\" C2 -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

cluster C1 "\/" C2 -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem :: COHSP_1:90

for C1, C2 being Coherence_Space
for x, y being set holds
( [[x,1],[y,1]] in Web (C1 "/\" C2) iff [x,y] in Web C1 )

proof end;

theorem :: COHSP_1:91

for C1, C2 being Coherence_Space
for x, y being set holds
( [[x,2],[y,2]] in Web (C1 "/\" C2) iff [x,y] in Web C2 )

proof end;

theorem :: COHSP_1:92

for C1, C2 being Coherence_Space
for x, y being set st x in union C1 & y in union C2 holds
( [[x,1],[y,2]] in Web (C1 "/\" C2) & [[y,2],[x,1]] in Web (C1 "/\" C2) )

proof end;

theorem :: COHSP_1:93

for C1, C2 being Coherence_Space
for x, y being set holds
( [[x,1],[y,1]] in Web (C1 "\/" C2) iff [x,y] in Web C1 )

proof end;

theorem :: COHSP_1:94

for C1, C2 being Coherence_Space
for x, y being set holds
( [[x,2],[y,2]] in Web (C1 "\/" C2) iff [x,y] in Web C2 )

proof end;

theorem :: COHSP_1:95

for C1, C2 being Coherence_Space
for x, y being set holds
( not [[x,1],[y,2]] in Web (C1 "\/" C2) & not [[y,2],[x,1]] in Web (C1 "\/" C2) )

proof end;

theorem :: COHSP_1:96

for C1, C2 being Coherence_Space holds 'not' (C1 "/\" C2) = ('not' C1) "\/" ('not' C2)

proof end;

definition

let C1, C2 be Coherence_Space;
func C1 [*] C2 -> set equals :: COHSP_1:def 26
union { (bool [:a,b:]) where a is Element of C1, b is Element of C2 : verum } ;
correctness ;

end;

:: deftheorem defines [*] COHSP_1:def 26 :

theorem Th97: :: COHSP_1:97

for C1, C2 being Coherence_Space
for x being set holds
( x in C1 [*] C2 iff ex a being Element of C1 ex b being Element of C2 st x c= [:a,b:] )

proof end;

registration

let C1, C2 be Coherence_Space;
cluster C1 [*] C2 -> non empty ;
coherence

proof end;

end;

theorem Th98: :: COHSP_1:98

for C1, C2 being Coherence_Space
for a being Element of C1 [*] C2 holds
( proj1 a in C1 & proj2 a in C2 & a c= [:(proj1 a),(proj2 a):] )

proof end;

registration

let C1, C2 be Coherence_Space;
cluster C1 [*] C2 -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem :: COHSP_1:99

for C1, C2 being Coherence_Space holds union (C1 [*] C2) = [:(union C1),(union C2):]

proof end;

theorem :: COHSP_1:100

for C1, C2 being Coherence_Space
for x1, y1, x2, y2 being set holds
( [[x1,x2],[y1,y2]] in Web (C1 [*] C2) iff ( [x1,y1] in Web C1 & [x2,y2] in Web C2 ) )

proof end;