:: Continuous, Stable, and Linear Maps of Coherence Spaces
:: by Grzegorz Bancerek
::
:: Received August 30, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

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
 ( X is binary_complete iff 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 )
proofend;
end;

:: deftheorem Def1 defines binary_complete COHSP_1:def_1_:_
 for X being set holds
( X is binary_complete iff 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 );

registration
cluster non empty finite subset-closed binary_complete for set ;
existence
 ex b1 being Coherence_Space st b1 is finite by COH_SP:3;
end;

definition
let X be set ;
func FlatCoh X ->  set  equals :: COHSP_1:def 2
 CohSp (id X);
correctness
coherence
CohSp (id X) is set ;
;
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
 ex b1 being Subset of X st
for x being set holds
( x in b1 iff ( x in X & x is finite ) )
proofend;
correctness
uniqueness
for b1, b2 being Subset of X st ( for x being set holds
( x in b1 iff ( x in X & x is finite ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & x is finite ) ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem  defines FlatCoh COHSP_1:def_2_:_
 for X being set holds FlatCoh X = CohSp (id X);

:: deftheorem Def3 defines Sub_of_Fin COHSP_1:def_3_:_
 for X being set
for b2 being Subset of X holds
( b2 = Sub_of_Fin X iff for x being set holds
( x in b2 iff ( x in X & x is finite ) ) );

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

theorem Th2: :: COHSP_1:2
for X being set holds union (FlatCoh X) = X
proofend;

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

registration
cluster{{}} ->  subset-closed binary_complete ;
coherence
 ( {{}} is subset-closed & {{}} is binary_complete ) by COH_SP:3;
let X be set ;
cluster bool X ->  subset-closed binary_complete ;
coherence
 ( bool X is subset-closed & bool X is binary_complete ) by COH_SP:2;
cluster FlatCoh X ->  non empty subset-closed binary_complete ;
coherence
 ( not FlatCoh X is empty & FlatCoh X is subset-closed & FlatCoh X is binary_complete ) ;
end;

registration
let C be non empty subset-closed set ;
cluster Sub_of_Fin C ->  non empty subset-closed ;
coherence
 ( not Sub_of_Fin C is empty & Sub_of_Fin C is subset-closed )
proofend;
end;

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

scheme :: COHSP_1:sch 1
MinimalElementwrtIncl{ F1() ->  set , F2() ->  set , P1[ set ] } :
 ex a being set st
( a in F2() & P1[a] & ( for b being set st b in F2() & P1[b] & b c= a holds
b = a ) )
provided
A1: ( F1() in F2() & P1[F1()] ) and
A2: F1() is finite
proofend;

registration
let C be Coherence_Space;
cluster finite for Element of C;
existence
 ex b1 being Element of C st b1 is finite
proofend;
end;

definition
let X be set ;
attrX 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 );
attrX 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_:_
 for X being set holds
( X is c=directed iff for Y being finite Subset of X ex a being set st
( union Y c= a & a in X ) );

:: deftheorem  defines c=filtered COHSP_1:def_5_:_
 for X being set holds
( X is c=filtered iff 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 ) );

registration
cluster c=directed  ->  non empty for set ;
coherence
 for b1 being set st b1 is c=directed holds
not b1 is empty
proofend;
cluster c=filtered  ->  non empty for set ;
coherence
 for b1 being set st b1 is c=filtered holds
not b1 is empty
proofend;
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 )
proofend;

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

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

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

theorem Th9: :: COHSP_1:9
for x being set holds
( {x} is c=directed & {x} is c=filtered )
proofend;

Lm2: now__::_thesis:_for_x,_y_being_set_holds_union_{x,y,(x_\/_y)}_=_x_\/_y
let x, y be set ; ::_thesis: union {x,y,(x \/ y)} = x \/ y
thus  union {x,y,(x \/ y)} = union ({x,y} \/ {(x \/ y)}) by ENUMSET1:3
.= (union {x,y}) \/ (union {(x \/ y)}) by ZFMISC_1:78
.= (x \/ y) \/ (union {(x \/ y)}) by ZFMISC_1:75
.= (x \/ y) \/ (x \/ y) by ZFMISC_1:25
.= x \/ y ; ::_thesis: verum
end;

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

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

registration
cluster finite c=directed c=filtered for set ;
existence
 ex b1 being set st
( b1 is c=directed & b1 is c=filtered & b1 is finite )
proofend;
end;

registration
let C be non empty set ;
cluster finite c=directed c=filtered for Element of bool C;
existence
 ex b1 being Subset of C st
( b1 is c=directed & b1 is c=filtered & b1 is finite )
proofend;
end;

theorem Th12: :: COHSP_1:12
for X being set holds
( Fin X is c=directed & Fin X is c=filtered )
proofend;

registration
let X be set ;
cluster Fin X ->  c=directed c=filtered ;
coherence
 ( Fin X is c=directed & Fin X is c=filtered ) by Th12;
end;

Lm3: now__::_thesis:_for_C_being_non_empty_subset-closed_set_
for_a_being_Element_of_C_holds_Fin_a_c=_C
let C be non empty subset-closed set ; ::_thesis: for a being Element of C holds Fin a c= C
let a be Element of C; ::_thesis: Fin a c= C
thus  Fin a c= C ::_thesis: verum
proof
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in Fin a or x in C )
assume  x in Fin a ; ::_thesis: x in C
then  x c= a by FINSUB_1:def_5;
hence  x in C by CLASSES1:def_1; ::_thesis: verum
end;
end;

registration
let C be non empty subset-closed set ;
cluster non empty preBoolean for Element of bool C;
existence
 ex b1 being Subset of C st
( b1 is preBoolean & not b1 is empty )
proofend;
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
 Fin a is non empty preBoolean Subset of C
proofend;
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 )
proofend;

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

definition
let X be set ;
attrX is d.union-closed  means :Def6: :: COHSP_1:def 6
 for A being Subset of X st A is c=directed holds
union A in X;
end;

:: deftheorem Def6 defines d.union-closed COHSP_1:def_6_:_
 for X being set holds
( X is d.union-closed iff for A being Subset of X st A is c=directed holds
union A in X );

registration
cluster subset-closed  ->  multiplicative for set ;
coherence
 for b1 being set st b1 is subset-closed holds
b1 is multiplicative
proofend;
end;

theorem Th14: :: COHSP_1:14
for C being Coherence_Space
for A being c=directed Subset of C holds union A in C
proofend;

registration
cluster non empty subset-closed binary_complete  ->  d.union-closed for set ;
coherence
 for b1 being Coherence_Space holds b1 is d.union-closed
proofend;
end;

registration
cluster non empty multiplicative subset-closed binary_complete d.union-closed for set ;
existence
 ex b1 being Coherence_Space st
( b1 is multiplicative & b1 is d.union-closed )
proofend;
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
 union A is Element of C by Def6;
end;

definition
let X, Y be set ;
predX includes_lattice_of Y means :: COHSP_1:def 7
 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_7_:_
 for X, Y being set holds
( X includes_lattice_of Y iff for a, b being set st a in Y & b in Y holds
( a /\ b in X & a \/ b in X ) );

theorem :: COHSP_1:15
for X being non empty set st X includes_lattice_of X holds
( X is c=directed & X is c=filtered )
proofend;

definition
let X, x, y be set ;
predX includes_lattice_of x,y means :: COHSP_1:def 8
X includes_lattice_of {x,y};
end;

:: deftheorem  defines includes_lattice_of COHSP_1:def_8_:_
 for X, x, y being set holds
( X includes_lattice_of x,y iff X includes_lattice_of {x,y} );

theorem Th16: :: COHSP_1:16
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 ) )
proofend;

begin

definition
let f be Function;
attrf is union-distributive  means :Def9: :: COHSP_1:def 9
 for A being Subset of (dom f) st union A in dom f holds
f . (union A) = union (f .: A);
attrf is d.union-distributive  means :Def10: :: COHSP_1:def 10
 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 Def9 defines union-distributive COHSP_1:def_9_:_
 for f being Function holds
( f is union-distributive iff for A being Subset of (dom f) st union A in dom f holds
f . (union A) = union (f .: A) );

:: deftheorem Def10 defines d.union-distributive COHSP_1:def_10_:_
 for f being Function holds
( f is d.union-distributive iff for A being Subset of (dom f) st A is c=directed & union A in dom f holds
f . (union A) = union (f .: A) );

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

:: deftheorem Def11 defines c=-monotone COHSP_1:def_11_:_
 for f being Function holds
( f is c=-monotone iff for a, b being set st a in dom f & b in dom f & a c= b holds
f . a c= f . b );

:: deftheorem Def12 defines cap-distributive COHSP_1:def_12_:_
 for f being Function holds
( f is cap-distributive iff for a, b being set st dom f includes_lattice_of a,b holds
f . (a /\ b) = (f . a) /\ (f . b) );

registration
cluster Relation-like Function-like d.union-distributive  ->  c=-monotone for set ;
coherence
 for b1 being Function st b1 is d.union-distributive holds
b1 is c=-monotone
proofend;
cluster Relation-like Function-like union-distributive  ->  d.union-distributive for set ;
coherence
 for b1 being Function st b1 is union-distributive holds
b1 is d.union-distributive
proofend;
end;

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

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

registration
let C1, C2 be Coherence_Space;
cluster Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) union-distributive cap-distributive for Element of bool [:C1,C2:];
existence
 ex b1 being Function of C1,C2 st
( b1 is union-distributive & b1 is cap-distributive )
proofend;
end;

registration
let C be Coherence_Space;
cluster Relation-like C -defined Function-like V30(C) union-distributive cap-distributive for set ;
existence
 ex b1 being ManySortedSet of C st
( b1 is union-distributive & b1 is cap-distributive )
proofend;
end;

::definition
:: cluster union-distributive cap-distributive Function;
::end;
definition
let f be Function;
attrf is U-continuous  means :Def13: :: COHSP_1:def 13
( dom f is d.union-closed & f is d.union-distributive );
end;

:: deftheorem Def13 defines U-continuous COHSP_1:def_13_:_
 for f being Function holds
( f is U-continuous iff ( dom f is d.union-closed & f is d.union-distributive ) );

definition
let f be Function;
attrf is U-stable  means :Def14: :: COHSP_1:def 14
( dom f is multiplicative & f is U-continuous & f is cap-distributive );
end;

:: deftheorem Def14 defines U-stable COHSP_1:def_14_:_
 for f being Function holds
( f is U-stable iff ( dom f is multiplicative & f is U-continuous & f is cap-distributive ) );

definition
let f be Function;
attrf is U-linear  means :Def15: :: COHSP_1:def 15
( f is U-stable & f is union-distributive );
end;

:: deftheorem Def15 defines U-linear COHSP_1:def_15_:_
 for f being Function holds
( f is U-linear iff ( f is U-stable & f is union-distributive ) );

registration
cluster Relation-like Function-like U-continuous  ->  d.union-distributive for set ;
coherence
 for b1 being Function st b1 is U-continuous holds
b1 is d.union-distributive by Def13;
cluster Relation-like Function-like U-stable  ->  cap-distributive U-continuous for set ;
coherence
 for b1 being Function st b1 is U-stable holds
( b1 is cap-distributive & b1 is U-continuous ) by Def14;
cluster Relation-like Function-like U-linear  ->  union-distributive U-stable for set ;
coherence
 for b1 being Function st b1 is U-linear holds
( b1 is union-distributive & b1 is U-stable ) by Def15;
end;

registration
let X be d.union-closed set ;
cluster Relation-like X -defined Function-like V30(X) d.union-distributive  ->  U-continuous for set ;
coherence
 for b1 being ManySortedSet of X st b1 is d.union-distributive holds
b1 is U-continuous
proofend;
end;

registration
let X be multiplicative set ;
cluster Relation-like X -defined Function-like V30(X) cap-distributive U-continuous  ->  U-stable for set ;
coherence
 for b1 being ManySortedSet of X st b1 is U-continuous & b1 is cap-distributive holds
b1 is U-stable
proofend;
end;

registration
cluster Relation-like Function-like union-distributive U-stable  ->  U-linear for set ;
coherence
 for b1 being Function st b1 is U-stable & b1 is union-distributive holds
b1 is U-linear by Def15;
end;

registration
cluster Relation-like Function-like U-linear for set ;
existence
 ex b1 being Function st b1 is U-linear
proofend;
let C be Coherence_Space;
cluster Relation-like C -defined Function-like V30(C) U-linear for set ;
existence
 ex b1 being ManySortedSet of C st b1 is U-linear
proofend;
let B be Coherence_Space;
cluster Relation-like B -defined C -valued Function-like V34(B,C) U-linear for Element of bool [:B,C:];
existence
 ex b1 being Function of B,C st b1 is U-linear
proofend;
end;

registration
let f be U-continuous Function;
cluster proj1 f ->  d.union-closed ;
coherence
 dom f is d.union-closed by Def13;
end;

registration
let f be U-stable Function;
cluster proj1 f ->  multiplicative ;
coherence
 dom f is multiplicative by Def14;
end;

theorem Th19: :: COHSP_1:19
for X being set holds union (Fin X) = X
proofend;

theorem Th20: :: COHSP_1:20
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))
proofend;

theorem Th21: :: COHSP_1:21
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 ) ) ) )
proofend;

theorem Th22: :: COHSP_1:22
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 ) ) ) ) )
proofend;

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

begin

definition
let f be Function;
func graph f ->  set  means :Def16: :: COHSP_1:def 16
 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
 ex b1 being set st
for x being set holds
( x in b1 iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) ) & ( for x being set holds
( x in b2 iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines graph COHSP_1:def_16_:_
 for f being Function
for b2 being set holds
( b2 = graph f iff for x being set holds
( x in b2 iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) );

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
 graph f is Subset of [:C1,(union C2):]
proofend;
end;

registration
let f be Function;
cluster graph f ->  Relation-like ;
coherence
 graph f is Relation-like
proofend;
end;

theorem Th24: :: COHSP_1:24
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 ) )
proofend;

theorem Th25: :: COHSP_1:25
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
proofend;

theorem Th26: :: COHSP_1:26
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
proofend;

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

theorem Th28: :: COHSP_1:28
for C1, C2 being Coherence_Space
for f, g being U-continuous Function of C1,C2 st graph f = graph g holds
f = g
proofend;

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

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

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

begin

definition
let f be Function;
func Trace f ->  set  means :Def17: :: COHSP_1:def 17
 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
 ex b1 being set st
for x being set holds
( x in b1 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 ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 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 ) ) ) ) & ( for x being set holds
( x in b2 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 ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines Trace COHSP_1:def_17_:_
 for f being Function
for b2 being set holds
( b2 = Trace f iff for x being set holds
( x in b2 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 ) ) ) );

theorem Th31: :: COHSP_1:31
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 ) ) )
proofend;

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
 Trace f is Subset of [:C1,(union C2):]
proofend;
end;

registration
let f be Function;
cluster Trace f ->  Relation-like ;
coherence
 Trace f is Relation-like
proofend;
end;

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

theorem Th33: :: COHSP_1:33
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
proofend;

theorem Th34: :: COHSP_1:34
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
proofend;

theorem Th35: :: COHSP_1:35
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
proofend;

theorem Th36: :: COHSP_1:36
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
proofend;

theorem Th37: :: COHSP_1:37
for C1, C2 being Coherence_Space
for f, g being U-stable Function of C1,C2 st Trace f = Trace g holds
f = g
proofend;

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

theorem Th38: :: COHSP_1:38
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
proofend;

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

theorem Th40: :: COHSP_1:40
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 ) )
proofend;

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

theorem Th42: :: COHSP_1:42
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]}
proofend;

theorem :: COHSP_1:43
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 = {} ) )
proofend;

theorem Th44: :: COHSP_1:44
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
proofend;

theorem Th45: :: COHSP_1:45
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
proofend;

definition
let C1, C2 be Coherence_Space;
func StabCoh (C1,C2) ->  set  means :Def18: :: COHSP_1:def 18
 for x being set holds
( x in it iff ex f being U-stable Function of C1,C2 st x = Trace f );
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being U-stable Function of C1,C2 st x = Trace f ) ) & ( for x being set holds
( x in b2 iff ex f being U-stable Function of C1,C2 st x = Trace f ) ) holds
b1 = b2
proofend;
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f being U-stable Function of C1,C2 st x = Trace f )
proofend;
end;

:: deftheorem Def18 defines StabCoh COHSP_1:def_18_:_
 for C1, C2 being Coherence_Space
for b3 being set holds
( b3 = StabCoh (C1,C2) iff for x being set holds
( x in b3 iff ex f being U-stable Function of C1,C2 st x = Trace f ) );

registration
let C1, C2 be Coherence_Space;
cluster StabCoh (C1,C2) ->  non empty subset-closed binary_complete ;
coherence
 ( not StabCoh (C1,C2) is empty & StabCoh (C1,C2) is subset-closed & StabCoh (C1,C2) is binary_complete )
proofend;
end;

theorem Th46: :: COHSP_1:46
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):]
proofend;

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

theorem Th48: :: COHSP_1:48
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 ) ) ) )
proofend;

begin

theorem Th49: :: COHSP_1:49
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} )
proofend;

definition
let f be Function;
func LinTrace f ->  set  means :Def19: :: COHSP_1:def 19
 for x being set holds
( x in it iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) );
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) ) ) & ( for x being set holds
( x in b2 iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) ) ) holds
b1 = b2
proofend;
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) )
proofend;
end;

:: deftheorem Def19 defines LinTrace COHSP_1:def_19_:_
 for f being Function
for b2 being set holds
( b2 = LinTrace f iff for x being set holds
( x in b2 iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) ) );

theorem Th50: :: COHSP_1:50
for f being Function
for x, y being set holds
( [x,y] in LinTrace f iff [{x},y] in Trace f )
proofend;

theorem Th51: :: COHSP_1:51
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
proofend;

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

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
 LinTrace f is Subset of [:(union C1),(union C2):]
proofend;
end;

registration
let f be Function;
cluster LinTrace f ->  Relation-like ;
coherence
 LinTrace f is Relation-like
proofend;
end;

definition
let C1, C2 be Coherence_Space;
func LinCoh (C1,C2) ->  set  means :Def20: :: COHSP_1:def 20
 for x being set holds
( x in it iff ex f being U-linear Function of C1,C2 st x = LinTrace f );
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being U-linear Function of C1,C2 st x = LinTrace f ) ) & ( for x being set holds
( x in b2 iff ex f being U-linear Function of C1,C2 st x = LinTrace f ) ) holds
b1 = b2
proofend;
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f being U-linear Function of C1,C2 st x = LinTrace f )
proofend;
end;

:: deftheorem Def20 defines LinCoh COHSP_1:def_20_:_
 for C1, C2 being Coherence_Space
for b3 being set holds
( b3 = LinCoh (C1,C2) iff for x being set holds
( x in b3 iff ex f being U-linear Function of C1,C2 st x = LinTrace f ) );

theorem Th53: :: COHSP_1:53
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
proofend;

theorem Th54: :: COHSP_1:54
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
proofend;

theorem Th55: :: COHSP_1:55
for C1, C2 being Coherence_Space
for f, g being U-linear Function of C1,C2 st LinTrace f = LinTrace g holds
f = g
proofend;

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

theorem Th56: :: COHSP_1:56
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
proofend;

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

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

theorem Th59: :: COHSP_1:59
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]}
proofend;

theorem :: COHSP_1:60
for C1, C2 being Coherence_Space
for x, y being set st x in union C1 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 = {} ) )
proofend;

theorem Th61: :: COHSP_1:61
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
proofend;

theorem Th62: :: COHSP_1:62
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
proofend;

registration
let C1, C2 be Coherence_Space;
cluster LinCoh (C1,C2) ->  non empty subset-closed binary_complete ;
coherence
 ( not LinCoh (C1,C2) is empty & LinCoh (C1,C2) is subset-closed & LinCoh (C1,C2) is binary_complete )
proofend;
end;

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

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

begin

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

:: deftheorem  defines 'not' COHSP_1:def_21_:_
 for C being Coherence_Space holds 'not' C =  {  a where a is Subset of (union C) : for b being Element of C ex x being set st a /\ b c= {x}  }  ;

theorem Th65: :: COHSP_1:65
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} ) ) )
proofend;

registration
let C be Coherence_Space;
cluster 'not' C ->  non empty subset-closed binary_complete ;
coherence
 ( not 'not' C is empty & 'not' C is subset-closed & 'not' C is binary_complete )
proofend;
end;

theorem Th66: :: COHSP_1:66
for C being Coherence_Space holds union ('not' C) = union C
proofend;

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

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

theorem :: COHSP_1:69
for C being Coherence_Space
for x, y being set holds
( [x,y] in Web ('not' C) iff ( x in union C &amp; y in union C &amp; ( x = y or not [x,y] in Web C ) ) )
proofend;

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

theorem Th70: :: COHSP_1:70
for C being Coherence_Space holds 'not' ('not' C) = C
proofend;

theorem :: COHSP_1:71
'not' {{}} = {{}}
proofend;

theorem :: COHSP_1:72
for X being set holds
( 'not' (FlatCoh X) = bool X &amp; 'not' (bool X) = FlatCoh X )
proofend;

begin

definition
let x, y be set ;
funcx U+ y ->  set  equals :: COHSP_1:def 22
 Union (disjoin <*x,y*>);
correctness
coherence
Union (disjoin <*x,y*>) is set ;
;
end;

:: deftheorem  defines U+ COHSP_1:def_22_:_
 for x, y being set holds x U+ y = Union (disjoin <*x,y*>);

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

theorem Th74: :: COHSP_1:74
for x being set holds
( x U+ {} = [:x,{1}:] &amp; {} U+ x = [:x,{2}:] )
proofend;

theorem Th75: :: COHSP_1:75
for x, y, z being set st z in x U+ y holds
( z = [(z `1),(z `2)] &amp; ( ( z `2 = 1 &amp; z `1 in x ) or ( z `2 = 2 &amp; z `1 in y ) ) )
proofend;

theorem Th76: :: COHSP_1:76
for x, y, z being set holds
( [z,1] in x U+ y iff z in x )
proofend;

theorem Th77: :: COHSP_1:77
for x, y, z being set holds
( [z,2] in x U+ y iff z in y )
proofend;

theorem Th78: :: COHSP_1:78
for x1, y1, x2, y2 being set holds
( x1 U+ y1 c= x2 U+ y2 iff ( x1 c= x2 &amp; y1 c= y2 ) )
proofend;

theorem Th79: :: COHSP_1:79
for x, y, z being set st z c= x U+ y holds
ex x1, y1 being set st
( z = x1 U+ y1 &amp; x1 c= x &amp; y1 c= y )
proofend;

theorem Th80: :: COHSP_1:80
for x1, y1, x2, y2 being set holds
( x1 U+ y1 = x2 U+ y2 iff ( x1 = x2 &amp; y1 = y2 ) )
proofend;

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

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

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

:: deftheorem  defines "/\" COHSP_1:def_23_:_
 for C1, C2 being Coherence_Space holds C1 "/\" C2 =  {  (a U+ b) where a is Element of C1, b is Element of C2 : verum  }  ;

:: deftheorem  defines "\/" COHSP_1:def_24_:_
 for C1, C2 being Coherence_Space holds C1 "\/" C2 =  {  (a U+ {}) where a is Element of C1 : verum  }  \/  {  ({} U+ b) where b is Element of C2 : verum  }  ;

theorem Th83: :: COHSP_1:83
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 Th84: :: COHSP_1:84
for C1, C2 being Coherence_Space
for x, y being set holds
( x U+ y in C1 "/\" C2 iff ( x in C1 &amp; y in C2 ) )
proofend;

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

theorem Th86: :: COHSP_1:86
for C1, C2 being Coherence_Space
for x, y being set holds
( x U+ y in C1 "\/" C2 iff ( ( x in C1 &amp; y = {} ) or ( x = {} &amp; y in C2 ) ) )
proofend;

theorem Th87: :: COHSP_1:87
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 &amp; ( a = {} or b = {} ) )
proofend;

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

registration
let C1, C2 be Coherence_Space;
clusterC1 "/\" C2 ->  non empty subset-closed binary_complete ;
coherence
 ( not C1 "/\" C2 is empty &amp; C1 "/\" C2 is subset-closed &amp; C1 "/\" C2 is binary_complete )
proofend;
clusterC1 "\/" C2 ->  non empty subset-closed binary_complete ;
coherence
 ( not C1 "\/" C2 is empty &amp; C1 "\/" C2 is subset-closed &amp; C1 "\/" C2 is binary_complete )
proofend;
end;

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

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

theorem :: COHSP_1:91
for C1, C2 being Coherence_Space
for x, y being set st x in union C1 &amp; y in union C2 holds
( [[x,1],[y,2]] in Web (C1 "/\" C2) &amp; [[y,2],[x,1]] in Web (C1 "/\" C2) )
proofend;

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

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

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

theorem :: COHSP_1:95
for C1, C2 being Coherence_Space holds 'not' (C1 "/\" C2) = ('not' C1) "\/" ('not' C2)
proofend;

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

:: deftheorem  defines [*] COHSP_1:def_25_:_
 for C1, C2 being Coherence_Space holds C1 [*] C2 = union  {  (bool [:a,b:]) where a is Element of C1, b is Element of C2 : verum  }  ;

theorem Th96: :: COHSP_1:96
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:] )
proofend;

registration
let C1, C2 be Coherence_Space;
clusterC1 [*] C2 ->  non empty ;
coherence
 not C1 [*] C2 is empty
proofend;
end;

theorem Th97: :: COHSP_1:97
for C1, C2 being Coherence_Space
for a being Element of C1 [*] C2 holds
( proj1 a in C1 &amp; proj2 a in C2 &amp; a c= [:(proj1 a),(proj2 a):] )
proofend;

registration
let C1, C2 be Coherence_Space;
clusterC1 [*] C2 ->  subset-closed binary_complete ;
coherence
 ( C1 [*] C2 is subset-closed &amp; C1 [*] C2 is binary_complete )
proofend;
end;

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

theorem :: COHSP_1:99
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 &amp; [x2,y2] in Web C2 ) )
proofend;