Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

Continuous, Stable, and Linear Maps of Coherence Spaces

by
Grzegorz Bancerek

MML identifier: COHSP_1
[ Mizar article, MML identifier index ]

environ

vocabulary FUNCT_1, TARSKI, FINSET_1, COH_SP, BOOLE, RELAT_1, CLASSES1,
TOLER_1, FINSUB_1, CARD_1, ARYTM_1, FUNCOP_1, PBOOLE, MCART_1, PROB_1,
ZF_LANG, CARD_3, FINSEQ_1, FUNCT_5, LATTICES, MONOID_0, COHSP_1;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, REAL_1, NAT_1,
MCART_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, FINSUB_1, TOLER_1,
CLASSES1, COH_SP, PBOOLE, CARD_1, FUNCT_5, PROB_1, CARD_3, PARTFUN1,
FUNCT_2, BORSUK_1;
constructors ENUMSET1, REAL_1, NAT_1, FINSUB_1, COH_SP, BORSUK_1, INDEX_1,
PROB_1, MEMBERED;
clusters SUBSET_1, RELSET_1, FINSET_1, FINSUB_1, FINSEQ_1, NAT_1, PARTFUN1;
requirements NUMERALS, BOOLE, SUBSET;

begin

definition
cluster finite Coherence_Space;
let X be set;
redefine attr X is binary_complete means
:: 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;
end;

definition
let X be set;
func FlatCoh X -> set equals
:: COHSP_1:def 2

CohSp id X;
func Sub_of_Fin X -> Subset of X means
:: COHSP_1:def 3

for x being set holds x in it iff x in X & x is finite;
end;

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

theorem :: COHSP_1:2
for X being set holds union FlatCoh X = X;

theorem :: COHSP_1:3
for X being finite subset-closed set holds Sub_of_Fin X = X;

definition
cluster {{}} -> subset-closed binary_complete;
let X be set;
cluster bool X -> subset-closed binary_complete;
cluster FlatCoh X -> non empty subset-closed binary_complete;
end;

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

theorem :: COHSP_1:4
Web {{}} = {};

scheme MinimalElement_wrt_Incl { a, A() -> set, P[set] }:
ex a being set st a in A() & P[a] &
for b being set st b in A() & P[b] & b c= a holds b = a
provided
a() in A()
and
P[a()]
and
a() is finite;

definition let C be Coherence_Space;
cluster finite Element of C;
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;

definition
cluster c=directed -> non empty set;
cluster c=filtered -> non empty set;
end;

theorem :: COHSP_1:5
for X being set st X is c=directed
for a,b being set st a in X & b in X ex c being set st a \/ b c= c & c in X;

theorem :: COHSP_1:6
for X being non empty set st
for a,b being set st a in X & b in X ex c being set st a \/ b c= c & c in X
holds X is c=directed;

theorem :: COHSP_1:7
for X being set st X is c=filtered
for a,b being set st a in X & b in X ex c being set st c c= a /\ b & c in X;

theorem :: COHSP_1:8
for X being non empty set st
for a,b being set st a in X & b in X ex c being set st c c= a /\ b & c in X
holds X is c=filtered;

theorem :: COHSP_1:9
for x being set holds {x} is c=directed c=filtered;

theorem :: COHSP_1:10
for x,y being set holds {x,y,x \/ y} is c=directed;

theorem :: COHSP_1:11
for x,y being set holds {x,y,x /\ y} is c=filtered;

definition
cluster c=directed c=filtered finite set;
end;

definition let C be non empty set;
cluster c=directed c=filtered finite Subset of C;
end;

theorem :: COHSP_1:12
for X being set holds Fin X is c=directed c=filtered;

definition let X be set;
cluster Fin X -> c=directed c=filtered;
end;

definition
let C be subset-closed non empty set;
cluster preBoolean non empty Subset of C;
end;

definition
let C be subset-closed non empty set;
let a be Element of C;
redefine func Fin a -> preBoolean non empty Subset of C;
end;

theorem :: COHSP_1:13
for X being non empty set, Y being set st
X is c=directed & Y c= union X & Y is finite
ex Z being set st Z in X & Y c= Z;

definition let X be set;
redefine attr X is cap-closed;
synonym X is multiplicative;
end;

definition let X be set;
canceled;

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

definition
cluster subset-closed -> multiplicative set;
end;

canceled;

theorem :: COHSP_1:15
for C being Coherence_Space, A being c=directed Subset of C holds union A in C
;

definition
cluster -> d.union-closed Coherence_Space;
end;

definition
cluster multiplicative d.union-closed Coherence_Space;
end;

definition
let C be d.union-closed non empty set, A be c=directed Subset of C;
redefine func union A -> Element of C;
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;

theorem :: COHSP_1:16
for X being non empty set st X includes_lattice_of X holds
X is c=directed c=filtered;

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;

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

begin :: Continuous, Stable, and Linear Functions

definition let f be Function;
attr f is union-distributive means
:: 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
:: 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;

definition let f be Function;
attr f is c=-monotone means
:: 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
:: 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;

definition
cluster d.union-distributive -> c=-monotone Function;
cluster union-distributive -> d.union-distributive Function;
end;

theorem :: COHSP_1:18
for f being Function st f is union-distributive
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);

theorem :: COHSP_1:19
for f being Function st f is union-distributive holds f.{} = {};

definition let C1,C2 be Coherence_Space;
cluster union-distributive cap-distributive Function of C1, C2;
end;

definition let C be Coherence_Space;
cluster union-distributive cap-distributive ManySortedSet of C;
end;

::definition
:: cluster union-distributive cap-distributive Function;
::end;

definition let f be Function;
attr f is U-continuous means
:: COHSP_1:def 14

dom f is d.union-closed & f is d.union-distributive;
end;

definition let f be Function;
attr f is U-stable means
:: COHSP_1:def 15

dom f is multiplicative & f is U-continuous cap-distributive;
end;

definition let f be Function;
attr f is U-linear means
:: COHSP_1:def 16

f is U-stable union-distributive;
end;

definition
cluster U-continuous -> d.union-distributive Function;
cluster U-stable -> cap-distributive U-continuous Function;
cluster U-linear -> union-distributive U-stable Function;
end;

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

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

definition
cluster U-stable union-distributive -> U-linear Function;
end;

definition
cluster U-linear Function;
let C be Coherence_Space;
cluster U-linear ManySortedSet of C;
let B be Coherence_Space;
cluster U-linear Function of B,C;
end;

definition let f be U-continuous Function;
cluster dom f -> d.union-closed;
end;

definition let f be U-stable Function;
cluster dom f -> multiplicative;
end;

theorem :: COHSP_1:20
for X being set holds union Fin X = X;

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

theorem :: 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
ex b being set st b is finite & b c= a & y in f.b;

theorem :: COHSP_1:23
for f being Function st dom f is subset-closed 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
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;

theorem :: COHSP_1:24
for f being Function st dom f is subset-closed 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
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;

begin :: Graph of Continuous Function

definition let f be Function;
func graph f -> set means
:: COHSP_1:def 17

for x being set holds x in it iff
ex y being finite set, z being set st x = [y,z] & y in dom f & z in f.y;
end;

definition
let C1,C2 be non empty set;
let f be Function of C1,C2;
redefine func graph f -> Subset of [:C1, union C2:];
end;

definition let f be Function;
cluster graph f -> Relation-like;
end;

theorem :: COHSP_1:25
for f being Function, x,y being set holds
[x,y] in graph f iff x is finite & x in dom f & y in f.x;

theorem :: 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
for y being set st [a,y] in graph f holds [b,y] in graph f;

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

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
for y1,y2 being set st [a,y1] in graph f & [b,y2] in graph f holds {y1,y2} in
C2;

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

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
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)
ex f being U-continuous Function of C1,C2 st X = graph f;

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;

begin :: Trace of Stable Function

definition let f be Function;
func Trace f -> set means
:: 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;
end;

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

definition
let C1, C2 be non empty set;
let f be Function of C1, C2;
redefine func Trace f -> Subset of [:C1, union C2:];
end;

definition let f be Function;
cluster Trace f -> Relation-like;
end;

theorem :: COHSP_1:33
for f being U-continuous Function st dom f is subset-closed holds
Trace f c= graph f;

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

theorem :: 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
for y1,y2 being set st [a1,y1] in Trace f & [a2,y2] in Trace f
holds {y1,y2} in C2;

theorem :: 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
for y being set st [a1,y] in Trace f & [a2,y] in Trace f holds a1 = a2;

theorem :: 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
for a being Element of C1 holds f.a c= g.a;

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

theorem :: 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
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
for y being set st [a,y] in X & [b,y] in X holds a = b)
ex f being U-stable Function of C1,C2 st X = Trace f;

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;

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

theorem :: COHSP_1:42
for C1, C2 being Coherence_Space
ex f being U-stable Function of C1, C2 st Trace f = {};

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

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

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

theorem :: 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
ex f being U-stable Function of C1,C2 st x \/ y = Trace f
ex f being U-stable Function of C1,C2 st union A = Trace f;

definition let C1, C2 be Coherence_Space;
func StabCoh(C1,C2) -> set means
:: 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;
end;

definition let C1, C2 be Coherence_Space;
cluster StabCoh(C1,C2) -> non empty subset-closed binary_complete;
end;

theorem :: COHSP_1:47
for C1,C2 being Coherence_Space, f being U-stable Function of C1,C2 holds
Trace f c= [:Sub_of_Fin C1, union C2:];

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

theorem :: COHSP_1:49
for C1,C2 being Coherence_Space
for a,b being finite Element of C1, 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);

begin :: Trace of Linear Functions

theorem :: 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 ex x being set st a = {x};

definition let f be Function;
func LinTrace f -> set means
:: 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;
end;

theorem :: COHSP_1:51
for f being Function, x,y being set holds
[x,y] in LinTrace f iff [{x},y] in Trace f;

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

theorem :: COHSP_1:53
for f being Function, x,y being set st [x,y] in LinTrace f
holds {x} in dom f & y in f.{x};

definition
let C1, C2 be non empty set;
let f be Function of C1, C2;
redefine func LinTrace f -> Subset of [:union C1, union C2:];
end;

definition let f be Function;
cluster LinTrace f -> Relation-like;
end;

definition let C1, C2 be Coherence_Space;
func LinCoh(C1,C2) -> set means
:: 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;
end;

theorem :: 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
for y1,y2 being set st [x1,y1] in LinTrace f & [x2,y2] in LinTrace f
holds {y1,y2} in C2;

theorem :: 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
for y being set st [x1,y] in LinTrace f & [x2,y] in LinTrace f holds x1 = x2;

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

theorem :: 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
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
for y being set st [a,y] in X & [b,y] in X holds a = b)
ex f being U-linear Function of C1,C2 st X = LinTrace f;

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;

theorem :: COHSP_1:59
for C1, C2 being Coherence_Space
ex f being U-linear Function of C1, C2 st LinTrace f = {};

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

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

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

theorem :: 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
ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f
ex f being U-linear Function of C1,C2 st union A = LinTrace f;

definition let C1, C2 be Coherence_Space;
cluster LinCoh(C1,C2) -> non empty subset-closed binary_complete;
end;

theorem :: COHSP_1:64
for C1,C2 being Coherence_Space holds
union LinCoh(C1,C2) = [:union C1, union C2:];

theorem :: COHSP_1:65
for C1,C2 being Coherence_Space
for x1,x2 being set, 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));

begin :: Negation of Coherence Spaces

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

theorem :: COHSP_1:66
for C being Coherence_Space, 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};

definition
let C be Coherence_Space;
cluster 'not' C -> non empty subset-closed binary_complete;
end;

theorem :: COHSP_1:67
for C being Coherence_Space holds union 'not' C = union C;

theorem :: COHSP_1:68
for C being Coherence_Space, x,y being set st x <> y & {x,y} in C
holds not {x,y} in 'not' C;

theorem :: COHSP_1:69
for C being Coherence_Space, x,y being set
st {x,y} c= union C & not {x,y} in C holds {x,y} in 'not' C;

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

theorem :: COHSP_1:71
for C being Coherence_Space holds 'not' 'not' C = C;

theorem :: COHSP_1:72
'not' {{}} = {{}};

theorem :: COHSP_1:73
for X being set holds 'not' FlatCoh X = bool X & 'not' bool X = FlatCoh X;

begin :: Product and Coproduct on Coherence Spaces

definition
let x,y be set;
func x U+ y -> set equals
:: COHSP_1:def 23

Union disjoin <*x,y*>;
end;

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

theorem :: COHSP_1:75
for x being set holds
x U+ {} = [:x,{1}:] & {} U+ x = [:x,{2}:];

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

theorem :: COHSP_1:77
for x,y,z being set holds [z,1] in x U+ y iff z in x;

theorem :: COHSP_1:78
for x,y,z being set holds [z,2] in x U+ y iff z in y;

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

theorem :: COHSP_1:80
for x,y, z being set st z c= x U+ y
ex x1,y1 being set st z = x1 U+ y1 & x1 c= x & y1 c= y;

theorem :: COHSP_1:81
for x1,y1, x2,y2 being set holds
x1 U+ y1 = x2 U+ y2 iff x1 = x2 & y1 = y2;

theorem :: COHSP_1:82
for x1,y1, x2,y2 being set holds
x1 U+ y1 \/ x2 U+ y2 = (x1 \/ x2) U+ (y1 \/ y2);

theorem :: COHSP_1:83
for x1,y1, x2,y2 being set holds
(x1 U+ y1) /\ (x2 U+ y2) = (x1 /\ x2) U+ (y1 /\ y2);

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: not contradiction};
func C1 "\/" C2 -> set equals
:: COHSP_1:def 25
{a U+ {} where a is Element of C1: not contradiction} \/
{{} U+ b where b is Element of C2: not contradiction};
end;

theorem :: 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, b being Element of C2 st x = a U+ b;

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

theorem :: COHSP_1:86
for C1,C2 being Coherence_Space holds
union (C1 "/\" C2) = (union C1) U+ (union C2);

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

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

theorem :: COHSP_1:89
for C1,C2 being Coherence_Space holds
union (C1 "\/" C2) = (union C1) U+ (union C2);

definition
let C1, C2 be Coherence_Space;
cluster C1 "/\" C2 -> non empty subset-closed binary_complete;
cluster C1 "\/" C2 -> non empty subset-closed binary_complete;
end;

reserve C1, C2 for Coherence_Space;

theorem :: COHSP_1:90
for x,y being set holds
[[x,1],[y,1]] in Web (C1 "/\" C2) iff [x,y] in Web C1;

theorem :: COHSP_1:91
for x,y being set holds
[[x,2],[y,2]] in Web (C1 "/\" C2) iff [x,y] in Web C2;

theorem :: COHSP_1:92
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);

theorem :: COHSP_1:93
for x,y being set holds
[[x,1],[y,1]] in Web (C1 "\/" C2) iff [x,y] in Web C1;

theorem :: COHSP_1:94
for x,y being set holds
[[x,2],[y,2]] in Web (C1 "\/" C2) iff [x,y] in Web C2;

theorem :: COHSP_1:95
for x,y being set holds
not [[x,1],[y,2]] in Web (C1 "\/" C2) & not [[y,2],[x,1]] in Web (C1 "\/" C2)
;

theorem :: COHSP_1:96
'not' (C1 "/\" C2) = 'not' C1 "\/" 'not' C2;

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

theorem :: COHSP_1:97
for C1,C2 being Coherence_Space, x being set holds
x in C1 [*] C2 iff
ex a being Element of C1, b being Element of C2 st x c= [:a,b:];

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

theorem :: COHSP_1:98
for C1,C2 being Coherence_Space, a being Element of C1 [*] C2 holds
proj1 a in C1 & proj2 a in C2 & a c= [:proj1 a, proj2 a:];

definition let C1,C2 be Coherence_Space;
cluster C1 [*] C2 -> subset-closed binary_complete;
end;

theorem :: COHSP_1:99
for C1,C2 being Coherence_Space holds
union (C1 [*] C2) = [:union C1, union C2:];

theorem :: COHSP_1:100
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;