:: Continuous, Stable, and Linear Maps of Coherence Spaces :: by Grzegorz Bancerek :: :: Received August 30, 1995 :: Copyright (c) 1995-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, FUNCT_1, SUBSET_1, TARSKI, COH_SP, FINSET_1, RELAT_1, CLASSES1, ZFMISC_1, FINSUB_1, CARD_1, ARYTM_3, ARYTM_1, MSSUBFAM, FUNCOP_1, PBOOLE, MCART_1, CARD_3, XBOOLEAN, FINSEQ_1, LATTICES, EQREL_1, COHSP_1, NAT_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, REAL_1, NAT_1, MCART_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, FINSUB_1, CLASSES1, COH_SP, PBOOLE, CARD_3, PARTFUN1, FUNCT_2, FUNCOP_1; constructors FINSUB_1, REAL_1, NAT_1, CARD_3, PBOOLE, BORSUK_1, COH_SP, XTUPLE_0, XREAL_0, NUMBERS, XFAMILY; registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1, XREAL_0, NAT_1, FINSEQ_1, ORDINAL1, CARD_1, RELAT_1, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET; begin definition 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; registration cluster finite for Coherence_Space; 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; registration 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; registration let C be non empty subset-closed set; cluster Sub_of_Fin C -> non empty subset-closed; end; theorem :: COHSP_1:4 Web {{}} = {}; scheme :: COHSP_1:sch 1 MinimalElementwrtIncl { 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() & P[a()] and a() is finite; registration let C be Coherence_Space; cluster finite for 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; registration cluster c=directed -> non empty for set; cluster c=filtered -> non empty for 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; registration cluster c=directed c=filtered finite for set; end; registration let C be non empty set; cluster c=directed c=filtered finite for Subset of C; end; theorem :: COHSP_1:12 for X being set holds Fin X is c=directed c=filtered; registration let X be set; cluster Fin X -> c=directed c=filtered; end; registration let C be subset-closed non empty set; cluster preBoolean non empty for 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; notation let X be set; synonym X is multiplicative for X is cap-closed; end; definition let X be set; attr X is d.union-closed means :: COHSP_1:def 6 for A being Subset of X st A is c=directed holds union A in X; end; registration cluster subset-closed -> multiplicative for set; end; theorem :: COHSP_1:14 for C being Coherence_Space, A being c=directed Subset of C holds union A in C; registration cluster -> d.union-closed for Coherence_Space; end; registration cluster multiplicative d.union-closed for 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 7 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:15 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 8 X includes_lattice_of {x, y}; end; theorem :: 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; begin :: Continuous, Stable, and Linear Functions definition let f be Function; attr f is union-distributive means :: COHSP_1:def 9 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 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; definition let f be Function; attr f is c=-monotone means :: 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; attr f is cap-distributive means :: 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; registration cluster d.union-distributive -> c=-monotone for Function; cluster union-distributive -> d.union-distributive for Function; end; theorem :: COHSP_1:17 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:18 for f being Function st f is union-distributive holds f.{} = {}; registration let C1,C2 be Coherence_Space; cluster union-distributive cap-distributive for Function of C1, C2; end; registration let C be Coherence_Space; cluster union-distributive cap-distributive for 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 13 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 14 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 15 f is U-stable union-distributive; end; registration cluster U-continuous -> d.union-distributive for Function; cluster U-stable -> cap-distributive U-continuous for Function; cluster U-linear -> union-distributive U-stable for Function; end; registration let X be d.union-closed set; cluster d.union-distributive -> U-continuous for ManySortedSet of X; end; registration let X be multiplicative set; cluster U-continuous cap-distributive -> U-stable for ManySortedSet of X; end; registration cluster U-stable union-distributive -> U-linear for Function; end; registration cluster U-linear for Function; let C be Coherence_Space; cluster U-linear for ManySortedSet of C; let B be Coherence_Space; cluster U-linear for Function of B,C; end; registration let f be U-continuous Function; cluster dom f -> d.union-closed; end; registration let f be U-stable Function; cluster dom f -> multiplicative; end; theorem :: COHSP_1:19 for X being set holds union Fin X = X; theorem :: COHSP_1:20 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: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 ex b being set st b is finite & b c= a & y in f.b; theorem :: COHSP_1:22 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:23 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 16 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; registration let f be Function; cluster graph f -> Relation-like; end; theorem :: COHSP_1:24 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:25 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: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; 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 for y1,y2 being set st [a,y1] in graph f & [b,y2] in graph f holds {y1,y2} in C2; theorem :: 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; 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 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: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; begin :: Trace of Stable Function definition let f be Function; func Trace f -> set means :: 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; end; theorem :: COHSP_1:31 for f being Function for a being set, y being object 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; registration let f be Function; cluster Trace f -> Relation-like; end; theorem :: COHSP_1:32 for f being U-continuous Function st dom f is subset-closed holds Trace f c= graph f; theorem :: COHSP_1:33 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: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 for y1,y2 being object st [a1,y1] in Trace f & [a2,y2] in Trace f holds {y1,y2} in C2; theorem :: 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 for y being object st [a1, y] in Trace f & [a2,y] in Trace f holds a1 = a2; theorem :: 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 for a being Element of C1 holds f.a c= g.a; theorem :: 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; theorem :: 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 for y1,y2 being object 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 object 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: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; theorem :: COHSP_1:40 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:41 for C1, C2 being Coherence_Space ex f being U-stable Function of C1, C2 st Trace f = {}; theorem :: COHSP_1:42 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:43 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: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; theorem :: 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 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 18 for x being set holds x in it iff ex f being U-stable Function of C1,C2 st x = Trace f; end; registration let C1, C2 be Coherence_Space; cluster StabCoh(C1,C2) -> non empty subset-closed binary_complete; end; theorem :: COHSP_1:46 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:47 for C1,C2 being Coherence_Space holds union StabCoh(C1,C2) = [: Sub_of_Fin C1, union C2:]; theorem :: COHSP_1:48 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:49 for C1, C2 being Coherence_Space for f being U-stable Function of C1,C2 holds f is U-linear iff for a being set, y being object 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 19 for x being object holds x in it iff ex y ,z being object st x = [y,z] & [{y},z] in Trace f; end; theorem :: COHSP_1:50 for f being Function, x,y being object holds [x,y] in LinTrace f iff [{x},y] in Trace f; theorem :: COHSP_1:51 for f being Function st f.{} = {} for x,y being object st {x} in dom f & y in f.{x} holds [x,y] in LinTrace f; theorem :: COHSP_1:52 for f being Function, x,y being object 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; registration 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 20 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:53 for C1, C2 being Coherence_Space for f being c=-monotone Function of C1,C2 for x1,x2 being object st {x1,x2} in C1 for y1,y2 being object st [ x1,y1] in LinTrace f & [x2,y2] in LinTrace f holds {y1,y2} in C2; theorem :: 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 for y being object st [x1,y ] in LinTrace f & [x2,y] in LinTrace f holds x1 = x2; theorem :: 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; theorem :: 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 for y1,y2 being object 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 object 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: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; theorem :: COHSP_1:58 for C1, C2 being Coherence_Space ex f being U-linear Function of C1, C2 st LinTrace f = {}; theorem :: COHSP_1:59 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:60 for C1, C2 being Coherence_Space for x being set, y being set st x in union C1 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: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; theorem :: 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 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; registration let C1, C2 be Coherence_Space; cluster LinCoh(C1,C2) -> non empty subset-closed binary_complete; end; theorem :: COHSP_1:63 for C1,C2 being Coherence_Space holds union LinCoh(C1,C2) = [:union C1 , union C2:]; theorem :: COHSP_1:64 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 21 {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:65 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}; registration let C be Coherence_Space; cluster 'not' C -> non empty subset-closed binary_complete; end; theorem :: COHSP_1:66 for C being Coherence_Space holds union 'not' C = union C; theorem :: COHSP_1:67 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:68 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:69 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:70 for C being Coherence_Space holds 'not' 'not' C = C; theorem :: COHSP_1:71 'not' {{}} = {{}}; theorem :: COHSP_1:72 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 22 Union disjoin <*x,y*>; end; theorem :: COHSP_1:73 for x,y being set holds x U+ y = [:x,{1}:] \/ [:y,{2}:]; theorem :: COHSP_1:74 for x being set holds x U+ {} = [:x,{1}:] & {} U+ x = [:x,{2}:]; theorem :: COHSP_1:75 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:76 for x,y being set, z being object holds [z,1] in x U+ y iff z in x; theorem :: COHSP_1:77 for x,y being set, z being object holds [z,2] in x U+ y iff z in y; theorem :: COHSP_1:78 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:79 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:80 for x1,y1, x2,y2 being set holds x1 U+ y1 = x2 U+ y2 iff x1 = x2 & y1 = y2; theorem :: COHSP_1:81 for x1,y1, x2,y2 being set holds x1 U+ y1 \/ x2 U+ y2 = (x1 \/ x2) U+ (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); definition let C1, C2 be Coherence_Space; func C1 "/\" C2 -> set equals :: COHSP_1:def 23 the set of all a U+ b where a is Element of C1, b is Element of C2; func C1 "\/" C2 -> set equals :: COHSP_1:def 24 (the set of all a U+ {} where a is Element of C1) \/ (the set of all {} U+ b where b is Element of C2); end; theorem :: COHSP_1:83 for C1,C2 being Coherence_Space for x being object 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:84 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:85 for C1,C2 being Coherence_Space holds union (C1 "/\" C2) = ( union C1) U+ (union C2); theorem :: 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 & y = {} or x = {} & y in C2; theorem :: COHSP_1:87 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:88 for C1,C2 being Coherence_Space holds union (C1 "\/" C2) = (union C1) U+ (union C2); registration 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:89 for x,y being set holds [[x,1],[y,1]] in Web (C1 "/\" C2) iff [x,y] in Web C1 ; theorem :: COHSP_1:90 for x,y being set holds [[x,2],[y,2]] in Web (C1 "/\" C2) iff [x,y] in Web C2 ; theorem :: COHSP_1:91 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:92 for x,y being set holds [[x,1],[y,1]] in Web (C1 "\/" C2) iff [x,y] in Web C1 ; theorem :: COHSP_1:93 for x,y being set holds [[x,2],[y,2]] in Web (C1 "\/" C2) iff [x,y] in Web C2 ; theorem :: COHSP_1:94 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:95 'not' (C1 "/\" C2) = 'not' C1 "\/" 'not' C2; definition let C1,C2 be Coherence_Space; func C1 [*] C2 -> set equals :: COHSP_1:def 25 union the set of all bool [:a,b:] where a is Element of C1, b is Element of C2; end; theorem :: COHSP_1:96 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:]; registration let C1,C2 be Coherence_Space; cluster C1 [*] C2 -> non empty; end; theorem :: COHSP_1:97 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:]; registration let C1,C2 be Coherence_Space; cluster C1 [*] C2 -> subset-closed binary_complete; end; theorem :: COHSP_1:98 for C1,C2 being Coherence_Space holds union (C1 [*] C2) = [:union C1, union C2:]; theorem :: COHSP_1:99 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;