The abstract of the Mizar article:

Continuous, Stable, and Linear Maps of Coherence Spaces

by

Grzegorz Bancerek

Received August 30, 1995

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:
       not contradiction};
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;