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

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

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

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

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

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

definition

let X be set ;

correctness

coherence

CohSp (id X) is set ;

;

ex b_{1} being Subset of X st

for x being set holds

( x in b_{1} iff ( x in X & x is finite ) )

uniqueness

for b_{1}, b_{2} being Subset of X st ( for x being set holds

( x in b_{1} iff ( x in X & x is finite ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X & x is finite ) ) ) holds

b_{1} = b_{2};

end;
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 for x being set holds

( x in it iff ( x in X & x is finite ) );

ex b

for x being set holds

( x in b

proof end;

correctness uniqueness

for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines Sub_of_Fin COHSP_1:def 3 :

for X being set

for b_{2} being Subset of X holds

( b_{2} = Sub_of_Fin X iff for x being set holds

( x in b_{2} iff ( x in X & x is finite ) ) );

for X being set

for b

( b

( x in b

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

( x in FlatCoh X iff ( x = {} or ex y being set st

( x = {y} & y in X ) ) )

proof end;

registration

coherence

( {{}} is subset-closed & {{}} is binary_complete ) by COH_SP:3;

let X be set ;

coherence

( bool X is subset-closed & bool X is binary_complete ) by COH_SP:2;

coherence

( not FlatCoh X is empty & FlatCoh X is subset-closed & FlatCoh X is binary_complete ) ;

end;
( {{}} is subset-closed & {{}} is binary_complete ) by COH_SP:3;

let X be set ;

coherence

( bool X is subset-closed & bool X is binary_complete ) by COH_SP:2;

coherence

( not FlatCoh X is empty & FlatCoh X is subset-closed & FlatCoh X is binary_complete ) ;

registration

let C be non empty subset-closed set ;

coherence

( not Sub_of_Fin C is empty & Sub_of_Fin C is subset-closed )

end;
coherence

( not Sub_of_Fin C is empty & Sub_of_Fin C is subset-closed )

proof end;

registration
end;

definition

let X be set ;

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

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

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

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

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

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

coherence

for b_{1} being set st b_{1} is c=directed holds

not b_{1} is empty

for b_{1} being set st b_{1} is c=filtered holds

not b_{1} is empty

end;
for b

not b

proof end;

coherence for b

not b

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

for a, b being set st a in X & b in X holds

ex c being set st

( a \/ b c= c & c in X )

proof end;

theorem Th6: :: COHSP_1:6

for X being non empty set st ( for a, b being set st a in X & b in X holds

ex c being set st

( a \/ b c= c & c in X ) ) holds

X is c=directed

ex c being set st

( a \/ b c= c & c in X ) ) holds

X is c=directed

proof end;

theorem :: COHSP_1:7

for X being set st X is c=filtered holds

for a, b being set st a in X & b in X holds

ex c being set st

( c c= a /\ b & c in X )

for a, b being set st a in X & b in X holds

ex c being set st

( c c= a /\ b & c in X )

proof end;

theorem Th8: :: COHSP_1:8

for X being non empty set st ( for a, b being set st a in X & b in X holds

ex c being set st

( c c= a /\ b & c in X ) ) holds

X is c=filtered

ex c being set st

( c c= a /\ b & c in X ) ) holds

X is c=filtered

proof end;

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

registration

existence

ex b_{1} being set st

( b_{1} is c=directed & b_{1} is c=filtered & b_{1} is finite )

end;
ex b

( b

proof end;

registration

let C be non empty set ;

existence

ex b_{1} being Subset of C st

( b_{1} is c=directed & b_{1} is c=filtered & b_{1} is finite )

end;
existence

ex b

( b

proof end;

Lm3: now :: thesis: for C being non empty subset-closed set

for a being Element of C holds Fin a c= C

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

end;
let a be Element of C; :: thesis: Fin a c= C

thus Fin a c= C :: thesis: verum

proof

let x be set ; :: according to TARSKI: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;
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

registration

let C be non empty subset-closed set ;

existence

ex b_{1} being Subset of C st

( b_{1} is preBoolean & not b_{1} is empty )

end;
existence

ex b

( b

proof 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

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

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

for Y being set st X is c=directed & Y c= union X & Y is finite holds

ex Z being set st

( Z in X & Y c= Z )

proof end;

definition

let X be set ;

end;
attr X 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;

for A being Subset of X st A is c=directed holds

union A in X;

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

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

registration
end;

registration

existence

ex b_{1} being Coherence_Space st

( b_{1} is multiplicative & b_{1} is d.union-closed )

end;
ex b

( b

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

definition

let X, Y be set ;

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

for a, b being set st a in Y & b in Y holds

( a /\ b in X & a \/ b in X );

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

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

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

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

( X includes_lattice_of x,y iff ( x in X & y in X & x /\ y in X & x \/ y in X ) )

proof end;

begin

definition

let f be Function;

end;
attr f 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);

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

for A being Subset of (dom f) st A is c=directed & union A in dom f holds

f . (union A) = union (f .: A);

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

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

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;

end;
attr f 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;

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

for a, b being set st dom f includes_lattice_of a,b holds

f . (a /\ b) = (f . a) /\ (f . b);

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

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

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

coherence

for b_{1} being Function st b_{1} is d.union-distributive holds

b_{1} is c=-monotone

for b_{1} being Function st b_{1} is union-distributive holds

b_{1} is d.union-distributive

end;
for b

b

proof end;

coherence for b

b

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

for x, y being set st x in dom f & y in dom f & x \/ y in dom f holds

f . (x \/ y) = (f . x) \/ (f . y)

proof end;

registration

let C1, C2 be Coherence_Space;

ex b_{1} being Function of C1,C2 st

( b_{1} is union-distributive & b_{1} is cap-distributive )

end;
cluster Relation-like C1 -defined C2 -valued Function-like V34(C1,C2) union-distributive cap-distributive for Element of bool [:C1,C2:];

existence ex b

( b

proof end;

registration

let C be Coherence_Space;

existence

ex b_{1} being ManySortedSet of C st

( b_{1} is union-distributive & b_{1} is cap-distributive )

end;
existence

ex b

( b

proof end;

definition

let f be Function;

end;
attr f is U-continuous means :Def13: :: COHSP_1:def 13

( dom f is d.union-closed & f is d.union-distributive );

( dom f is d.union-closed & f is d.union-distributive );

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

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;

end;
attr f is U-stable means :Def14: :: COHSP_1:def 14

( dom f is multiplicative & f is U-continuous & f is cap-distributive );

( dom f is multiplicative & f is U-continuous & f is cap-distributive );

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

for f being Function holds

( f is U-stable iff ( dom f is multiplicative & f is U-continuous & f is cap-distributive ) );

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

for f being Function holds

( f is U-linear iff ( f is U-stable & f is union-distributive ) );

registration

coherence

for b_{1} being Function st b_{1} is U-continuous holds

b_{1} is d.union-distributive
by Def13;

coherence

for b_{1} being Function st b_{1} is U-stable holds

( b_{1} is cap-distributive & b_{1} is U-continuous )
by Def14;

coherence

for b_{1} being Function st b_{1} is U-linear holds

( b_{1} is union-distributive & b_{1} is U-stable )
by Def15;

end;
for b

b

coherence

for b

( b

coherence

for b

( b

registration

let X be d.union-closed set ;

for b_{1} being ManySortedSet of X st b_{1} is d.union-distributive holds

b_{1} is U-continuous

end;
cluster Relation-like X -defined Function-like V30(X) d.union-distributive -> U-continuous for set ;

coherence for b

b

proof end;

registration

let X be multiplicative set ;

for b_{1} being ManySortedSet of X st b_{1} is U-continuous & b_{1} is cap-distributive holds

b_{1} is U-stable

end;
cluster Relation-like X -defined Function-like V30(X) cap-distributive U-continuous -> U-stable for set ;

coherence for b

b

proof end;

registration

coherence

for b_{1} being Function st b_{1} is U-stable & b_{1} is union-distributive holds

b_{1} is U-linear
by Def15;

end;
for b

b

registration

existence

ex b_{1} being Function st b_{1} is U-linear

existence

ex b_{1} being ManySortedSet of C st b_{1} is U-linear

ex b_{1} being Function of B,C st b_{1} is U-linear

end;
ex b

proof end;

let C be Coherence_Space;existence

ex b

proof end;

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 b

proof end;

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

for a being set st a in dom f holds

f . a = union (f .: (Fin a))

proof end;

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

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

ex b being set st

( b is finite & b c= a & y in f . b ) ) ) )

proof end;

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

( f is U-stable iff ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds

ex b being set st

( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds

b c= c ) ) ) ) )

proof end;

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

( f is U-linear iff ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds

ex x being set st

( x in a & y in f . {x} & ( for b being set st b c= a & y in f . b holds

x in b ) ) ) ) )

proof end;

begin

definition

let f be Function;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex y being finite set ex z being set st

( x = [y,z] & y in dom f & z in f . y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} 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 b_{2} iff ex y being finite set ex z being set st

( x = [y,z] & y in dom f & z in f . y ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being set holds

( x in b

( x = [y,z] & y in dom f & z in f . y ) )

proof end;

uniqueness for b

( x in b

( x = [y,z] & y in dom f & z in f . y ) ) ) & ( for x being set holds

( x in b

( x = [y,z] & y in dom f & z in f . y ) ) ) holds

b

proof end;

:: deftheorem Def16 defines graph COHSP_1:def 16 :

for f being Function

for b_{2} being set holds

( b_{2} = graph f iff for x being set holds

( x in b_{2} iff ex y being finite set ex z being set st

( x = [y,z] & y in dom f & z in f . y ) ) );

for f being Function

for b

( b

( x in b

( 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):]

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

proof end;

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

for x, y being set holds

( [x,y] in graph f iff ( x is finite & x in dom f & y in f . x ) )

proof end;

theorem 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

for a, b being set st b in dom f & a c= b & b is finite holds

for y being set st [a,y] in graph f holds

[b,y] in graph f

proof end;

theorem 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

for f being Function of C1,C2

for a being Element of C1

for y1, y2 being set st [a,y1] in graph f & [a,y2] in graph f holds

{y1,y2} in C2

proof end;

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

for f being c=-monotone Function of C1,C2

for a, b being Element of C1 st a \/ b in C1 holds

for y1, y2 being set st [a,y1] in graph f & [b,y2] in graph f holds

{y1,y2} in C2

proof end;

theorem 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

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

f = g

proof end;

Lm4: for C1, C2 being Coherence_Space

for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds

x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds

for y being set st [a,y] in X holds

[b,y] in X ) & ( for a being finite Element of C1

for y1, y2 being set st [a,y1] in X & [a,y2] in X holds

{y1,y2} in C2 ) holds

ex f being U-continuous Function of C1,C2 st

( X = graph f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )

proof end;

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

for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds

x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds

for y being set st [a,y] in X holds

[b,y] in X ) & ( for a being finite Element of C1

for y1, y2 being set st [a,y1] in X & [a,y2] in X holds

{y1,y2} in C2 ) holds

ex f being U-continuous Function of C1,C2 st X = graph f

proof end;

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

for f being U-continuous Function of C1,C2

for a being Element of C1 holds f . a = (graph f) .: (Fin a)

proof end;

begin

definition

let f be Function;

ex b_{1} being set st

for x being set holds

( x in b_{1} 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 b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} 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 b_{2} 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

b_{1} = b_{2}

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

ex b

for x being set holds

( x in b

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

proof end;

uniqueness for b

( x in b

( 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 b

( 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

b

proof end;

:: deftheorem Def17 defines Trace COHSP_1:def 17 :

for f being Function

for b_{2} being set holds

( b_{2} = Trace f iff for x being set holds

( x in b_{2} 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 f being Function

for b

( b

( x in b

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

for a, y being set holds

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

a = b ) ) )

proof end;

definition

let C1, C2 be non empty set ;

let f be Function of C1,C2;

:: original: Trace

redefine func Trace f -> Subset of [:C1,(union C2):];

coherence

Trace f is Subset of [:C1,(union C2):]

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

proof end;

registration
end;

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

for a, y being set st [a,y] in Trace f holds

a is finite

proof end;

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

for f being c=-monotone Function of C1,C2

for a1, a2 being set st a1 \/ a2 in C1 holds

for y1, y2 being set st [a1,y1] in Trace f & [a2,y2] in Trace f holds

{y1,y2} in C2

proof end;

theorem 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

for f being cap-distributive Function of C1,C2

for a1, a2 being set st a1 \/ a2 in C1 holds

for y being set st [a1,y] in Trace f & [a2,y] in Trace f holds

a1 = a2

proof end;

theorem 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

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

for a being Element of C1 holds f . a c= g . a

proof end;

theorem 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

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

f = g

proof end;

Lm5: for C1, C2 being Coherence_Space

for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds

x `1 is finite ) & ( for a, b being Element of C1 st a \/ b in C1 holds

for y1, y2 being set st [a,y1] in X & [b,y2] in X holds

{y1,y2} in C2 ) & ( for a, b being Element of C1 st a \/ b in C1 holds

for y being set st [a,y] in X & [b,y] in X holds

a = b ) holds

ex f being U-stable Function of C1,C2 st

( X = Trace f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )

proof end;

theorem 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

for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds

x `1 is finite ) & ( for a, b being Element of C1 st a \/ b in C1 holds

for y1, y2 being set st [a,y1] in X & [b,y2] in X holds

{y1,y2} in C2 ) & ( for a, b being Element of C1 st a \/ b in C1 holds

for y being set st [a,y] in X & [b,y] in X holds

a = b ) holds

ex f being U-stable Function of C1,C2 st X = Trace f

proof end;

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

for f being U-stable Function of C1,C2

for a being Element of C1 holds f . a = (Trace f) .: (Fin a)

proof end;

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

for f being U-stable Function of C1,C2

for a being Element of C1

for y being set holds

( y in f . a iff ex b being Element of C1 st

( [b,y] in Trace f & b c= a ) )

proof end;

theorem 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]}

for a being finite Element of C1

for y being set st y in union C2 holds

ex f being U-stable Function of C1,C2 st Trace f = {[a,y]}

proof end;

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

for a being Element of C1

for y being set

for f being U-stable Function of C1,C2 st Trace f = {[a,y]} holds

for b being Element of C1 holds

( ( a c= b implies f . b = {y} ) & ( not a c= b implies f . b = {} ) )

proof end;

theorem 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

for f being U-stable Function of C1,C2

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

proof end;

theorem 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

for A being set st ( for x, y being set st x in A & y in A holds

ex f being U-stable Function of C1,C2 st x \/ y = Trace f ) holds

ex f being U-stable Function of C1,C2 st union A = Trace f

proof end;

definition

let C1, C2 be Coherence_Space;

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex f being U-stable Function of C1,C2 st x = Trace f ) ) & ( for x being set holds

( x in b_{2} iff ex f being U-stable Function of C1,C2 st x = Trace f ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex f being U-stable Function of C1,C2 st x = Trace f )

end;
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 x being set holds

( x in it iff ex f being U-stable Function of C1,C2 st x = Trace f );

for b

( x in b

( x in b

b

proof end;

existence ex b

for x being set holds

( x in b

proof end;

:: deftheorem Def18 defines StabCoh COHSP_1:def 18 :

for C1, C2 being Coherence_Space

for b_{3} being set holds

( b_{3} = StabCoh (C1,C2) iff for x being set holds

( x in b_{3} iff ex f being U-stable Function of C1,C2 st x = Trace f ) );

for C1, C2 being Coherence_Space

for b

( b

( x in b

registration

let C1, C2 be Coherence_Space;

coherence

( not StabCoh (C1,C2) is empty & StabCoh (C1,C2) is subset-closed & StabCoh (C1,C2) is binary_complete )

end;
coherence

( not StabCoh (C1,C2) is empty & StabCoh (C1,C2) is subset-closed & StabCoh (C1,C2) is binary_complete )

proof 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):]

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

proof end;

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

for a, b being finite Element of C1

for y1, y2 being set holds

( [[a,y1],[b,y2]] in Web (StabCoh (C1,C2)) iff ( ( not a \/ b in C1 & y1 in union C2 & y2 in union C2 ) or ( [y1,y2] in Web C2 & ( y1 = y2 implies a = b ) ) ) )

proof end;

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

for f being U-stable Function of C1,C2 holds

( f is U-linear iff for a, y being set st [a,y] in Trace f holds

ex x being set st a = {x} )

proof end;

definition

let f be Function;

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex y, z being set st

( x = [y,z] & [{y},z] in Trace f ) ) ) & ( for x being set holds

( x in b_{2} iff ex y, z being set st

( x = [y,z] & [{y},z] in Trace f ) ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex y, z being set st

( x = [y,z] & [{y},z] in Trace f ) )

end;
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 x being set holds

( x in it iff ex y, z being set st

( x = [y,z] & [{y},z] in Trace f ) );

for b

( x in b

( x = [y,z] & [{y},z] in Trace f ) ) ) & ( for x being set holds

( x in b

( x = [y,z] & [{y},z] in Trace f ) ) ) holds

b

proof end;

existence ex b

for x being set holds

( x in b

( x = [y,z] & [{y},z] in Trace f ) )

proof end;

:: deftheorem Def19 defines LinTrace COHSP_1:def 19 :

for f being Function

for b_{2} being set holds

( b_{2} = LinTrace f iff for x being set holds

( x in b_{2} iff ex y, z being set st

( x = [y,z] & [{y},z] in Trace f ) ) );

for f being Function

for b

( b

( x in b

( x = [y,z] & [{y},z] in Trace f ) ) );

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

for x, y being set st {x} in dom f & y in f . {x} holds

[x,y] in LinTrace f

proof end;

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

for x, y being set st [x,y] in LinTrace f holds

( {x} in dom f & y in f . {x} )

proof end;

definition

let C1, C2 be non empty set ;

let f be Function of C1,C2;

:: original: LinTrace

redefine func LinTrace f -> Subset of [:(union C1),(union C2):];

coherence

LinTrace f is Subset of [:(union C1),(union C2):]

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

proof end;

definition

let C1, C2 be Coherence_Space;

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex f being U-linear Function of C1,C2 st x = LinTrace f ) ) & ( for x being set holds

( x in b_{2} iff ex f being U-linear Function of C1,C2 st x = LinTrace f ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex f being U-linear Function of C1,C2 st x = LinTrace f )

end;
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 x being set holds

( x in it iff ex f being U-linear Function of C1,C2 st x = LinTrace f );

for b

( x in b

( x in b

b

proof end;

existence ex b

for x being set holds

( x in b

proof end;

:: deftheorem Def20 defines LinCoh COHSP_1:def 20 :

for C1, C2 being Coherence_Space

for b_{3} being set holds

( b_{3} = LinCoh (C1,C2) iff for x being set holds

( x in b_{3} iff ex f being U-linear Function of C1,C2 st x = LinTrace f ) );

for C1, C2 being Coherence_Space

for b

( b

( x in b

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

for f being c=-monotone Function of C1,C2

for x1, x2 being set st {x1,x2} in C1 holds

for y1, y2 being set st [x1,y1] in LinTrace f & [x2,y2] in LinTrace f holds

{y1,y2} in C2

proof end;

theorem 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

for f being cap-distributive Function of C1,C2

for x1, x2 being set st {x1,x2} in C1 holds

for y being set st [x1,y] in LinTrace f & [x2,y] in LinTrace f holds

x1 = x2

proof end;

theorem 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

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

f = g

proof end;

Lm6: for C1, C2 being Coherence_Space

for X being Subset of [:(union C1),(union C2):] st ( for a, b being set st {a,b} in C1 holds

for y1, y2 being set st [a,y1] in X & [b,y2] in X holds

{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds

for y being set st [a,y] in X & [b,y] in X holds

a = b ) holds

ex f being U-linear Function of C1,C2 st

( X = LinTrace f & ( for a being Element of C1 holds f . a = X .: a ) )

proof end;

theorem 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

for X being Subset of [:(union C1),(union C2):] st ( for a, b being set st {a,b} in C1 holds

for y1, y2 being set st [a,y1] in X & [b,y2] in X holds

{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds

for y being set st [a,y] in X & [b,y] in X holds

a = b ) holds

ex f being U-linear Function of C1,C2 st X = LinTrace f

proof end;

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

for f being U-linear Function of C1,C2

for a being Element of C1 holds f . a = (LinTrace f) .: a

proof end;

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]}

for x, y being set st x in union C1 & y in union C2 holds

ex f being U-linear Function of C1,C2 st LinTrace f = {[x,y]}

proof end;

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

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 = {} ) )

proof end;

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

for f being U-linear Function of C1,C2

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

proof end;

theorem 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

for A being set st ( for x, y being set st x in A & y in A holds

ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f ) holds

ex f being U-linear Function of C1,C2 st union A = LinTrace f

proof end;

registration

let C1, C2 be Coherence_Space;

coherence

( not LinCoh (C1,C2) is empty & LinCoh (C1,C2) is subset-closed & LinCoh (C1,C2) is binary_complete )

end;
coherence

( not LinCoh (C1,C2) is empty & LinCoh (C1,C2) is subset-closed & LinCoh (C1,C2) is binary_complete )

proof end;

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

for x1, x2, y1, y2 being set holds

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

proof end;

begin

definition

let C be Coherence_Space;

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;
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 { a where a is Subset of (union C) : for b being Element of C ex x being set st a /\ b c= {x} } ;

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 ;

;

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

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

for x being set holds

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

proof end;

registration

let C be Coherence_Space;

coherence

( not 'not' C is empty & 'not' C is subset-closed & 'not' C is binary_complete )

end;
coherence

( not 'not' C is empty & 'not' C is subset-closed & 'not' C is binary_complete )

proof end;

theorem Th68: :: COHSP_1:68

for C being Coherence_Space

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

{x,y} in 'not' C

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

{x,y} in 'not' C

proof end;

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

for x, y being set holds

( [x,y] in Web ('not' C) iff ( x in union C & y in union C & ( x = y or not [x,y] in Web C ) ) )

proof end;

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

proof end;

begin

:: deftheorem defines U+ COHSP_1:def 22 :

for x, y being set holds x U+ y = Union (disjoin <*x,y*>);

for x, y being set holds x U+ y = Union (disjoin <*x,y*>);

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

( z = [(z `1),(z `2)] & ( ( z `2 = 1 & z `1 in x ) or ( z `2 = 2 & z `1 in y ) ) )

proof end;

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 & x1 c= x & y1 c= y )

ex x1, y1 being set st

( z = x1 U+ y1 & x1 c= x & y1 c= y )

proof end;

definition

let C1, C2 be Coherence_Space;

coherence

{ (a U+ b) where a is Element of C1, b is Element of C2 : verum } is set ;

;

coherence

{ (a U+ {}) where a is Element of C1 : verum } \/ { ({} U+ b) where b is Element of C2 : verum } is set ;

;

end;
func C1 "/\" C2 -> set equals :: COHSP_1:def 23

{ (a U+ b) where a is Element of C1, b is Element of C2 : verum } ;

correctness { (a U+ b) where a is Element of C1, b is Element of C2 : verum } ;

coherence

{ (a U+ b) where a is Element of C1, b is Element of C2 : verum } is set ;

;

func C1 "\/" 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 { (a U+ {}) where a is Element of C1 : verum } \/ { ({} U+ b) where b is Element of C2 : verum } ;

coherence

{ (a U+ {}) where a is Element of C1 : verum } \/ { ({} U+ b) where b is Element of C2 : verum } is set ;

;

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

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

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 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 & y in C2 ) )

for x, y being set holds

( x U+ y in C1 "/\" C2 iff ( x in C1 & y in C2 ) )

proof end;

theorem Th86: :: COHSP_1:86

for C1, C2 being Coherence_Space

for x, y being set holds

( x U+ y in C1 "\/" C2 iff ( ( x in C1 & y = {} ) or ( x = {} & y in C2 ) ) )

for x, y being set holds

( x U+ y in C1 "\/" C2 iff ( ( x in C1 & y = {} ) or ( x = {} & y in C2 ) ) )

proof end;

theorem 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 & ( a = {} or b = {} ) )

for x being set st x in C1 "\/" C2 holds

ex a being Element of C1 ex b being Element of C2 st

( x = a U+ b & ( a = {} or b = {} ) )

proof end;

registration

let C1, C2 be Coherence_Space;

coherence

( not C1 "/\" C2 is empty & C1 "/\" C2 is subset-closed & C1 "/\" C2 is binary_complete )

( not C1 "\/" C2 is empty & C1 "\/" C2 is subset-closed & C1 "\/" C2 is binary_complete )

end;
coherence

( not C1 "/\" C2 is empty & C1 "/\" C2 is subset-closed & C1 "/\" C2 is binary_complete )

proof end;

coherence ( not C1 "\/" C2 is empty & C1 "\/" C2 is subset-closed & C1 "\/" C2 is binary_complete )

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

for x, y being set holds

( [[x,1],[y,1]] in Web (C1 "/\" C2) iff [x,y] in Web C1 )

proof end;

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

for x, y being set holds

( [[x,2],[y,2]] in Web (C1 "/\" C2) iff [x,y] in Web C2 )

proof end;

theorem :: COHSP_1:91

for C1, C2 being Coherence_Space

for x, y being set st x in union C1 & y in union C2 holds

( [[x,1],[y,2]] in Web (C1 "/\" C2) & [[y,2],[x,1]] in Web (C1 "/\" C2) )

for x, y being set st x in union C1 & y in union C2 holds

( [[x,1],[y,2]] in Web (C1 "/\" C2) & [[y,2],[x,1]] in Web (C1 "/\" C2) )

proof end;

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

for x, y being set holds

( [[x,1],[y,1]] in Web (C1 "\/" C2) iff [x,y] in Web C1 )

proof end;

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

for x, y being set holds

( [[x,2],[y,2]] in Web (C1 "\/" C2) iff [x,y] in Web C2 )

proof end;

theorem :: COHSP_1:94

for C1, C2 being Coherence_Space

for x, y being set holds

( not [[x,1],[y,2]] in Web (C1 "\/" C2) & not [[y,2],[x,1]] in Web (C1 "\/" C2) )

for x, y being set holds

( not [[x,1],[y,2]] in Web (C1 "\/" C2) & not [[y,2],[x,1]] in Web (C1 "\/" C2) )

proof end;

definition

let C1, C2 be Coherence_Space;

coherence

union { (bool [:a,b:]) where a is Element of C1, b is Element of C2 : verum } is set ;

;

end;
func C1 [*] C2 -> set equals :: COHSP_1:def 25

union { (bool [:a,b:]) where a is Element of C1, b is Element of C2 : verum } ;

correctness union { (bool [:a,b:]) where a is Element of C1, b is Element of C2 : verum } ;

coherence

union { (bool [:a,b:]) where a is Element of C1, b is Element of C2 : verum } is set ;

;

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

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:] )

for x being set holds

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

proof end;

theorem Th97: :: COHSP_1:97

for C1, C2 being Coherence_Space

for a being Element of C1 [*] C2 holds

( proj1 a in C1 & proj2 a in C2 & a c= [:(proj1 a),(proj2 a):] )

for a being Element of C1 [*] C2 holds

( proj1 a in C1 & proj2 a in C2 & a c= [:(proj1 a),(proj2 a):] )

proof end;

registration

let C1, C2 be Coherence_Space;

coherence

( C1 [*] C2 is subset-closed & C1 [*] C2 is binary_complete )

end;
coherence

( C1 [*] C2 is subset-closed & C1 [*] C2 is binary_complete )

proof end;

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 & [x2,y2] in Web C2 ) )

for x1, y1, x2, y2 being set holds

( [[x1,x2],[y1,y2]] in Web (C1 [*] C2) iff ( [x1,y1] in Web C1 & [x2,y2] in Web C2 ) )

proof end;

:: cluster union-distributive cap-distributive Function;

::end;