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;
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
begin
begin
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) ) )
theorem
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
begin
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) ) )
theorem Th38:
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
begin
definition
let f be
Function;
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;
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 ) )
theorem Th56:
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
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
Lm7:
for C being Coherence_Space holds 'not' ('not' C) c= C
begin
theorem Th76:
for
x,
y,
z being
set holds
(
[z,1] in x U+ y iff
z in x )
theorem Th77:
for
x,
y,
z being
set holds
(
[z,2] in x U+ y iff
z in y )
theorem Th78:
for
x1,
y1,
x2,
y2 being
set holds
(
x1 U+ y1 c= x2 U+ y2 iff (
x1 c= x2 &
y1 c= y2 ) )
theorem Th79:
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 Th80:
for
x1,
y1,
x2,
y2 being
set holds
(
x1 U+ y1 = x2 U+ y2 iff (
x1 = x2 &
y1 = y2 ) )
theorem Th81:
for
x1,
y1,
x2,
y2 being
set holds
(x1 U+ y1) \/ (x2 U+ y2) = (x1 \/ x2) U+ (y1 \/ y2)
theorem Th82:
for
x1,
y1,
x2,
y2 being
set holds
(x1 U+ y1) /\ (x2 U+ y2) = (x1 /\ x2) U+ (y1 /\ y2)
:: cluster union-distributive cap-distributive Function;
::end;