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;
:: deftheorem Def1 defines binary_complete COHSP_1:def 1 :
:: deftheorem defines FlatCoh COHSP_1:def 2 :
:: deftheorem Def3 defines Sub_of_Fin COHSP_1:def 3 :
theorem Th1:
theorem Th2:
theorem
theorem
scheme
MinimalElementwrtIncl{
F1()
-> set ,
F2()
-> set ,
P1[
set ] } :
ex
a being
set st
(
a in F2() &
P1[
a] & ( for
b being
set st
b in F2() &
P1[
b] &
b c= a holds
b = a ) )
provided
A1:
(
F1()
in F2() &
P1[
F1()] )
and A2:
F1() is
finite
:: deftheorem defines c=directed COHSP_1:def 4 :
:: deftheorem defines c=filtered COHSP_1:def 5 :
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem
theorem
theorem Th12:
theorem Th13:
:: deftheorem COHSP_1:def 6 :
canceled;
:: deftheorem Def7 defines d.union-closed COHSP_1:def 7 :
theorem
canceled;
theorem Th15:
:: deftheorem defines includes_lattice_of COHSP_1:def 8 :
theorem
:: deftheorem defines includes_lattice_of COHSP_1:def 9 :
theorem Th17:
begin
:: deftheorem Def10 defines union-distributive COHSP_1:def 10 :
:: deftheorem Def11 defines d.union-distributive COHSP_1:def 11 :
:: deftheorem Def12 defines c=-monotone COHSP_1:def 12 :
:: deftheorem Def13 defines cap-distributive COHSP_1:def 13 :
theorem
theorem Th19:
:: deftheorem Def14 defines U-continuous COHSP_1:def 14 :
:: deftheorem Def15 defines U-stable COHSP_1:def 15 :
:: deftheorem Def16 defines U-linear COHSP_1:def 16 :
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
begin
:: deftheorem Def17 defines graph COHSP_1:def 17 :
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem Th29:
Lm4:
for C1, C2 being Coherence_Space
for X being Subset of 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) ) )
theorem
theorem
begin
:: deftheorem Def18 defines Trace COHSP_1:def 18 :
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
Lm5:
for C1, C2 being Coherence_Space
for X being Subset of 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) ) )
theorem Th39:
for
C1,
C2 being
Coherence_Space for
X being
Subset of 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
theorem
theorem Th41:
theorem
theorem Th43:
theorem
theorem Th45:
theorem Th46:
:: deftheorem Def19 defines StabCoh COHSP_1:def 19 :
theorem Th47:
theorem
theorem Th49:
begin
theorem Th50:
definition
let f be
Function;
func LinTrace f -> set means :
Def20:
for
x being
set holds
(
x in it iff ex
y,
z being
set st
(
x = [y,z] &
[{y},z] in Trace f ) );
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) ) ) & ( for x being set holds
( x in b2 iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) ) ) holds
b1 = b2
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) )
end;
:: deftheorem Def20 defines LinTrace COHSP_1:def 20 :
theorem Th51:
theorem Th52:
theorem Th53:
:: deftheorem Def21 defines LinCoh COHSP_1:def 21 :
theorem Th54:
theorem Th55:
theorem Th56:
Lm6:
for C1, C2 being Coherence_Space
for X being Subset of 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 ) )
theorem Th57:
for
C1,
C2 being
Coherence_Space for
X being
Subset of 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
theorem
theorem
theorem Th60:
theorem
theorem Th62:
theorem Th63:
theorem
theorem
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 ) ) ) ) )
begin
:: deftheorem defines 'not' COHSP_1:def 22 :
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem
Lm7:
for C being Coherence_Space holds 'not' ('not' C) c= C
theorem Th71:
theorem
theorem
begin
:: deftheorem defines U+ COHSP_1:def 23 :
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
for
x,
y,
z being
set holds
(
[z,1] in x U+ y iff
z in x )
theorem Th78:
for
x,
y,
z being
set holds
(
[z,2] in x U+ y iff
z in y )
theorem Th79:
for
x1,
y1,
x2,
y2 being
set holds
(
x1 U+ y1 c= x2 U+ y2 iff (
x1 c= x2 &
y1 c= y2 ) )
theorem Th80:
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 )
theorem Th81:
for
x1,
y1,
x2,
y2 being
set holds
(
x1 U+ y1 = x2 U+ y2 iff (
x1 = x2 &
y1 = y2 ) )
theorem Th82:
for
x1,
y1,
x2,
y2 being
set holds
(x1 U+ y1) \/ (x2 U+ y2) = (x1 \/ x2) U+ (y1 \/ y2)
theorem Th83:
for
x1,
y1,
x2,
y2 being
set holds
(x1 U+ y1) /\ (x2 U+ y2) = (x1 /\ x2) U+ (y1 /\ y2)
:: deftheorem defines "/\" COHSP_1:def 24 :
:: deftheorem defines "\/" COHSP_1:def 25 :
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines [*] COHSP_1:def 26 :
theorem Th97:
theorem Th98:
theorem
theorem