cohsp_1.miz
begin
Lm1: for X,Y be non
empty
set holds for f be
Function of X, Y holds for x be
Element of X holds for y be
set st y
in (f
. x) holds y
in (
union Y) by
TARSKI:def 4;
definition
let X be
set;
:: original:
binary_complete
redefine
::
COHSP_1:def1
attr X is
binary_complete means
:
Def1: for A be
set st for a,b be
set st a
in A & b
in A holds (a
\/ b)
in X holds (
union A)
in X;
compatibility
proof
thus X is
binary_complete implies for A be
set st for a,b be
set st a
in A & b
in A holds (a
\/ b)
in X holds (
union A)
in X
proof
assume
A1: for A be
set st A
c= X & for a,b be
set st a
in A & b
in A holds (a
\/ b)
in X holds (
union A)
in X;
let A be
set;
assume
A2: for a,b be
set st a
in A & b
in A holds (a
\/ b)
in X;
A
c= X
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in A;
then (xx
\/ xx)
in X by
A2;
hence thesis;
end;
hence thesis by
A1,
A2;
end;
assume for A be
set st for a,b be
set st a
in A & b
in A holds (a
\/ b)
in X holds (
union A)
in X;
hence for A be
set st A
c= X & for a,b be
set st a
in A & b
in A holds (a
\/ b)
in X holds (
union A)
in X;
end;
end
registration
cluster
finite for
Coherence_Space;
existence by
COH_SP: 3;
end
definition
let X be
set;
::
COHSP_1:def2
func
FlatCoh X ->
set equals (
CohSp (
id X));
correctness ;
::
COHSP_1:def3
func
Sub_of_Fin X ->
Subset of X means
:
Def3: for x be
set holds x
in it iff x
in X & x is
finite;
existence
proof
defpred
P[
set] means $1 is
finite;
thus ex W be
Subset of X st for x be
set holds x
in W iff x
in X &
P[x] from
SUBSET_1:sch 1;
end;
correctness
proof
let X1,X2 be
Subset of X;
assume
A1: not thesis;
then
consider x be
object such that
A2: not (x
in X1 iff x
in X2) by
TARSKI: 2;
reconsider x as
set by
TARSKI: 1;
x
in X2 iff not (x
in X & x is
finite) by
A1,
A2;
hence thesis by
A1;
end;
end
theorem ::
COHSP_1:1
Th1: for X,x be
set holds x
in (
FlatCoh X) iff x
=
{} or ex y be
set st x
=
{y} & y
in X
proof
let X,x be
set;
hereby
assume
A1: x
in (
FlatCoh X);
assume x
<>
{} ;
then
reconsider y = x as non
empty
set;
set z = the
Element of y;
reconsider z as
set;
take z;
thus x
=
{z}
proof
hereby
let c be
object;
assume c
in x;
then
[z, c]
in (
id X) by
A1,
COH_SP:def 3;
then c
= z by
RELAT_1:def 10;
hence c
in
{z} by
TARSKI:def 1;
end;
thus thesis by
ZFMISC_1: 31;
end;
[z, z]
in (
id X) by
A1,
COH_SP:def 3;
hence z
in X by
RELAT_1:def 10;
end;
A2:
now
given a be
set such that
A3: x
=
{a} and
A4: a
in X;
let y,z be
set;
assume y
in x & z
in x;
then y
= a & z
= a by
A3,
TARSKI:def 1;
hence
[y, z]
in (
id X) by
A4,
RELAT_1:def 10;
end;
assume x
=
{} or ex y be
set st x
=
{y} & y
in X;
hence thesis by
A2,
COH_SP: 1,
COH_SP:def 3;
end;
theorem ::
COHSP_1:2
Th2: for X be
set holds (
union (
FlatCoh X))
= X
proof
let X be
set;
hereby
let x be
object;
assume x
in (
union (
FlatCoh X));
then
consider y be
set such that
A1: x
in y and
A2: y
in (
FlatCoh X) by
TARSKI:def 4;
ex z be
set st y
=
{z} & z
in X by
A1,
A2,
Th1;
hence x
in X by
A1,
TARSKI:def 1;
end;
let x be
object;
assume x
in X;
then x
in
{x} &
{x}
in (
FlatCoh X) by
Th1,
TARSKI:def 1;
hence thesis by
TARSKI:def 4;
end;
theorem ::
COHSP_1:3
for X be
finite
subset-closed
set holds (
Sub_of_Fin X)
= X
proof
let X be
finite
subset-closed
set;
thus (
Sub_of_Fin X)
c= X;
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume
A1: x
in X;
(
bool xx)
c= X by
A1,
CLASSES1:def 1;
then xx is
finite;
hence thesis by
A1,
Def3;
end;
registration
cluster
{
{} } ->
subset-closed
binary_complete;
coherence by
COH_SP: 3;
let X be
set;
cluster (
bool X) ->
subset-closed
binary_complete;
coherence by
COH_SP: 2;
cluster (
FlatCoh X) -> non
empty
subset-closed
binary_complete;
coherence ;
end
registration
let C be non
empty
subset-closed
set;
cluster (
Sub_of_Fin C) -> non
empty
subset-closed;
coherence
proof
set c = the
Element of C;
{}
c= c;
then
{}
in C by
CLASSES1:def 1;
hence (
Sub_of_Fin C) is non
empty by
Def3;
let a,b be
set;
assume
A1: a
in (
Sub_of_Fin C);
then
A2: a is
finite by
Def3;
assume
A3: b
c= a;
then b
in C by
A1,
CLASSES1:def 1;
hence thesis by
A2,
A3,
Def3;
end;
end
theorem ::
COHSP_1:4
(
Web
{
{} })
=
{}
proof
(
union
{
{} })
=
{} by
ZFMISC_1: 25;
hence thesis;
end;
scheme ::
COHSP_1:sch1
MinimalElementwrtIncl { a,A() ->
set , P[
set] } :
ex a be
set st a
in A() & P[a] & for b be
set st b
in A() & P[b] & b
c= a holds b
= a
provided
A1: a()
in A() & P[a()]
and
A2: a() is
finite;
reconsider a = a() as
finite
set by
A2;
defpred
p[
set] means $1
c= a() & P[$1];
consider X be
set such that
A3: for x be
set holds x
in X iff x
in A() &
p[x] from
XFAMILY:sch 1;
A4: (
bool a) is
finite & X
c= (
bool a)
proof
thus (
bool a) is
finite;
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in X;
then xx
c= a by
A3;
hence thesis;
end;
defpred
P[
set,
set] means $1
c= $2;
A5: for x,y be
set st
P[x, y] &
P[y, x] holds x
= y;
A6: for x,y,z be
set st
P[x, y] &
P[y, z] holds
P[x, z] by
XBOOLE_1: 1;
reconsider X as
finite
set by
A4;
A7: X
<>
{} by
A1,
A3;
consider x be
set such that
A8: x
in X & for y be
set st y
in X & y
<> x holds not
P[y, x] from
CARD_2:sch 3(
A7,
A5,
A6);
take x;
thus x
in A() & P[x] by
A3,
A8;
let b be
set;
assume that
A9: b
in A() & P[b] and
A10: b
c= x;
x
c= a by
A3,
A8;
then b
c= a by
A10;
then b
in X by
A3,
A9;
hence thesis by
A8,
A10;
end;
registration
let C be
Coherence_Space;
cluster
finite for
Element of C;
existence
proof
reconsider E =
{} as
Element of C by
COH_SP: 1;
take E;
thus thesis;
end;
end
definition
let X be
set;
::
COHSP_1:def4
attr X is
c=directed means for Y be
finite
Subset of X holds ex a be
set st (
union Y)
c= a & a
in X;
::
COHSP_1:def5
attr X is
c=filtered means for Y be
finite
Subset of X holds ex a be
set st (for y be
set st y
in Y holds a
c= y) & a
in X;
end
registration
cluster
c=directed -> non
empty for
set;
coherence
proof
let X be
set;
assume for Y be
finite
Subset of X holds ex a be
set st (
union Y)
c= a & a
in X;
then ex a be
set st (
union (
{} X))
c= a & a
in X;
hence thesis;
end;
cluster
c=filtered -> non
empty for
set;
coherence
proof
let X be
set;
assume for Y be
finite
Subset of X holds ex a be
set st (for y be
set st y
in Y holds a
c= y) & a
in X;
then ex a be
set st (for y be
set st y
in (
{} X) holds a
c= y) & a
in X;
hence thesis;
end;
end
theorem ::
COHSP_1:5
Th5: for X be
set st X is
c=directed holds for a,b be
set st a
in X & b
in X holds ex c be
set st (a
\/ b)
c= c & c
in X
proof
let X be
set;
assume
A1: for Y be
finite
Subset of X holds ex a be
set st (
union Y)
c= a & a
in X;
let a,b be
set;
assume a
in X & b
in X;
then
A2:
{a, b} is
finite
Subset of X by
ZFMISC_1: 32;
(
union
{a, b})
= (a
\/ b) by
ZFMISC_1: 75;
hence thesis by
A1,
A2;
end;
theorem ::
COHSP_1:6
Th6: for X be non
empty
set st for a,b be
set st a
in X & b
in X holds ex c be
set st (a
\/ b)
c= c & c
in X holds X is
c=directed
proof
let X be non
empty
set such that
A1: for a,b be
set st a
in X & b
in X holds ex c be
set st (a
\/ b)
c= c & c
in X;
set a = the
Element of X;
defpred
P[
set] means ex a be
set st (
union $1)
c= a & a
in X;
let Y be
finite
Subset of X;
A2:
now
let x,B be
set;
assume that
A3: x
in Y and B
c= Y;
assume
P[B];
then
consider a be
set such that
A4: (
union B)
c= a and
A5: a
in X;
consider c be
set such that
A6: (a
\/ x)
c= c & c
in X by
A1,
A3,
A5;
thus
P[(B
\/
{x})]
proof
take c;
(
union (B
\/
{x}))
= ((
union B)
\/ (
union
{x})) by
ZFMISC_1: 78
.= ((
union B)
\/ x) by
ZFMISC_1: 25;
then (
union (B
\/
{x}))
c= (a
\/ x) by
A4,
XBOOLE_1: 9;
hence thesis by
A6;
end;
end;
(
union
{} )
c= a by
ZFMISC_1: 2;
then
A7:
P[
{} ];
A8: Y is
finite;
thus
P[Y] from
FINSET_1:sch 2(
A8,
A7,
A2);
end;
theorem ::
COHSP_1:7
for X be
set st X is
c=filtered holds for a,b be
set st a
in X & b
in X holds ex c be
set st c
c= (a
/\ b) & c
in X
proof
let X be
set;
assume
A1: for Y be
finite
Subset of X holds ex a be
set st (for y be
set st y
in Y holds a
c= y) & a
in X;
let a,b be
set;
assume a
in X & b
in X;
then
{a, b}
c= X by
ZFMISC_1: 32;
then
consider c be
set such that
A2: for y be
set st y
in
{a, b} holds c
c= y and
A3: c
in X by
A1;
take c;
b
in
{a, b} by
TARSKI:def 2;
then
A4: c
c= b by
A2;
a
in
{a, b} by
TARSKI:def 2;
then c
c= a by
A2;
hence thesis by
A3,
A4,
XBOOLE_1: 19;
end;
theorem ::
COHSP_1:8
Th8: for X be non
empty
set st for a,b be
set st a
in X & b
in X holds ex c be
set st c
c= (a
/\ b) & c
in X holds X is
c=filtered
proof
let X be non
empty
set such that
A1: for a,b be
set st a
in X & b
in X holds ex c be
set st c
c= (a
/\ b) & c
in X;
set a = the
Element of X;
defpred
P[
set] means ex a be
set st (for y be
set st y
in $1 holds a
c= y) & a
in X;
let Y be
finite
Subset of X;
A2:
now
let x,B be
set;
assume that
A3: x
in Y and B
c= Y;
assume
P[B];
then
consider a be
set such that
A4: for y be
set st y
in B holds a
c= y and
A5: a
in X;
consider c be
set such that
A6: c
c= (a
/\ x) and
A7: c
in X by
A1,
A3,
A5;
A8: (a
/\ x)
c= a & (a
/\ x)
c= x by
XBOOLE_1: 17;
thus
P[(B
\/
{x})]
proof
take c;
hereby
let y be
set;
assume y
in (B
\/
{x});
then y
in B or y
in
{x} by
XBOOLE_0:def 3;
then a
c= y & c
c= a or y
= x & c
c= x by
A4,
A6,
A8,
TARSKI:def 1;
hence c
c= y;
end;
thus thesis by
A7;
end;
end;
for y be
set st y
in
{} holds a
c= y;
then
A9:
P[
{} ];
A10: Y is
finite;
thus
P[Y] from
FINSET_1:sch 2(
A10,
A9,
A2);
end;
theorem ::
COHSP_1:9
Th9: for x be
set holds
{x} is
c=directed
c=filtered
proof
let x be
set;
set X =
{x};
hereby
let Y be
finite
Subset of X;
take x;
(
union Y)
c= (
union X) by
ZFMISC_1: 77;
hence (
union Y)
c= x & x
in X by
TARSKI:def 1,
ZFMISC_1: 25;
end;
let Y be
finite
Subset of X;
take x;
thus for y be
set st y
in Y holds x
c= y by
TARSKI:def 1;
thus thesis by
TARSKI:def 1;
end;
Lm2:
now
let x,y be
set;
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);
end;
theorem ::
COHSP_1:10
for x,y be
set holds
{x, y, (x
\/ y)} is
c=directed
proof
let x,y be
set;
set X =
{x, y, (x
\/ y)};
let A be
finite
Subset of X;
take a = (x
\/ y);
(
union X)
= a by
Lm2;
hence (
union A)
c= a by
ZFMISC_1: 77;
thus thesis by
ENUMSET1:def 1;
end;
theorem ::
COHSP_1:11
for x,y be
set holds
{x, y, (x
/\ y)} is
c=filtered
proof
let x,y be
set;
let A be
finite
Subset of
{x, y, (x
/\ y)};
take a = (x
/\ y);
hereby
let b be
set;
assume b
in A;
then b
= x or b
= y or b
= (x
/\ y) by
ENUMSET1:def 1;
hence a
c= b by
XBOOLE_1: 17;
end;
thus thesis by
ENUMSET1:def 1;
end;
registration
cluster
c=directed
c=filtered
finite for
set;
existence
proof
take
{
{} };
thus thesis by
Th9;
end;
end
registration
let C be non
empty
set;
cluster
c=directed
c=filtered
finite for
Subset of C;
existence
proof
set x = the
Element of C;
{x} is
Subset of C &
{x} is
c=directed
c=filtered
finite by
Th9,
ZFMISC_1: 31;
hence thesis;
end;
end
theorem ::
COHSP_1:12
Th12: for X be
set holds (
Fin X) is
c=directed
c=filtered
proof
let X be
set;
now
let a,b be
set;
assume
A1: a
in (
Fin X) & b
in (
Fin X);
take c = (a
\/ b);
thus (a
\/ b)
c= c;
a
c= X & b
c= X by
A1,
FINSUB_1:def 5;
then (a
\/ b)
c= X by
XBOOLE_1: 8;
hence c
in (
Fin X) by
A1,
FINSUB_1:def 5;
end;
hence (
Fin X) is
c=directed by
Th6;
now
reconsider c =
{} as
set;
let a,b be
set;
assume that a
in (
Fin X) and b
in (
Fin X);
take c;
thus c
c= (a
/\ b);
thus c
in (
Fin X) by
FINSUB_1: 7;
end;
hence thesis by
Th8;
end;
registration
let X be
set;
cluster (
Fin X) ->
c=directed
c=filtered;
coherence by
Th12;
end
Lm3:
now
let C be
subset-closed non
empty
set;
let a be
Element of C;
thus (
Fin a)
c= C
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
Fin a);
then xx
c= a by
FINSUB_1:def 5;
hence thesis by
CLASSES1:def 1;
end;
end;
registration
let C be
subset-closed non
empty
set;
cluster
preBoolean non
empty for
Subset of C;
existence
proof
set a = the
Element of C;
reconsider b = (
Fin a) as
Subset of C by
Lm3;
take b;
thus thesis;
end;
end
definition
let C be
subset-closed non
empty
set;
let a be
Element of C;
:: original:
Fin
redefine
func
Fin a ->
preBoolean non
empty
Subset of C ;
coherence
proof
(
Fin a)
c= C
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
Fin a);
then xx
c= a by
FINSUB_1:def 5;
hence thesis by
CLASSES1:def 1;
end;
hence thesis;
end;
end
theorem ::
COHSP_1:13
Th13: for X be non
empty
set, Y be
set st X is
c=directed & Y
c= (
union X) & Y is
finite holds ex Z be
set st Z
in X & Y
c= Z
proof
let X be non
empty
set, Y be
set;
set x = the
Element of X;
defpred
P[
Nat] means for Y be
set st Y
c= (
union X) & Y is
finite & (
card Y)
= $1 holds ex Z be
set st Z
in X & Y
c= Z;
assume
A1: X is
c=directed;
A2:
now
let n be
Nat;
assume
A3:
P[n];
thus
P[(n
+ 1)]
proof
let Y be
set;
assume that
A4: Y
c= (
union X) and
A5: Y is
finite and
A6: (
card Y)
= (n
+ 1);
reconsider Y9 = Y as non
empty
set by
A6;
set y = the
Element of Y9;
A7: (Y
\
{y})
c= (
union X) by
A4;
y
in Y;
then
consider Z9 be
set such that
A8: y
in Z9 and
A9: Z9
in X by
A4,
TARSKI:def 4;
A10: ((n
+ 1)
- 1)
= n by
XCMPLX_1: 26;
{y}
c= Y & (
card
{y})
= 1 by
CARD_1: 30,
ZFMISC_1: 31;
then (
card (Y
\
{y}))
= n by
A5,
A6,
A10,
CARD_2: 44;
then
consider Z be
set such that
A11: Z
in X and
A12: (Y
\
{y})
c= Z by
A3,
A5,
A7;
consider V be
set such that
A13: (Z
\/ Z9)
c= V and
A14: V
in X by
A1,
A11,
A9,
Th5;
take V;
thus V
in X by
A14;
thus Y
c= V
proof
let x be
object;
A15: x
in
{y} or not x
in
{y};
assume x
in Y;
then x
= y or x
in (Y
\
{y}) by
A15,
TARSKI:def 1,
XBOOLE_0:def 5;
then x
in (Z
\/ Z9) by
A12,
A8,
XBOOLE_0:def 3;
hence thesis by
A13;
end;
end;
end;
A16:
P[
0 ]
proof
let Y be
set;
assume that Y
c= (
union X) and Y is
finite and
A17: (
card Y)
=
0 ;
Y
=
{} by
A17;
then Y
c= x;
hence thesis;
end;
A18: for n be
Nat holds
P[n] from
NAT_1:sch 2(
A16,
A2);
assume that
A19: Y
c= (
union X) and
A20: Y is
finite;
reconsider Y9 = Y as
finite
set by
A20;
(
card Y)
= (
card Y9);
hence thesis by
A18,
A19;
end;
notation
let X be
set;
synonym X is
multiplicative for X is
cap-closed;
end
definition
let X be
set;
::
COHSP_1:def6
attr X is
d.union-closed means
:
Def6: for A be
Subset of X st A is
c=directed holds (
union A)
in X;
end
registration
cluster
subset-closed ->
multiplicative for
set;
coherence
proof
let C be
set such that
A1: C is
subset-closed;
let x,y be
set;
(x
/\ y)
c= x by
XBOOLE_1: 17;
hence thesis by
A1;
end;
end
theorem ::
COHSP_1:14
Th14: for C be
Coherence_Space, A be
c=directed
Subset of C holds (
union A)
in C
proof
let C be
Coherence_Space, A be
c=directed
Subset of C;
now
let a,b be
set;
assume a
in A & b
in A;
then ex c be
set st (a
\/ b)
c= c & c
in A by
Th5;
hence (a
\/ b)
in C by
CLASSES1:def 1;
end;
hence thesis by
Def1;
end;
registration
cluster ->
d.union-closed for
Coherence_Space;
coherence by
Th14;
end
registration
cluster
multiplicative
d.union-closed for
Coherence_Space;
existence
proof
set C = the
Coherence_Space;
take C;
thus thesis;
end;
end
definition
let C be
d.union-closed non
empty
set, A be
c=directed
Subset of C;
:: original:
union
redefine
func
union A ->
Element of C ;
coherence by
Def6;
end
definition
let X,Y be
set;
::
COHSP_1:def7
pred X
includes_lattice_of Y means for a,b be
set st a
in Y & b
in Y holds (a
/\ b)
in X & (a
\/ b)
in X;
end
theorem ::
COHSP_1:15
for X be non
empty
set st X
includes_lattice_of X holds X is
c=directed
c=filtered
proof
let X be non
empty
set such that
A1: for a,b be
set st a
in X & b
in X holds (a
/\ b)
in X & (a
\/ b)
in X;
for a,b be
set st a
in X & b
in X holds ex c be
set st (a
\/ b)
c= c & c
in X by
A1;
hence X is
c=directed by
Th6;
for a,b be
set st a
in X & b
in X holds ex c be
set st c
c= (a
/\ b) & c
in X by
A1;
hence thesis by
Th8;
end;
definition
let X,x,y be
set;
::
COHSP_1:def8
pred X
includes_lattice_of x,y means X
includes_lattice_of
{x, y};
end
theorem ::
COHSP_1:16
Th16: for X,x,y be
set holds X
includes_lattice_of (x,y) iff x
in X & y
in X & (x
/\ y)
in X & (x
\/ y)
in X
proof
let X,x,y be
set;
thus X
includes_lattice_of (x,y) implies x
in X & y
in X & (x
/\ y)
in X & (x
\/ y)
in X
proof
A1: (x
\/ x)
= x & (y
\/ y)
= y;
A2: x
in
{x, y} & y
in
{x, y} by
TARSKI:def 2;
assume for a,b be
set st a
in
{x, y} & b
in
{x, y} holds (a
/\ b)
in X & (a
\/ b)
in X;
hence thesis by
A2,
A1;
end;
assume
A3: x
in X & y
in X & (x
/\ y)
in X & (x
\/ y)
in X;
let a,b be
set;
assume that
A4: a
in
{x, y} and
A5: b
in
{x, y};
A6: b
= x or b
= y by
A5,
TARSKI:def 2;
a
= x or a
= y by
A4,
TARSKI:def 2;
hence thesis by
A3,
A6;
end;
begin
definition
let f be
Function;
::
COHSP_1:def9
attr f is
union-distributive means
:
Def9: for A be
Subset of (
dom f) st (
union A)
in (
dom f) holds (f
. (
union A))
= (
union (f
.: A));
::
COHSP_1:def10
attr f is
d.union-distributive means
:
Def10: for A be
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;
::
COHSP_1:def11
attr f is
c=-monotone means
:
Def11: for a,b be
set st a
in (
dom f) & b
in (
dom f) & a
c= b holds (f
. a)
c= (f
. b);
::
COHSP_1:def12
attr f is
cap-distributive means
:
Def12: for a,b be
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;
coherence
proof
let f be
Function;
assume
A1: for A be
Subset of (
dom f) st A is
c=directed & (
union A)
in (
dom f) holds (f
. (
union A))
= (
union (f
.: A));
let a,b be
set;
assume that
A2: a
in (
dom f) and
A3: b
in (
dom f) and
A4: a
c= b;
reconsider A =
{a, b} as
Subset of (
dom f) by
A2,
A3,
ZFMISC_1: 32;
A5: A is
c=directed
proof
let Y be
finite
Subset of A;
take b;
(
union Y)
c= (
union A) by
ZFMISC_1: 77;
then (
union Y)
c= (a
\/ b) by
ZFMISC_1: 75;
hence thesis by
A4,
TARSKI:def 2,
XBOOLE_1: 12;
end;
a
in A by
TARSKI:def 2;
then
A6: (f
. a)
in (f
.: A) by
FUNCT_1:def 6;
(
union A)
= (a
\/ b) by
ZFMISC_1: 75
.= b by
A4,
XBOOLE_1: 12;
then (
union (f
.: A))
= (f
. b) by
A1,
A3,
A5;
hence thesis by
A6,
ZFMISC_1: 74;
end;
cluster
union-distributive ->
d.union-distributive for
Function;
coherence ;
end
theorem ::
COHSP_1:17
for f be
Function st f is
union-distributive holds for x,y be
set st x
in (
dom f) & y
in (
dom f) & (x
\/ y)
in (
dom f) holds (f
. (x
\/ y))
= ((f
. x)
\/ (f
. y))
proof
let f be
Function such that
A1: f is
union-distributive;
let x,y be
set;
set X =
{x, y};
assume that
A2: x
in (
dom f) & y
in (
dom f) and
A3: (x
\/ y)
in (
dom f);
A4: (
union X)
= (x
\/ y) by
ZFMISC_1: 75;
X
c= (
dom f) by
A2,
ZFMISC_1: 32;
hence (f
. (x
\/ y))
= (
union (f
.: X)) by
A1,
A3,
A4
.= (
union
{(f
. x), (f
. y)}) by
A2,
FUNCT_1: 60
.= ((f
. x)
\/ (f
. y)) by
ZFMISC_1: 75;
end;
theorem ::
COHSP_1:18
Th18: for f be
Function st f is
union-distributive holds (f
.
{} )
=
{}
proof
let f be
Function such that
A1: for A be
Subset of (
dom f) st (
union A)
in (
dom f) holds (f
. (
union A))
= (
union (f
.: A));
A2:
{}
c= (
dom f) & (f
.:
{} )
=
{} ;
not
{}
in (
dom f) implies (f
.
{} )
=
{} by
FUNCT_1:def 2;
hence thesis by
A1,
A2,
ZFMISC_1: 2;
end;
registration
let C1,C2 be
Coherence_Space;
cluster
union-distributive
cap-distributive for
Function of C1, C2;
existence
proof
reconsider a =
{} as
Element of C2 by
COH_SP: 1;
take f = (C1
--> a);
A1: (
dom f)
= C1 by
FUNCOP_1: 13;
thus f is
union-distributive
proof
let A be
Subset of (
dom f);
assume (
union A)
in (
dom f);
then
A2: (f
. (
union A))
=
{} by
A1,
FUNCOP_1: 7;
(f
.: A)
c=
{
{} }
proof
let x be
object;
assume x
in (f
.: A);
then ex y be
object st y
in (
dom f) & y
in A & x
= (f
. y) by
FUNCT_1:def 6;
then x
=
{} by
A1,
FUNCOP_1: 7;
hence thesis by
TARSKI:def 1;
end;
then
A3: (
union (f
.: A))
c= (
union
{
{} }) by
ZFMISC_1: 77;
(
union
{
{} })
=
{} by
ZFMISC_1: 25;
hence thesis by
A2,
A3;
end;
let a,b be
set;
assume
A4: (
dom f)
includes_lattice_of (a,b);
then a
in (
dom f) by
Th16;
then
A5: (f
. a)
=
{} by
A1,
FUNCOP_1: 7;
(a
/\ b)
in (
dom f) by
A4,
Th16;
hence thesis by
A1,
A5,
FUNCOP_1: 7;
end;
end
registration
let C be
Coherence_Space;
cluster
union-distributive
cap-distributive for
ManySortedSet of C;
existence
proof
set f = the
union-distributive
cap-distributive
Function of C, C;
(
dom f)
= C by
FUNCT_2: 52;
then
reconsider f as
ManySortedSet of C by
PARTFUN1:def 2;
take f;
thus thesis;
end;
end
definition
let f be
Function;
::
COHSP_1:def13
attr f is
U-continuous means
:
Def13: (
dom f) is
d.union-closed & f is
d.union-distributive;
end
definition
let f be
Function;
::
COHSP_1:def14
attr f is
U-stable means
:
Def14: (
dom f) is
multiplicative & f is
U-continuous
cap-distributive;
end
definition
let f be
Function;
::
COHSP_1:def15
attr f is
U-linear means f is
U-stable
union-distributive;
end
registration
cluster
U-continuous ->
d.union-distributive for
Function;
coherence ;
cluster
U-stable ->
cap-distributive
U-continuous for
Function;
coherence ;
cluster
U-linear ->
union-distributive
U-stable for
Function;
coherence ;
end
registration
let X be
d.union-closed
set;
cluster
d.union-distributive ->
U-continuous for
ManySortedSet of X;
coherence by
PARTFUN1:def 2;
end
registration
let X be
multiplicative
set;
cluster
U-continuous
cap-distributive ->
U-stable for
ManySortedSet of X;
coherence by
PARTFUN1:def 2;
end
registration
cluster
U-stable
union-distributive ->
U-linear for
Function;
coherence ;
end
registration
cluster
U-linear for
Function;
existence
proof
set C = the
Coherence_Space;
set f = the
union-distributive
cap-distributive
ManySortedSet of C;
take f;
thus thesis;
end;
let C be
Coherence_Space;
cluster
U-linear for
ManySortedSet of C;
existence
proof
set f = the
union-distributive
cap-distributive
ManySortedSet of C;
take f;
thus thesis;
end;
let B be
Coherence_Space;
cluster
U-linear for
Function of B, C;
existence
proof
set f = the
union-distributive
cap-distributive
Function of B, C;
take f;
(
dom f)
= B by
FUNCT_2:def 1;
then
reconsider f as
union-distributive
cap-distributive
ManySortedSet of B by
PARTFUN1:def 2;
f is
U-linear;
hence thesis;
end;
end
registration
let f be
U-continuous
Function;
cluster (
dom f) ->
d.union-closed;
coherence by
Def13;
end
registration
let f be
U-stable
Function;
cluster (
dom f) ->
multiplicative;
coherence by
Def14;
end
theorem ::
COHSP_1:19
Th19: for X be
set holds (
union (
Fin X))
= X
proof
let X be
set;
(
union (
Fin X))
c= (
union (
bool X)) by
FINSUB_1: 13,
ZFMISC_1: 77;
hence (
union (
Fin X))
c= X by
ZFMISC_1: 81;
let x be
object;
assume x
in X;
then
{x}
c= X by
ZFMISC_1: 31;
then
A1:
{x}
in (
Fin X) by
FINSUB_1:def 5;
x
in
{x} by
TARSKI:def 1;
hence thesis by
A1,
TARSKI:def 4;
end;
theorem ::
COHSP_1:20
Th20: for f be
U-continuous
Function st (
dom f) is
subset-closed holds for a be
set st a
in (
dom f) holds (f
. a)
= (
union (f
.: (
Fin a)))
proof
let f be
U-continuous
Function such that
A1: (
dom f) is
subset-closed;
let a be
set;
assume
A2: a
in (
dom f);
then
reconsider C = (
dom f) as
d.union-closed
subset-closed non
empty
set by
A1;
reconsider a as
Element of C by
A2;
(f
. a)
= (f
. (
union (
Fin a))) by
Th19;
hence thesis by
Def10;
end;
theorem ::
COHSP_1:21
Th21: for f be
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 be
set st a
in (
dom f) & y
in (f
. a) holds ex b be
set st b is
finite & b
c= a & y
in (f
. b)
proof
let f be
Function such that
A1: (
dom f) is
subset-closed;
hereby
assume
A2: f is
U-continuous;
hence (
dom f) is
d.union-closed & f is
c=-monotone;
reconsider C = (
dom f) as
d.union-closed
subset-closed
set by
A1,
A2;
let a,y be
set;
assume that
A3: a
in (
dom f) and
A4: y
in (f
. a);
reconsider A = { b where b be
Subset of a : b is
finite } as
set;
A5: A is
c=directed
proof
let Y be
finite
Subset of A;
take (
union Y);
now
let x be
set;
assume x
in Y;
then x
in A;
then ex c be
Subset of a st x
= c & c is
finite;
hence x
c= a;
end;
then
A6: (
union Y)
c= a by
ZFMISC_1: 76;
now
let b be
set;
assume b
in Y;
then b
in A;
then ex c be
Subset of a st b
= c & c is
finite;
hence b is
finite;
end;
then (
union Y) is
finite by
FINSET_1: 7;
hence thesis by
A6;
end;
A7: (
union A)
= a
proof
thus (
union A)
c= a
proof
let x be
object;
assume x
in (
union A);
then
consider b be
set such that
A8: x
in b and
A9: b
in A by
TARSKI:def 4;
ex c be
Subset of a st b
= c & c is
finite by
A9;
hence thesis by
A8;
end;
let x be
object;
assume x
in a;
then
{x}
c= a by
ZFMISC_1: 31;
then x
in
{x} &
{x}
in A by
TARSKI:def 1;
hence thesis by
TARSKI:def 4;
end;
A10: A
c= C
proof
let x be
object;
assume x
in A;
then ex b be
Subset of a st x
= b & b is
finite;
hence thesis by
A3,
CLASSES1:def 1;
end;
then (
union A)
in C by
A5,
Def6;
then (f
. (
union A))
= (
union (f
.: A)) by
A2,
A5,
A10,
Def10;
then
consider B be
set such that
A11: y
in B and
A12: B
in (f
.: A) by
A4,
A7,
TARSKI:def 4;
consider b be
object such that b
in (
dom f) and
A13: b
in A and
A14: B
= (f
. b) by
A12,
FUNCT_1:def 6;
reconsider bb = b as
set by
TARSKI: 1;
take bb;
ex c be
Subset of a st b
= c & c is
finite by
A13;
hence bb is
finite & bb
c= a & y
in (f
. bb) by
A11,
A14;
end;
assume (
dom f) is
d.union-closed;
then
reconsider C = (
dom f) as
d.union-closed
set;
assume that
A15: for a,b be
set st a
in (
dom f) & b
in (
dom f) & a
c= b holds (f
. a)
c= (f
. b) and
A16: for a,y be
set st a
in (
dom f) & y
in (f
. a) holds ex b be
set st b is
finite & b
c= a & y
in (f
. b);
C is
d.union-closed;
hence (
dom f) is
d.union-closed;
thus f is
d.union-distributive
proof
let A be
Subset of (
dom f);
assume that
A17: A is
c=directed and
A18: (
union A)
in (
dom f);
reconsider A9 = A as
Subset of C;
thus (f
. (
union A))
c= (
union (f
.: A))
proof
let x be
object;
assume x
in (f
. (
union A));
then
consider b be
set such that
A19: b is
finite & b
c= (
union A9) and
A20: x
in (f
. b) by
A16,
A18;
consider c be
set such that
A21: c
in A and
A22: b
c= c by
A17,
A19,
Th13;
b
in C by
A1,
A21,
A22;
then
A23: (f
. b)
c= (f
. c) by
A15,
A21,
A22;
(f
. c)
in (f
.: A) by
A21,
FUNCT_1:def 6;
hence thesis by
A20,
A23,
TARSKI:def 4;
end;
let x be
object;
assume x
in (
union (f
.: A));
then
consider B be
set such that
A24: x
in B and
A25: B
in (f
.: A) by
TARSKI:def 4;
ex b be
object st b
in (
dom f) & b
in A & B
= (f
. b) by
A25,
FUNCT_1:def 6;
then B
c= (f
. (
union A9)) by
A15,
A18,
ZFMISC_1: 74;
hence thesis by
A24;
end;
end;
theorem ::
COHSP_1:22
Th22: for f be
Function st (
dom f) is
subset-closed
d.union-closed holds f is
U-stable iff f is
c=-monotone & for a,y be
set st a
in (
dom f) & y
in (f
. a) holds ex b be
set st b is
finite & b
c= a & y
in (f
. b) & for c be
set st c
c= a & y
in (f
. c) holds b
c= c
proof
let f be
Function such that
A1: (
dom f) is
subset-closed
d.union-closed;
reconsider C = (
dom f) as
subset-closed
d.union-closed
set by
A1;
hereby
assume f is
U-stable;
then
reconsider f9 = f as
U-stable
Function;
(
dom f9) is
multiplicative;
hence f is
c=-monotone;
defpred
P[
set,
set] means $1
c= $2;
let a,y be
set;
set C = (
dom f9);
assume that
A2: a
in (
dom f) and
A3: y
in (f
. a);
consider b be
set such that
A4: b is
finite and
A5: b
c= a and
A6: y
in (f9
. b) by
A1,
A2,
A3,
Th21;
b
c= b;
then b
in { c where c be
Subset of b : y
in (f
. c) } by
A6;
then
reconsider A = { c where c be
Subset of b : y
in (f
. c) } as non
empty
set;
A7: (
bool b) is
finite & A
c= (
bool b)
proof
thus (
bool b) is
finite by
A4;
let x be
object;
assume x
in A;
then ex c be
Subset of b st x
= c & y
in (f
. c);
hence thesis;
end;
A8: for x,y,z be
set st
P[x, y] &
P[y, z] holds
P[x, z] by
XBOOLE_1: 1;
A9: for x,y be
set st
P[x, y] &
P[y, x] holds x
= y;
reconsider A as
finite non
empty
set by
A7;
A10: A
<>
{} ;
consider c be
set such that
A11: c
in A & for y be
set st y
in A & y
<> c holds not
P[y, c] from
CARD_2:sch 3(
A10,
A9,
A8);
ex d be
Subset of b st c
= d & y
in (f
. d) by
A11;
then
reconsider c9 = c as
Subset of b;
reconsider c9 as
finite
Subset of b by
A4;
take c;
A12: ex d be
Subset of b st c
= d & y
in (f
. d) by
A11;
hence
A13: c is
finite & c
c= a & y
in (f
. c) by
A4,
A5;
then
A14: c9
in C by
A1,
A2;
let d be
set;
assume that
A15: d
c= a and
A16: y
in (f
. d);
A17: d
in C by
A1,
A2,
A15;
(c
\/ d)
c= a by
A13,
A15,
XBOOLE_1: 8;
then
A18: (c
\/ d)
in (
dom f) by
A1,
A2;
A19: (c
/\ d)
c= c9 by
XBOOLE_1: 17;
then (c
/\ d)
in (
dom f) by
A1,
A14;
then (
dom f)
includes_lattice_of (c,d) by
A14,
A17,
A18,
Th16;
then (f
. (c
/\ d))
= ((f
. c)
/\ (f
. d)) by
A14,
Def12;
then
A20: y
in (f
. (c
/\ d)) by
A12,
A16,
XBOOLE_0:def 4;
(c
/\ d) is
finite
Subset of b by
A19,
XBOOLE_1: 1;
then (c
/\ d)
c= d & (c
/\ d)
in A by
A20,
XBOOLE_1: 17;
hence c
c= d by
A11,
XBOOLE_1: 17;
end;
assume that
A21: f is
c=-monotone and
A22: for a,y be
set st a
in (
dom f) & y
in (f
. a) holds ex b be
set st b is
finite & b
c= a & y
in (f
. b) & for c be
set st c
c= a & y
in (f
. c) holds b
c= c;
C is
subset-closed
set;
hence (
dom f) is
multiplicative;
now
let a,y be
set;
assume a
in (
dom f) & y
in (f
. a);
then ex b be
set st b is
finite & b
c= a & y
in (f
. b) & for c be
set st c
c= a & y
in (f
. c) holds b
c= c by
A22;
hence ex b be
set st b is
finite & b
c= a & y
in (f
. b);
end;
hence f is
U-continuous by
A1,
A21,
Th21;
thus f is
cap-distributive
proof
let a,b be
set;
A23: (a
/\ b)
c= b by
XBOOLE_1: 17;
assume
A24: (
dom f)
includes_lattice_of (a,b);
then
A25: (a
/\ b)
in (
dom f) by
Th16;
b
in (
dom f) by
A24,
Th16;
then
A26: (f
. (a
/\ b))
c= (f
. b) by
A21,
A25,
A23;
A27: a
in (
dom f) by
A24,
Th16;
(a
/\ b)
c= a by
XBOOLE_1: 17;
then (f
. (a
/\ b))
c= (f
. a) by
A21,
A27,
A25;
hence (f
. (a
/\ b))
c= ((f
. a)
/\ (f
. b)) by
A26,
XBOOLE_1: 19;
let x be
object;
assume
A28: x
in ((f
. a)
/\ (f
. b));
then
A29: x
in (f
. a) by
XBOOLE_0:def 4;
A30: (a
\/ b)
in (
dom f) by
A24,
Th16;
a
c= (a
\/ b) by
XBOOLE_1: 7;
then (f
. a)
c= (f
. (a
\/ b)) by
A21,
A27,
A30;
then
consider c be
set such that c is
finite and c
c= (a
\/ b) and
A31: x
in (f
. c) and
A32: for d be
set st d
c= (a
\/ b) & x
in (f
. d) holds c
c= d by
A22,
A30,
A29;
A33: c
c= a by
A29,
A32,
XBOOLE_1: 7;
x
in (f
. b) by
A28,
XBOOLE_0:def 4;
then c
c= b by
A32,
XBOOLE_1: 7;
then
A34: c
c= (a
/\ b) by
A33,
XBOOLE_1: 19;
C
= (
dom f);
then c
in (
dom f) by
A27,
A33,
CLASSES1:def 1;
then (f
. c)
c= (f
. (a
/\ b)) by
A21,
A25,
A34;
hence thesis by
A31;
end;
end;
theorem ::
COHSP_1:23
Th23: for f be
Function st (
dom f) is
subset-closed
d.union-closed holds f is
U-linear iff f is
c=-monotone & for a,y be
set st a
in (
dom f) & y
in (f
. a) holds ex x be
set st x
in a & y
in (f
.
{x}) & for b be
set st b
c= a & y
in (f
. b) holds x
in b
proof
let f be
Function;
assume
A1: (
dom f) is
subset-closed
d.union-closed;
then
reconsider C = (
dom f) as
subset-closed
d.union-closed
set;
hereby
A2:
{} is
Subset of (
dom f) by
XBOOLE_1: 2;
assume
A3: f is
U-linear;
hence f is
c=-monotone;
let a,y be
set;
assume that
A4: a
in (
dom f) and
A5: y
in (f
. a);
consider b be
set such that b is
finite and
A6: b
c= a and
A7: y
in (f
. b) and
A8: for c be
set st c
c= a & y
in (f
. c) holds b
c= c by
A1,
A3,
A4,
A5,
Th22;
A9: (
dom f)
= C;
{}
c= a;
then
{}
in (
dom f) by
A4,
A9,
CLASSES1:def 1;
then (f
.
{} )
= (
union (f
.:
{} )) by
A3,
A2,
Def9,
ZFMISC_1: 2
.=
{} by
ZFMISC_1: 2;
then
reconsider b as non
empty
set by
A7;
reconsider A = the set of all
{x} where x be
Element of b as
set;
A10: b
in (
dom f) by
A4,
A6,
A9,
CLASSES1:def 1;
A11: A
c= (
dom f)
proof
let X be
object;
reconsider xx = X as
set by
TARSKI: 1;
assume X
in A;
then ex x be
Element of b st X
=
{x};
then xx
c= b by
ZFMISC_1: 31;
hence thesis by
A9,
A10,
CLASSES1:def 1;
end;
now
let X be
set;
assume X
in A;
then ex x be
Element of b st X
=
{x};
hence X
c= b by
ZFMISC_1: 31;
end;
then (
union A)
c= b by
ZFMISC_1: 76;
then
A12: (
union A)
in (
dom f) by
A9,
A10,
CLASSES1:def 1;
reconsider A as
Subset of (
dom f) by
A11;
b
c= (
union A)
proof
let x be
object;
assume x
in b;
then
{x}
in A;
then
{x}
c= (
union A) by
ZFMISC_1: 74;
hence thesis by
ZFMISC_1: 31;
end;
then
A13: (f
. b)
c= (f
. (
union A)) by
A3,
A10,
A12,
Def11;
(f
. (
union A))
= (
union (f
.: A)) by
A3,
A12,
Def9;
then
consider Y be
set such that
A14: y
in Y and
A15: Y
in (f
.: A) by
A7,
A13,
TARSKI:def 4;
consider X be
object such that X
in (
dom f) and
A16: X
in A and
A17: Y
= (f
. X) by
A15,
FUNCT_1:def 6;
consider x be
Element of b such that
A18: X
=
{x} by
A16;
reconsider x as
set;
take x;
thus x
in a & y
in (f
.
{x}) by
A6,
A14,
A17,
A18;
let c be
set;
assume c
c= a & y
in (f
. c);
then x
in b & b
c= c by
A8;
hence x
in c;
end;
assume that
A19: f is
c=-monotone and
A20: for a,y be
set st a
in (
dom f) & y
in (f
. a) holds ex x be
set st x
in a & y
in (f
.
{x}) & for b be
set st b
c= a & y
in (f
. b) holds x
in b;
now
let a,y be
set;
assume a
in (
dom f) & y
in (f
. a);
then
consider x be
set such that
A21: x
in a & y
in (f
.
{x}) and
A22: for b be
set st b
c= a & y
in (f
. b) holds x
in b by
A20;
reconsider b =
{x} as
set;
take b;
thus b is
finite & b
c= a & y
in (f
. b) by
A21,
ZFMISC_1: 31;
let c be
set;
assume c
c= a & y
in (f
. c);
then x
in c by
A22;
hence b
c= c by
ZFMISC_1: 31;
end;
hence f is
U-stable by
A1,
A19,
Th22;
thus f is
union-distributive
proof
let A be
Subset of (
dom f) such that
A23: (
union A)
in (
dom f);
thus (f
. (
union A))
c= (
union (f
.: A))
proof
let y be
object;
assume y
in (f
. (
union A));
then
consider x be
set such that
A24: x
in (
union A) and
A25: y
in (f
.
{x}) and for b be
set st b
c= (
union A) & y
in (f
. b) holds x
in b by
A20,
A23;
consider a be
set such that
A26: x
in a and
A27: a
in A by
A24,
TARSKI:def 4;
A28:
{x}
c= a by
A26,
ZFMISC_1: 31;
then
{x}
in C by
A27,
CLASSES1:def 1;
then
A29: (f
.
{x})
c= (f
. a) by
A19,
A27,
A28;
(f
. a)
in (f
.: A) by
A27,
FUNCT_1:def 6;
hence thesis by
A25,
A29,
TARSKI:def 4;
end;
now
let X be
set;
assume X
in (f
.: A);
then
consider a be
object such that
A30: a
in (
dom f) and
A31: a
in A and
A32: X
= (f
. a) by
FUNCT_1:def 6;
reconsider aa = a as
set by
TARSKI: 1;
aa
c= (
union A) by
A31,
ZFMISC_1: 74;
hence X
c= (f
. (
union A)) by
A19,
A23,
A30,
A32;
end;
hence thesis by
ZFMISC_1: 76;
end;
end;
begin
definition
let f be
Function;
::
COHSP_1:def16
func
graph f ->
set means
:
Def16: for x be
set holds x
in it iff ex y be
finite
set, z be
set st x
=
[y, z] & y
in (
dom f) & z
in (f
. y);
existence
proof
defpred
P[
object] means ex y be
finite
set, z be
set st $1
=
[y, z] & y
in (
dom f) & z
in (f
. y);
consider X be
set such that
A1: for x be
object holds x
in X iff x
in
[:(
dom f), (
union (
rng f)):] &
P[x] from
XBOOLE_0:sch 1;
take X;
let x be
set;
now
given y be
finite
set, z be
set such that
A2: x
=
[y, z] and
A3: y
in (
dom f) and
A4: z
in (f
. y);
(f
. y)
in (
rng f) by
A3,
FUNCT_1:def 3;
then z
in (
union (
rng f)) by
A4,
TARSKI:def 4;
hence x
in
[:(
dom f), (
union (
rng f)):] by
A2,
A3,
ZFMISC_1: 87;
end;
hence thesis by
A1;
end;
uniqueness
proof
let X1,X2 be
set;
assume
A5: not thesis;
then
consider x be
object such that
A6: not (x
in X1 iff x
in X2) by
TARSKI: 2;
x
in X2 iff not ex y be
finite
set, z be
set st x
=
[y, z] & y
in (
dom f) & z
in (f
. y) by
A5,
A6;
hence thesis by
A5;
end;
end
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
proof
(
graph f)
c=
[:C1, (
union C2):]
proof
let x be
object;
assume x
in (
graph f);
then
consider y be
finite
set, z be
set such that
A1: x
=
[y, z] and
A2: y
in (
dom f) and
A3: z
in (f
. y) by
Def16;
(
rng f)
c= C2 & (f
. y)
in (
rng f) by
A2,
FUNCT_1:def 3,
RELAT_1:def 19;
then (
dom f)
= C1 & z
in (
union C2) by
A3,
FUNCT_2:def 1,
TARSKI:def 4;
hence thesis by
A1,
A2,
ZFMISC_1: 87;
end;
hence thesis;
end;
end
registration
let f be
Function;
cluster (
graph f) ->
Relation-like;
coherence
proof
let x be
object;
assume x
in (
graph f);
then ex y be
finite
set, z be
set st x
=
[y, z] & y
in (
dom f) & z
in (f
. y) by
Def16;
hence thesis;
end;
end
theorem ::
COHSP_1:24
Th24: for f be
Function, x,y be
set holds
[x, y]
in (
graph f) iff x is
finite & x
in (
dom f) & y
in (f
. x)
proof
let f be
Function, x,y be
set;
now
given y9 be
finite
set, z be
set such that
A1:
[x, y]
=
[y9, z] and
A2: y9
in (
dom f) & z
in (f
. y9);
x
= y9 by
A1,
XTUPLE_0: 1;
hence x is
finite & x
in (
dom f) & y
in (f
. x) by
A1,
A2,
XTUPLE_0: 1;
end;
hence thesis by
Def16;
end;
theorem ::
COHSP_1:25
Th25: for f be
c=-monotone
Function holds for a,b be
set st b
in (
dom f) & a
c= b & b is
finite holds for y be
set st
[a, y]
in (
graph f) holds
[b, y]
in (
graph f)
proof
let f be
c=-monotone
Function;
let a,b be
set such that
A1: b
in (
dom f) and
A2: a
c= b and
A3: b is
finite;
let y be
set;
assume
A4:
[a, y]
in (
graph f);
then a
in (
dom f) by
Th24;
then
A5: (f
. a)
c= (f
. b) by
A1,
A2,
Def11;
y
in (f
. a) by
A4,
Th24;
hence thesis by
A1,
A3,
A5,
Th24;
end;
theorem ::
COHSP_1:26
Th26: for C1,C2 be
Coherence_Space holds for f be
Function of C1, C2 holds for a be
Element of C1 holds for y1,y2 be
set st
[a, y1]
in (
graph f) &
[a, y2]
in (
graph f) holds
{y1, y2}
in C2
proof
let C1,C2 be
Coherence_Space;
let f be
Function of C1, C2;
let a be
Element of C1, y1,y2 be
set;
assume
[a, y1]
in (
graph f) &
[a, y2]
in (
graph f);
then y1
in (f
. a) & y2
in (f
. a) by
Th24;
then
{y1, y2}
c= (f
. a) by
ZFMISC_1: 32;
hence thesis by
CLASSES1:def 1;
end;
theorem ::
COHSP_1:27
for C1,C2 be
Coherence_Space holds for f be
c=-monotone
Function of C1, C2 holds for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y1,y2 be
set st
[a, y1]
in (
graph f) &
[b, y2]
in (
graph f) holds
{y1, y2}
in C2
proof
let C1,C2 be
Coherence_Space;
let f be
c=-monotone
Function of C1, C2;
let a,b be
Element of C1 such that
A1: (a
\/ b)
in C1;
let y1,y2 be
set;
assume
A2:
[a, y1]
in (
graph f) &
[b, y2]
in (
graph f);
then a is
finite & b is
finite by
Th24;
then
reconsider c = (a
\/ b) as
finite
Element of C1 by
A1;
(
dom f)
= C1 by
FUNCT_2:def 1;
then
[c, y1]
in (
graph f) &
[c, y2]
in (
graph f) by
A2,
Th25,
XBOOLE_1: 7;
hence thesis by
Th26;
end;
theorem ::
COHSP_1:28
Th28: for C1,C2 be
Coherence_Space holds for f,g be
U-continuous
Function of C1, C2 st (
graph f)
= (
graph g) holds f
= g
proof
let C1,C2 be
Coherence_Space;
let f,g be
U-continuous
Function of C1, C2;
A1: (
dom f)
= C1 by
FUNCT_2:def 1;
A2: (
dom g)
= C1 by
FUNCT_2:def 1;
A3:
now
let x be
finite
Element of C1;
let f,g be
U-continuous
Function of C1, C2;
A4: (
dom f)
= C1 by
FUNCT_2:def 1;
assume
A5: (
graph f)
= (
graph g);
thus (f
. x)
c= (g
. x)
proof
let z be
object;
assume
A6: z
in (f
. x);
reconsider x, z as
set by
TARSKI: 1;
[x, z]
in (
graph f) by
A4,
Th24,
A6;
hence thesis by
A5,
Th24;
end;
end;
A7:
now
let a be
Element of C1;
let f,g be
U-continuous
Function of C1, C2;
A8: (
dom g)
= C1 by
FUNCT_2:def 1;
assume
A9: (
graph f)
= (
graph g);
thus (f
.: (
Fin a))
c= (g
.: (
Fin a))
proof
let y be
object;
assume y
in (f
.: (
Fin a));
then
consider x be
object such that x
in (
dom f) and
A10: x
in (
Fin a) and
A11: y
= (f
. x) by
FUNCT_1:def 6;
(f
. x)
c= (g
. x) & (g
. x)
c= (f
. x) by
A3,
A9,
A10;
then (f
. x)
= (g
. x);
hence thesis by
A8,
A10,
A11,
FUNCT_1:def 6;
end;
end;
assume
A12: (
graph f)
= (
graph g);
now
let a be
Element of C1;
(f
.: (
Fin a))
c= (g
.: (
Fin a)) & (g
.: (
Fin a))
c= (f
.: (
Fin a)) by
A12,
A7;
then
A13: (f
.: (
Fin a))
= (g
.: (
Fin a));
thus (f
. a)
= (
union (f
.: (
Fin a))) by
A1,
Th20
.= (g
. a) by
A2,
A13,
Th20;
end;
hence thesis by
FUNCT_2: 63;
end;
Lm4: for C1,C2 be
Coherence_Space holds for X be
Subset of
[:C1, (
union C2):] st (for x be
set st x
in X holds (x
`1 ) is
finite) & (for a,b be
finite
Element of C1 st a
c= b holds for y be
set st
[a, y]
in X holds
[b, y]
in X) & (for a be
finite
Element of C1 holds for y1,y2 be
set st
[a, y1]
in X &
[a, y2]
in X holds
{y1, y2}
in C2) holds ex f be
U-continuous
Function of C1, C2 st X
= (
graph f) & for a be
Element of C1 holds (f
. a)
= (X
.: (
Fin a))
proof
let C1,C2 be
Coherence_Space;
let X be
Subset of
[:C1, (
union C2):] such that
A1: for x be
set st x
in X holds (x
`1 ) is
finite and
A2: for a,b be
finite
Element of C1 st a
c= b holds for y be
set st
[a, y]
in X holds
[b, y]
in X and
A3: for a be
finite
Element of C1 holds for y1,y2 be
set st
[a, y1]
in X &
[a, y2]
in X holds
{y1, y2}
in C2;
deffunc
f(
set) = (X
.: (
Fin $1));
consider f be
Function such that
A4: (
dom f)
= C1 & for a be
set st a
in C1 holds (f
. a)
=
f(a) from
FUNCT_1:sch 5;
A5: (
rng f)
c= C2
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
rng f);
then
consider a be
object such that
A6: a
in (
dom f) and
A7: x
= (f
. a) by
FUNCT_1:def 3;
reconsider a as
Element of C1 by
A4,
A6;
A8: x
= (X
.: (
Fin a)) by
A4,
A7;
now
let z,y be
set;
assume z
in xx;
then
consider z1 be
object such that
A9:
[z1, z]
in X and
A10: z1
in (
Fin a) by
A8,
RELAT_1:def 13;
assume y
in xx;
then
consider y1 be
object such that
A11:
[y1, y]
in X and
A12: y1
in (
Fin a) by
A8,
RELAT_1:def 13;
reconsider z1, y1 as
finite
Element of C1 by
A10,
A12;
(z1
\/ y1)
in (
Fin a) by
A10,
A12,
FINSUB_1: 1;
then
reconsider b = (z1
\/ y1) as
finite
Element of C1;
A13:
[b, y]
in X by
A2,
A11,
XBOOLE_1: 7;
[b, z]
in X by
A2,
A9,
XBOOLE_1: 7;
hence
{z, y}
in C2 by
A3,
A13;
end;
hence thesis by
COH_SP: 6;
end;
A14:
now
let a,y be
set;
assume that
A15: a
in (
dom f) and
A16: y
in (f
. a);
y
in (X
.: (
Fin a)) by
A4,
A15,
A16;
then
consider x be
object such that
A17:
[x, y]
in X and
A18: x
in (
Fin a) by
RELAT_1:def 13;
reconsider x as
set by
TARSKI: 1;
x
c= a by
A18,
FINSUB_1:def 5;
then x
in C1 by
A4,
A15,
CLASSES1:def 1;
then
A19: (f
. x)
= (X
.: (
Fin x)) by
A4;
take x;
x
in (
Fin x) by
A18,
FINSUB_1:def 5;
hence x is
finite & x
c= a & y
in (f
. x) by
A17,
A18,
A19,
FINSUB_1:def 5,
RELAT_1:def 13;
end;
f is
c=-monotone
proof
let a,b be
set;
assume that
A20: a
in (
dom f) & b
in (
dom f) and
A21: a
c= b;
reconsider a, b as
Element of C1 by
A4,
A20;
(
Fin a)
c= (
Fin b) by
A21,
FINSUB_1: 10;
then
A22: (X
.: (
Fin a))
c= (X
.: (
Fin b)) by
RELAT_1: 123;
(f
. a)
= (X
.: (
Fin a)) by
A4;
hence thesis by
A4,
A22;
end;
then
reconsider f as
U-continuous
Function of C1, C2 by
A4,
A5,
A14,
Th21,
FUNCT_2:def 1,
RELSET_1: 4;
take f;
thus X
= (
graph f)
proof
let a,b be
object;
hereby
assume
A23:
[a, b]
in X;
(
[a, b]
`1 )
= a;
then
reconsider a9 = a as
finite
Element of C1 by
A1,
A23,
ZFMISC_1: 87;
a9
in (
Fin a9) by
FINSUB_1:def 5;
then
A24: b
in (X
.: (
Fin a9)) by
A23,
RELAT_1:def 13;
(f
. a9)
= (X
.: (
Fin a9)) by
A4;
hence
[a, b]
in (
graph f) by
A4,
A24,
Th24;
end;
A25: a is
set & b is
set by
TARSKI: 1;
assume
A26:
[a, b]
in (
graph f);
then
reconsider a as
finite
Element of C1 by
A4,
Th24,
A25;
A27: (f
. a)
= (X
.: (
Fin a)) by
A4;
b
in (f
. a) by
A26,
Th24,
A25;
then
consider x be
object such that
A28:
[x, b]
in X and
A29: x
in (
Fin a) by
A27,
RELAT_1:def 13;
reconsider x as
set by
TARSKI: 1;
x
c= a by
A29,
FINSUB_1:def 5;
hence thesis by
A2,
A28,
A29,
A25;
end;
thus thesis by
A4;
end;
theorem ::
COHSP_1:29
for C1,C2 be
Coherence_Space holds for X be
Subset of
[:C1, (
union C2):] st (for x be
set st x
in X holds (x
`1 ) is
finite) & (for a,b be
finite
Element of C1 st a
c= b holds for y be
set st
[a, y]
in X holds
[b, y]
in X) & (for a be
finite
Element of C1 holds for y1,y2 be
set st
[a, y1]
in X &
[a, y2]
in X holds
{y1, y2}
in C2) holds ex f be
U-continuous
Function of C1, C2 st X
= (
graph f)
proof
let C1,C2 be
Coherence_Space;
let X be
Subset of
[:C1, (
union C2):];
assume
A1: not thesis;
then ex f be
U-continuous
Function of C1, C2 st X
= (
graph f) & for a be
Element of C1 holds (f
. a)
= (X
.: (
Fin a)) by
Lm4;
hence thesis by
A1;
end;
theorem ::
COHSP_1:30
for C1,C2 be
Coherence_Space holds for f be
U-continuous
Function of C1, C2 holds for a be
Element of C1 holds (f
. a)
= ((
graph f)
.: (
Fin a))
proof
let C1,C2 be
Coherence_Space;
let f be
U-continuous
Function of C1, C2;
let a be
Element of C1;
set X = (
graph f);
A1:
now
let x be
set;
assume x
in X;
then ex y be
finite
set, z be
set st x
=
[y, z] & y
in (
dom f) & z
in (f
. y) by
Def16;
hence (x
`1 ) is
finite;
end;
(
dom f)
= C1 by
FUNCT_2:def 1;
then
A2: for a,b be
finite
Element of C1 st a
c= b holds for y be
set st
[a, y]
in X holds
[b, y]
in X by
Th25;
for a be
finite
Element of C1 holds for y1,y2 be
set st
[a, y1]
in X &
[a, y2]
in X holds
{y1, y2}
in C2 by
Th26;
then
consider g be
U-continuous
Function of C1, C2 such that
A3: X
= (
graph g) and
A4: for a be
Element of C1 holds (g
. a)
= (X
.: (
Fin a)) by
A1,
A2,
Lm4;
(g
. a)
= (X
.: (
Fin a)) by
A4;
hence thesis by
A3,
Th28;
end;
begin
definition
let f be
Function;
::
COHSP_1:def17
func
Trace f ->
set means
:
Def17: for x be
set holds x
in it iff ex a,y be
set st x
=
[a, y] & a
in (
dom f) & y
in (f
. a) & for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b;
existence
proof
defpred
P[
object] means ex a,y be
set st $1
=
[a, y] & a
in (
dom f) & y
in (f
. a) & for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b;
consider T be
set such that
A1: for x be
object holds x
in T iff x
in
[:(
dom f), (
Union f):] &
P[x] from
XBOOLE_0:sch 1;
take T;
let x be
set;
now
given a,y be
set such that
A2: x
=
[a, y] and
A3: a
in (
dom f) and
A4: y
in (f
. a) and for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b;
y
in (
Union f) by
A3,
A4,
CARD_5: 2;
hence x
in
[:(
dom f), (
Union f):] by
A2,
A3,
ZFMISC_1: 87;
end;
hence thesis by
A1;
end;
uniqueness
proof
let T1,T2 be
set;
assume
A5: not thesis;
then
consider x be
object such that
A6: not (x
in T1 iff x
in T2) by
TARSKI: 2;
x
in T2 iff not ex a,y be
set st x
=
[a, y] & a
in (
dom f) & y
in (f
. a) & for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
A5,
A6;
hence contradiction by
A5;
end;
end
theorem ::
COHSP_1:31
Th31: for f be
Function holds for a be
set, y be
object holds
[a, y]
in (
Trace f) iff a
in (
dom f) & y
in (f
. a) & for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b
proof
let f be
Function, a9 be
set, y9 be
object;
now
given a,y be
set such that
A1:
[a9, y9]
=
[a, y] and
A2: a
in (
dom f) & y
in (f
. a) & for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b;
a9
= a & y9
= y by
A1,
XTUPLE_0: 1;
hence a9
in (
dom f) & y9
in (f
. a9) & for b be
set st b
in (
dom f) & b
c= a9 & y9
in (f
. b) holds a9
= b by
A2;
end;
hence thesis by
Def17;
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
proof
(
Trace f)
c=
[:C1, (
union C2):]
proof
let x be
object;
assume x
in (
Trace f);
then
consider a,y be
set such that
A1: x
=
[a, y] and
A2: a
in (
dom f) and
A3: y
in (f
. a) and for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
Def17;
(
rng f)
c= C2 & (f
. a)
in (
rng f) by
A2,
FUNCT_1:def 3,
RELAT_1:def 19;
then (
dom f)
= C1 & y
in (
union C2) by
A3,
FUNCT_2:def 1,
TARSKI:def 4;
hence thesis by
A1,
A2,
ZFMISC_1: 87;
end;
hence thesis;
end;
end
registration
let f be
Function;
cluster (
Trace f) ->
Relation-like;
coherence
proof
let x be
object;
assume x
in (
Trace f);
then ex a,y be
set st x
=
[a, y] & a
in (
dom f) & y
in (f
. a) & for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
Def17;
hence thesis;
end;
end
theorem ::
COHSP_1:32
for f be
U-continuous
Function st (
dom f) is
subset-closed holds (
Trace f)
c= (
graph f)
proof
let f be
U-continuous
Function such that
A1: (
dom f) is
subset-closed;
let x,z be
object;
assume
[x, z]
in (
Trace f);
then
consider a,y be
set such that
A2:
[x, z]
=
[a, y] and
A3: a
in (
dom f) and
A4: y
in (f
. a) and
A5: for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
Def17;
consider b be
set such that
A6: b is
finite and
A7: b
c= a and
A8: y
in (f
. b) by
A1,
A3,
A4,
Th21;
b
in (
dom f) by
A1,
A3,
A7;
then a
= b by
A5,
A7,
A8;
hence thesis by
A2,
A3,
A4,
A6,
Th24;
end;
theorem ::
COHSP_1:33
Th33: for f be
U-continuous
Function st (
dom f) is
subset-closed holds for a,y be
set st
[a, y]
in (
Trace f) holds a is
finite
proof
let f be
U-continuous
Function such that
A1: (
dom f) is
subset-closed;
let a,y be
set;
assume
A2:
[a, y]
in (
Trace f);
then
A3: a
in (
dom f) by
Th31;
y
in (f
. a) by
A2,
Th31;
then
consider b be
set such that
A4: b is
finite and
A5: b
c= a and
A6: y
in (f
. b) by
A1,
A3,
Th21;
b
in (
dom f) by
A1,
A3,
A5;
hence thesis by
A2,
A4,
A5,
A6,
Th31;
end;
theorem ::
COHSP_1:34
Th34: for C1,C2 be
Coherence_Space holds for f be
c=-monotone
Function of C1, C2 holds for a1,a2 be
set st (a1
\/ a2)
in C1 holds for y1,y2 be
object st
[a1, y1]
in (
Trace f) &
[a2, y2]
in (
Trace f) holds
{y1, y2}
in C2
proof
let C1,C2 be
Coherence_Space;
let f be
c=-monotone
Function of C1, C2;
A1: (
dom f)
= C1 by
FUNCT_2:def 1;
let a1,a2 be
set;
set a = (a1
\/ a2);
assume a
in C1;
then
reconsider a as
Element of C1;
A2: a2
c= a by
XBOOLE_1: 7;
then a2
in C1 by
CLASSES1:def 1;
then
A3: (f
. a2)
c= (f
. a) by
A1,
A2,
Def11;
let y1,y2 be
object;
assume
[a1, y1]
in (
Trace f) &
[a2, y2]
in (
Trace f);
then
A4: y1
in (f
. a1) & y2
in (f
. a2) by
Th31;
A5: a1
c= a by
XBOOLE_1: 7;
then a1
in C1 by
CLASSES1:def 1;
then (f
. a1)
c= (f
. a) by
A1,
A5,
Def11;
then
{y1, y2}
c= (f
. a) by
A3,
A4,
ZFMISC_1: 32;
hence thesis by
CLASSES1:def 1;
end;
theorem ::
COHSP_1:35
Th35: for C1,C2 be
Coherence_Space holds for f be
cap-distributive
Function of C1, C2 holds for a1,a2 be
set st (a1
\/ a2)
in C1 holds for y be
object st
[a1, y]
in (
Trace f) &
[a2, y]
in (
Trace f) holds a1
= a2
proof
let C1,C2 be
Coherence_Space;
let f be
cap-distributive
Function of C1, C2;
A1: (
dom f)
= C1 by
FUNCT_2:def 1;
let a1,a2 be
set;
set a = (a1
\/ a2);
assume
A2: a
in C1;
a2
c= a by
XBOOLE_1: 7;
then
A3: a2
in C1 by
A2,
CLASSES1:def 1;
a1
c= a by
XBOOLE_1: 7;
then
A4: a1
in C1 by
A2,
CLASSES1:def 1;
then
reconsider b = (a1
/\ a2) as
Element of C1 by
A3,
FINSUB_1:def 2;
b
in C1;
then
A5: C1
includes_lattice_of (a1,a2) by
A2,
A4,
A3,
Th16;
let y be
object;
assume that
A6:
[a1, y]
in (
Trace f) and
A7:
[a2, y]
in (
Trace f);
y
in (f
. a1) & y
in (f
. a2) by
A6,
A7,
Th31;
then y
in ((f
. a1)
/\ (f
. a2)) by
XBOOLE_0:def 4;
then
A8: y
in (f
. b) by
A1,
A5,
Def12;
b
c= a1 by
XBOOLE_1: 17;
then b
c= a2 & b
= a1 by
A1,
A6,
A8,
Th31,
XBOOLE_1: 17;
hence thesis by
A1,
A7,
A8,
Th31;
end;
theorem ::
COHSP_1:36
Th36: for C1,C2 be
Coherence_Space holds for f,g be
U-stable
Function of C1, C2 st (
Trace f)
c= (
Trace g) holds for a be
Element of C1 holds (f
. a)
c= (g
. a)
proof
let C1,C2 be
Coherence_Space;
let f,g be
U-stable
Function of C1, C2;
assume
A1: (
Trace f)
c= (
Trace g);
let x be
Element of C1;
A2: (
dom f)
= C1 by
FUNCT_2:def 1;
let z be
object;
assume z
in (f
. x);
then
consider b be
set such that b is
finite and
A3: b
c= x and
A4: z
in (f
. b) and
A5: for c be
set st c
c= x & z
in (f
. c) holds b
c= c by
A2,
Th22;
reconsider b as
Element of C1 by
A3,
CLASSES1:def 1;
now
let c be
set;
assume that c
in (
dom f) and
A6: c
c= b and
A7: z
in (f
. c);
c
c= x by
A3,
A6;
then b
c= c by
A5,
A7;
hence b
= c by
A6;
end;
then
[b, z]
in (
Trace f) by
A2,
A4,
Th31;
then
A8: z
in (g
. b) by
A1,
Th31;
(
dom g)
= C1 by
FUNCT_2:def 1;
then (g
. b)
c= (g
. x) by
A3,
Def11;
hence thesis by
A8;
end;
theorem ::
COHSP_1:37
Th37: for C1,C2 be
Coherence_Space holds for f,g be
U-stable
Function of C1, C2 st (
Trace f)
= (
Trace g) holds f
= g
proof
let C1,C2 be
Coherence_Space;
let f,g be
U-stable
Function of C1, C2;
A1: (
dom f)
= C1 by
FUNCT_2:def 1;
A2: (
dom g)
= C1 by
FUNCT_2:def 1;
A3:
now
let a be
Element of C1;
let f,g be
U-stable
Function of C1, C2;
A4: (
dom g)
= C1 by
FUNCT_2:def 1;
assume
A5: (
Trace f)
= (
Trace g);
thus (f
.: (
Fin a))
c= (g
.: (
Fin a))
proof
let y be
object;
assume y
in (f
.: (
Fin a));
then
consider x be
object such that x
in (
dom f) and
A6: x
in (
Fin a) and
A7: y
= (f
. x) by
FUNCT_1:def 6;
(f
. x)
c= (g
. x) & (g
. x)
c= (f
. x) by
A5,
A6,
Th36;
then (f
. x)
= (g
. x);
hence thesis by
A4,
A6,
A7,
FUNCT_1:def 6;
end;
end;
assume
A8: (
Trace f)
= (
Trace g);
now
let a be
Element of C1;
(f
.: (
Fin a))
c= (g
.: (
Fin a)) & (g
.: (
Fin a))
c= (f
.: (
Fin a)) by
A8,
A3;
then
A9: (f
.: (
Fin a))
= (g
.: (
Fin a));
thus (f
. a)
= (
union (f
.: (
Fin a))) by
A1,
Th20
.= (g
. a) by
A2,
A9,
Th20;
end;
hence thesis by
FUNCT_2: 63;
end;
Lm5: for C1,C2 be
Coherence_Space holds for X be
Subset of
[:C1, (
union C2):] st (for x be
set st x
in X holds (x
`1 ) is
finite) & (for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2) & (for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b) holds ex f be
U-stable
Function of C1, C2 st X
= (
Trace f) & for a be
Element of C1 holds (f
. a)
= (X
.: (
Fin a))
proof
let C1,C2 be
Coherence_Space;
let X be
Subset of
[:C1, (
union C2):] such that
A1: for x be
set st x
in X holds (x
`1 ) is
finite and
A2: for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2 and
A3: for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b;
deffunc
f(
set) = (X
.: (
Fin $1));
consider f be
Function such that
A4: (
dom f)
= C1 & for a be
set st a
in C1 holds (f
. a)
=
f(a) from
FUNCT_1:sch 5;
A5:
now
let a,y be
set;
assume that
A6: a
in (
dom f) and
A7: y
in (f
. a);
reconsider a9 = a as
Element of C1 by
A4,
A6;
y
in (X
.: (
Fin a)) by
A4,
A6,
A7;
then
consider x be
object such that
A8:
[x, y]
in X and
A9: x
in (
Fin a) by
RELAT_1:def 13;
reconsider x as
set by
TARSKI: 1;
x
c= a by
A9,
FINSUB_1:def 5;
then x
in C1 by
A4,
A6,
CLASSES1:def 1;
then
A10: (f
. x)
= (X
.: (
Fin x)) by
A4;
take x;
x
in (
Fin x) by
A9,
FINSUB_1:def 5;
hence x is
finite & x
c= a & y
in (f
. x) by
A8,
A9,
A10,
FINSUB_1:def 5,
RELAT_1:def 13;
let c be
set;
assume that
A11: c
c= a and
A12: y
in (f
. c);
c
c= a9 by
A11;
then c
in (
dom f) by
A4,
CLASSES1:def 1;
then y
in (X
.: (
Fin c)) by
A4,
A12;
then
consider z be
object such that
A13:
[z, y]
in X and
A14: z
in (
Fin c) by
RELAT_1:def 13;
A15: (
Fin c)
c= (
Fin a) by
A11,
FINSUB_1: 10;
then
A16: z
in (
Fin a9) by
A14;
reconsider z as
set by
TARSKI: 1;
(x
\/ z)
in (
Fin a9) by
A9,
A14,
A15,
FINSUB_1: 1;
then x
= z by
A3,
A8,
A9,
A13,
A16;
hence x
c= c by
A14,
FINSUB_1:def 5;
end;
A17: (
rng f)
c= C2
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
rng f);
then
consider a be
object such that
A18: a
in (
dom f) and
A19: x
= (f
. a) by
FUNCT_1:def 3;
reconsider a as
Element of C1 by
A4,
A18;
A20: x
= (X
.: (
Fin a)) by
A4,
A19;
now
let z,y be
set;
assume z
in xx;
then
consider z1 be
object such that
A21:
[z1, z]
in X and
A22: z1
in (
Fin a) by
A20,
RELAT_1:def 13;
assume y
in xx;
then
consider y1 be
object such that
A23:
[y1, y]
in X and
A24: y1
in (
Fin a) by
A20,
RELAT_1:def 13;
reconsider y1, z1 as
set by
TARSKI: 1;
(z1
\/ y1)
in (
Fin a) by
A22,
A24,
FINSUB_1: 1;
hence
{z, y}
in C2 by
A2,
A21,
A22,
A23,
A24;
end;
hence thesis by
COH_SP: 6;
end;
f is
c=-monotone
proof
let a,b be
set;
assume that
A25: a
in (
dom f) & b
in (
dom f) and
A26: a
c= b;
reconsider a, b as
Element of C1 by
A4,
A25;
(
Fin a)
c= (
Fin b) by
A26,
FINSUB_1: 10;
then
A27: (X
.: (
Fin a))
c= (X
.: (
Fin b)) by
RELAT_1: 123;
(f
. a)
= (X
.: (
Fin a)) by
A4;
hence thesis by
A4,
A27;
end;
then
reconsider f as
U-stable
Function of C1, C2 by
A4,
A17,
A5,
Th22,
FUNCT_2:def 1,
RELSET_1: 4;
take f;
thus X
= (
Trace f)
proof
let a,b be
object;
hereby
assume
A28:
[a, b]
in X;
(
[a, b]
`1 )
= a;
then
reconsider a9 = a as
finite
Element of C1 by
A1,
A28,
ZFMISC_1: 87;
a9
in (
Fin a9) by
FINSUB_1:def 5;
then
A29: b
in (X
.: (
Fin a9)) by
A28,
RELAT_1:def 13;
A30:
now
let c be
set;
assume that
A31: c
in (
dom f) and
A32: c
c= a9 and
A33: b
in (f
. c);
reconsider c9 = c as
Element of C1 by
A4,
A31;
b
in (X
.: (
Fin c9)) by
A4,
A33;
then
consider x be
object such that
A34:
[x, b]
in X and
A35: x
in (
Fin c9) by
RELAT_1:def 13;
reconsider x as
set by
TARSKI: 1;
A36: x
c= c by
A35,
FINSUB_1:def 5;
then (x
\/ a9)
= a9 by
A32,
XBOOLE_1: 1,
XBOOLE_1: 12;
then x
= a by
A3,
A28,
A34,
A35;
hence a9
= c by
A32,
A36;
end;
(f
. a9)
= (X
.: (
Fin a9)) by
A4;
hence
[a, b]
in (
Trace f) by
A4,
A29,
A30,
Th31;
end;
assume
A37:
[a, b]
in (
Trace f);
reconsider a, b as
set by
TARSKI: 1;
a
in (
dom f) & b
in (f
. a) by
Th31,
A37;
then b
in (X
.: (
Fin a)) by
A4;
then
consider x be
object such that
A38:
[x, b]
in X and
A39: x
in (
Fin a) by
RELAT_1:def 13;
reconsider a as
Element of C1 by
A4,
A37,
Th31;
x
in (
Fin a) by
A39;
then
reconsider x as
finite
Element of C1;
x
in (
Fin x) by
FINSUB_1:def 5;
then b
in (X
.: (
Fin x)) by
A38,
RELAT_1:def 13;
then
A40: b
in (f
. x) by
A4;
x
c= a by
A39,
FINSUB_1:def 5;
hence thesis by
A4,
A37,
A38,
A40,
Th31;
end;
thus thesis by
A4;
end;
theorem ::
COHSP_1:38
Th38: for C1,C2 be
Coherence_Space holds for X be
Subset of
[:C1, (
union C2):] st (for x be
set st x
in X holds (x
`1 ) is
finite) & (for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2) & (for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b) holds ex f be
U-stable
Function of C1, C2 st X
= (
Trace f)
proof
let C1,C2 be
Coherence_Space;
let X be
Subset of
[:C1, (
union C2):];
assume
A1: not thesis;
then ex f be
U-stable
Function of C1, C2 st X
= (
Trace f) & for a be
Element of C1 holds (f
. a)
= (X
.: (
Fin a)) by
Lm5;
hence thesis by
A1;
end;
theorem ::
COHSP_1:39
for C1,C2 be
Coherence_Space holds for f be
U-stable
Function of C1, C2 holds for a be
Element of C1 holds (f
. a)
= ((
Trace f)
.: (
Fin a))
proof
let C1,C2 be
Coherence_Space;
let f be
U-stable
Function of C1, C2;
let a be
Element of C1;
set X = (
Trace f);
A1: (
dom f)
= C1 by
FUNCT_2:def 1;
A2:
now
let x be
set;
assume
A3: x
in X;
then
consider a,y be
set such that
A4: x
=
[a, y] and a
in (
dom f) and y
in (f
. a) and for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
Def17;
a is
finite by
A1,
A3,
A4,
Th33;
hence (x
`1 ) is
finite by
A4;
end;
(for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2) & for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b by
Th34,
Th35;
then
consider g be
U-stable
Function of C1, C2 such that
A5: X
= (
Trace g) and
A6: for a be
Element of C1 holds (g
. a)
= (X
.: (
Fin a)) by
A2,
Lm5;
(g
. a)
= (X
.: (
Fin a)) by
A6;
hence thesis by
A5,
Th37;
end;
theorem ::
COHSP_1:40
Th40: for C1,C2 be
Coherence_Space, f be
U-stable
Function of C1, C2 holds for a be
Element of C1, y be
set holds y
in (f
. a) iff ex b be
Element of C1 st
[b, y]
in (
Trace f) & b
c= a
proof
let C1,C2 be
Coherence_Space, f be
U-stable
Function of C1, C2;
let a be
Element of C1, y be
set;
A1: (
dom f)
= C1 by
FUNCT_2:def 1;
hereby
assume y
in (f
. a);
then
consider b be
set such that b is
finite and
A2: b
c= a and
A3: y
in (f
. b) and
A4: for c be
set st c
c= a & y
in (f
. c) holds b
c= c by
A1,
Th22;
reconsider b as
Element of C1 by
A2,
CLASSES1:def 1;
take b;
now
let c be
set;
assume that c
in (
dom f) and
A5: c
c= b and
A6: y
in (f
. c);
c
c= a by
A2,
A5;
then b
c= c by
A4,
A6;
hence b
= c by
A5;
end;
hence
[b, y]
in (
Trace f) by
A1,
A3,
Th31;
thus b
c= a by
A2;
end;
given b be
Element of C1 such that
A7:
[b, y]
in (
Trace f) and
A8: b
c= a;
A9: y
in (f
. b) by
A7,
Th31;
(f
. b)
c= (f
. a) by
A1,
A8,
Def11;
hence thesis by
A9;
end;
theorem ::
COHSP_1:41
for C1,C2 be
Coherence_Space holds ex f be
U-stable
Function of C1, C2 st (
Trace f)
=
{}
proof
let C1,C2 be
Coherence_Space;
reconsider X =
{} as
Subset of
[:C1, (
union C2):] by
XBOOLE_1: 2;
A1: for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b;
(for x be
set st x
in X holds (x
`1 ) is
finite) & for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2;
hence thesis by
A1,
Th38;
end;
theorem ::
COHSP_1:42
Th42: for C1,C2 be
Coherence_Space holds for a be
finite
Element of C1, y be
set st y
in (
union C2) holds ex f be
U-stable
Function of C1, C2 st (
Trace f)
=
{
[a, y]}
proof
let C1,C2 be
Coherence_Space;
let a be
finite
Element of C1, y be
set;
assume
A1: y
in (
union C2);
then
[a, y]
in
[:C1, (
union C2):] by
ZFMISC_1: 87;
then
reconsider X =
{
[a, y]} as
Subset of
[:C1, (
union C2):] by
ZFMISC_1: 31;
A2:
now
let a1,b be
Element of C1;
assume (a1
\/ b)
in C1;
let y1,y2 be
object;
assume that
A3:
[a1, y1]
in X and
A4:
[b, y2]
in X;
[b, y2]
=
[a, y] by
A4,
TARSKI:def 1;
then
A5: y2
= y by
XTUPLE_0: 1;
[a1, y1]
=
[a, y] by
A3,
TARSKI:def 1;
then y1
= y by
XTUPLE_0: 1;
then
{y1, y2}
=
{y} by
A5,
ENUMSET1: 29;
hence
{y1, y2}
in C2 by
A1,
COH_SP: 4;
end;
A6:
now
let a1,b be
Element of C1;
assume (a1
\/ b)
in C1;
let y1 be
object;
assume
[a1, y1]
in X &
[b, y1]
in X;
then
[a1, y1]
=
[a, y] &
[b, y1]
=
[a, y] by
TARSKI:def 1;
hence a1
= b by
XTUPLE_0: 1;
end;
now
let x be
set;
assume x
in X;
then x
=
[a, y] by
TARSKI:def 1;
hence (x
`1 ) is
finite;
end;
hence thesis by
A2,
A6,
Th38;
end;
theorem ::
COHSP_1:43
for C1,C2 be
Coherence_Space holds for a be
Element of C1, y be
set holds for f be
U-stable
Function of C1, C2 st (
Trace f)
=
{
[a, y]} holds for b be
Element of C1 holds (a
c= b implies (f
. b)
=
{y}) & ( not a
c= b implies (f
. b)
=
{} )
proof
let C1,C2 be
Coherence_Space;
let a be
Element of C1, y be
set;
let f be
U-stable
Function of C1, C2;
assume
A1: (
Trace f)
=
{
[a, y]};
let b be
Element of C1;
A2:
[a, y]
in (
Trace f) by
A1,
TARSKI:def 1;
hereby
A3: (f
. b)
c=
{y}
proof
let x be
object;
assume x
in (f
. b);
then
consider c be
Element of C1 such that
A4:
[c, x]
in (
Trace f) and c
c= b by
Th40;
[c, x]
=
[a, y] by
A1,
A4,
TARSKI:def 1;
then x
= y by
XTUPLE_0: 1;
hence thesis by
TARSKI:def 1;
end;
assume a
c= b;
then y
in (f
. b) by
A2,
Th40;
then
{y}
c= (f
. b) by
ZFMISC_1: 31;
hence (f
. b)
=
{y} by
A3;
end;
assume that
A5: not a
c= b and
A6: (f
. b)
<>
{} ;
reconsider B = (f
. b) as non
empty
set by
A6;
set z = the
Element of B;
consider c be
Element of C1 such that
A7:
[c, z]
in (
Trace f) and
A8: c
c= b by
Th40;
[c, z]
=
[a, y] by
A1,
A7,
TARSKI:def 1;
hence thesis by
A5,
A8,
XTUPLE_0: 1;
end;
theorem ::
COHSP_1:44
Th44: for C1,C2 be
Coherence_Space holds for f be
U-stable
Function of C1, C2 holds for X be
Subset of (
Trace f) holds ex g be
U-stable
Function of C1, C2 st (
Trace g)
= X
proof
let C1,C2 be
Coherence_Space;
let f be
U-stable
Function of C1, C2;
let X be
Subset of (
Trace f);
A1: for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b by
Th35;
A2:
now
let x be
set;
assume
A3: x
in X;
then
consider a,y be
set such that
A4: x
=
[a, y] and a
in (
dom f) and y
in (f
. a) and for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
Def17;
(
dom f)
= C1 by
FUNCT_2:def 1;
then a is
finite by
A3,
A4,
Th33;
hence (x
`1 ) is
finite by
A4;
end;
X is
Subset of
[:C1, (
union C2):] & for a,b be
Element of C1 st (a
\/ b)
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2 by
Th34,
XBOOLE_1: 1;
hence thesis by
A2,
A1,
Th38;
end;
theorem ::
COHSP_1:45
Th45: for C1,C2 be
Coherence_Space holds for A be
set st for x,y be
set st x
in A & y
in A holds ex f be
U-stable
Function of C1, C2 st (x
\/ y)
= (
Trace f) holds ex f be
U-stable
Function of C1, C2 st (
union A)
= (
Trace f)
proof
let C1,C2 be
Coherence_Space;
let A be
set such that
A1: for x,y be
set st x
in A & y
in A holds ex f be
U-stable
Function of C1, C2 st (x
\/ y)
= (
Trace f);
set X = (
union A);
A2:
now
let a,b be
Element of C1 such that
A3: (a
\/ b)
in C1;
let y1,y2 be
object;
assume
[a, y1]
in X;
then
consider x1 be
set such that
A4:
[a, y1]
in x1 and
A5: x1
in A by
TARSKI:def 4;
assume
[b, y2]
in X;
then
consider x2 be
set such that
A6:
[b, y2]
in x2 and
A7: x2
in A by
TARSKI:def 4;
A8: x1
c= (x1
\/ x2) & x2
c= (x1
\/ x2) by
XBOOLE_1: 7;
ex f be
U-stable
Function of C1, C2 st (x1
\/ x2)
= (
Trace f) by
A1,
A5,
A7;
hence
{y1, y2}
in C2 by
A3,
A4,
A6,
A8,
Th34;
end;
A9:
now
let a,b be
Element of C1 such that
A10: (a
\/ b)
in C1;
let y be
object;
assume
[a, y]
in X;
then
consider x1 be
set such that
A11:
[a, y]
in x1 and
A12: x1
in A by
TARSKI:def 4;
assume
[b, y]
in X;
then
consider x2 be
set such that
A13:
[b, y]
in x2 and
A14: x2
in A by
TARSKI:def 4;
A15: x1
c= (x1
\/ x2) & x2
c= (x1
\/ x2) by
XBOOLE_1: 7;
ex f be
U-stable
Function of C1, C2 st (x1
\/ x2)
= (
Trace f) by
A1,
A12,
A14;
hence a
= b by
A10,
A11,
A13,
A15,
Th35;
end;
A16:
now
let x be
set;
assume x
in X;
then
consider y be
set such that
A17: x
in y and
A18: y
in A by
TARSKI:def 4;
(y
\/ y)
= y;
then
consider f be
U-stable
Function of C1, C2 such that
A19: y
= (
Trace f) by
A1,
A18;
consider a,y be
set such that
A20: x
=
[a, y] and a
in (
dom f) and y
in (f
. a) and for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
A17,
A19,
Def17;
(
dom f)
= C1 by
FUNCT_2:def 1;
then a is
finite by
A17,
A19,
A20,
Th33;
hence (x
`1 ) is
finite by
A20;
end;
X
c=
[:C1, (
union C2):]
proof
let x be
object;
assume x
in X;
then
consider y be
set such that
A21: x
in y and
A22: y
in A by
TARSKI:def 4;
(y
\/ y)
= y;
then ex f be
U-stable
Function of C1, C2 st y
= (
Trace f) by
A1,
A22;
hence thesis by
A21;
end;
hence thesis by
A16,
A2,
A9,
Th38;
end;
definition
let C1,C2 be
Coherence_Space;
::
COHSP_1:def18
func
StabCoh (C1,C2) ->
set means
:
Def18: for x be
set holds x
in it iff ex f be
U-stable
Function of C1, C2 st x
= (
Trace f);
uniqueness
proof
let X1,X2 be
set;
assume
A1: not thesis;
then
consider x be
object such that
A2: not (x
in X1 iff x
in X2) by
TARSKI: 2;
x
in X2 iff not ex f be
U-stable
Function of C1, C2 st x
= (
Trace f) by
A1,
A2;
hence thesis by
A1;
end;
existence
proof
defpred
P[
object] means ex f be
U-stable
Function of C1, C2 st $1
= (
Trace f);
consider X be
set such that
A3: for x be
object holds x
in X iff x
in (
bool
[:C1, (
union C2):]) &
P[x] from
XBOOLE_0:sch 1;
take X;
let x be
set;
thus thesis by
A3;
end;
end
registration
let C1,C2 be
Coherence_Space;
cluster (
StabCoh (C1,C2)) -> non
empty
subset-closed
binary_complete;
coherence
proof
set C = (
StabCoh (C1,C2));
set f = the
U-stable
Function of C1, C2;
(
Trace f)
in C by
Def18;
hence C is non
empty;
thus C is
subset-closed
proof
let a,b be
set;
assume a
in C;
then
A1: ex f be
U-stable
Function of C1, C2 st a
= (
Trace f) by
Def18;
assume b
c= a;
then ex g be
U-stable
Function of C1, C2 st (
Trace g)
= b by
A1,
Th44;
hence thesis by
Def18;
end;
let A be
set;
assume
A2: for a,b be
set st a
in A & b
in A holds (a
\/ b)
in C;
now
let x,y be
set;
assume x
in A & y
in A;
then (x
\/ y)
in C by
A2;
hence ex f be
U-stable
Function of C1, C2 st (x
\/ y)
= (
Trace f) by
Def18;
end;
then ex f be
U-stable
Function of C1, C2 st (
union A)
= (
Trace f) by
Th45;
hence thesis by
Def18;
end;
end
theorem ::
COHSP_1:46
Th46: for C1,C2 be
Coherence_Space, f be
U-stable
Function of C1, C2 holds (
Trace f)
c=
[:(
Sub_of_Fin C1), (
union C2):]
proof
let C1,C2 be
Coherence_Space, f be
U-stable
Function of C1, C2;
let x1,x2 be
object;
assume
A1:
[x1, x2]
in (
Trace f);
then
consider a,y be
set such that
A2:
[x1, x2]
=
[a, y] and
A3: a
in (
dom f) and
A4: y
in (f
. a) and for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
Def17;
A5: (
dom f)
= C1 by
FUNCT_2:def 1;
then a is
finite by
A1,
A2,
Th33;
then
A6: a
in (
Sub_of_Fin C1) by
A3,
A5,
Def3;
y
in (
union C2) by
A3,
A4,
A5,
Lm1;
hence thesis by
A2,
A6,
ZFMISC_1: 87;
end;
theorem ::
COHSP_1:47
for C1,C2 be
Coherence_Space holds (
union (
StabCoh (C1,C2)))
=
[:(
Sub_of_Fin C1), (
union C2):]
proof
let C1,C2 be
Coherence_Space;
thus (
union (
StabCoh (C1,C2)))
c=
[:(
Sub_of_Fin C1), (
union C2):]
proof
let x be
object;
assume x
in (
union (
StabCoh (C1,C2)));
then
consider a be
set such that
A1: x
in a and
A2: a
in (
StabCoh (C1,C2)) by
TARSKI:def 4;
ex f be
U-stable
Function of C1, C2 st a
= (
Trace f) by
A2,
Def18;
then a
c=
[:(
Sub_of_Fin C1), (
union C2):] by
Th46;
hence thesis by
A1;
end;
let x,y be
object;
assume
A3:
[x, y]
in
[:(
Sub_of_Fin C1), (
union C2):];
then
A4: y
in (
union C2) by
ZFMISC_1: 87;
reconsider x as
set by
TARSKI: 1;
A5: x
in (
Sub_of_Fin C1) by
A3,
ZFMISC_1: 87;
then x is
finite by
Def3;
then ex f be
U-stable
Function of C1, C2 st (
Trace f)
=
{
[x, y]} by
A5,
A4,
Th42;
then
[x, y]
in
{
[x, y]} &
{
[x, y]}
in (
StabCoh (C1,C2)) by
Def18,
TARSKI:def 1;
hence thesis by
TARSKI:def 4;
end;
theorem ::
COHSP_1:48
Th48: for C1,C2 be
Coherence_Space holds for a,b be
finite
Element of C1, y1,y2 be
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
let C1,C2 be
Coherence_Space;
let a,b be
finite
Element of C1, y1,y2 be
set;
hereby
assume
[
[a, y1],
[b, y2]]
in (
Web (
StabCoh (C1,C2)));
then
{
[a, y1],
[b, y2]}
in (
StabCoh (C1,C2)) by
COH_SP: 5;
then
A1: ex f be
U-stable
Function of C1, C2 st
{
[a, y1],
[b, y2]}
= (
Trace f) by
Def18;
A2:
[a, y1]
in
{
[a, y1],
[b, y2]} &
[b, y2]
in
{
[a, y1],
[b, y2]} by
TARSKI:def 2;
assume
A3: (a
\/ b)
in C1 or not y1
in (
union C2) or not y2
in (
union C2);
then
{y1, y2}
in C2 by
A1,
A2,
Th34,
ZFMISC_1: 87;
hence
[y1, y2]
in (
Web C2) by
COH_SP: 5;
thus y1
= y2 implies a
= b by
A1,
A2,
A3,
Th35,
ZFMISC_1: 87;
end;
assume
A4: not (a
\/ b)
in C1 & y1
in (
union C2) & y2
in (
union C2) or
[y1, y2]
in (
Web C2) & (y1
= y2 implies a
= b);
then
A5: y2
in (
union C2) by
ZFMISC_1: 87;
then
A6:
[b, y2]
in
[:C1, (
union C2):] by
ZFMISC_1: 87;
A7: y1
in (
union C2) by
A4,
ZFMISC_1: 87;
then
[a, y1]
in
[:C1, (
union C2):] by
ZFMISC_1: 87;
then
reconsider X =
{
[a, y1],
[b, y2]} as
Subset of
[:C1, (
union C2):] by
A6,
ZFMISC_1: 32;
A8:
now
let a1,b1 be
Element of C1;
assume
A9: (a1
\/ b1)
in C1;
let z1,z2 be
object;
assume that
A10:
[a1, z1]
in X and
A11:
[b1, z2]
in X;
[b1, z2]
=
[a, y1] or
[b1, z2]
=
[b, y2] by
A11,
TARSKI:def 2;
then
A12: z2
= y1 & b1
= a or b1
= b & z2
= y2 by
XTUPLE_0: 1;
[a1, z1]
=
[a, y1] or
[a1, z1]
=
[b, y2] by
A10,
TARSKI:def 2;
then z1
= y1 & a1
= a or a1
= b & z1
= y2 by
XTUPLE_0: 1;
then
{z1, z2}
=
{y1} or
{z1, z2}
in C2 or
{z1, z2}
=
{y2} by
A4,
A9,
A12,
COH_SP: 5,
ENUMSET1: 29;
hence
{z1, z2}
in C2 by
A7,
A5,
COH_SP: 4;
end;
A13:
now
let a1,b1 be
Element of C1;
assume
A14: (a1
\/ b1)
in C1;
let y be
object;
assume that
A15:
[a1, y]
in X and
A16:
[b1, y]
in X;
[a1, y]
=
[a, y1] or
[a1, y]
=
[b, y2] by
A15,
TARSKI:def 2;
then
A17: a1
= a & y
= y1 or a1
= b & y
= y2 by
XTUPLE_0: 1;
[b1, y]
=
[a, y1] or
[b1, y]
=
[b, y2] by
A16,
TARSKI:def 2;
hence a1
= b1 by
A4,
A14,
A17,
XTUPLE_0: 1;
end;
now
let x be
set;
assume x
in X;
then x
=
[a, y1] or x
=
[b, y2] by
TARSKI:def 2;
hence (x
`1 ) is
finite;
end;
then ex f be
U-stable
Function of C1, C2 st X
= (
Trace f) by
A8,
A13,
Th38;
then X
in (
StabCoh (C1,C2)) by
Def18;
hence thesis by
COH_SP: 5;
end;
begin
theorem ::
COHSP_1:49
Th49: for C1,C2 be
Coherence_Space holds for f be
U-stable
Function of C1, C2 holds f is
U-linear iff for a be
set, y be
object st
[a, y]
in (
Trace f) holds ex x be
set st a
=
{x}
proof
let C1,C2 be
Coherence_Space;
let f be
U-stable
Function of C1, C2;
A1: (
dom f)
= C1 by
FUNCT_2:def 1;
hereby
assume
A2: f is
U-linear;
let a be
set, y be
object;
assume
A3:
[a, y]
in (
Trace f);
then
A4: a
in (
dom f) by
Th31;
y
in (f
. a) by
A3,
Th31;
then
consider x be
set such that
A5: x
in a and
A6: y
in (f
.
{x}) and for b be
set st b
c= a & y
in (f
. b) holds x
in b by
A1,
A2,
A4,
Th23;
A7:
{x}
c= a by
A5,
ZFMISC_1: 31;
take x;
A8:
{x, x}
=
{x} by
ENUMSET1: 29;
{x, x}
in C1 by
A1,
A4,
A5,
COH_SP: 6;
hence a
=
{x} by
A1,
A3,
A6,
A7,
A8,
Th31;
end;
assume
A9: for a be
set, y be
object st
[a, y]
in (
Trace f) holds ex x be
set st a
=
{x};
now
let a,y be
set;
assume that
A10: a
in (
dom f) and
A11: y
in (f
. a);
consider b be
set such that b is
finite and
A12: b
c= a and
A13: y
in (f
. b) and
A14: for c be
set st c
c= a & y
in (f
. c) holds b
c= c by
A1,
A10,
A11,
Th22;
now
thus b
in (
dom f) by
A1,
A10,
A12,
CLASSES1:def 1;
let c be
set;
assume that c
in (
dom f) and
A15: c
c= b and
A16: y
in (f
. c);
c
c= a by
A12,
A15;
then b
c= c by
A14,
A16;
hence b
= c by
A15;
end;
then
[b, y]
in (
Trace f) by
A13,
Th31;
then
consider x be
set such that
A17: b
=
{x} by
A9;
take x;
x
in b by
A17,
TARSKI:def 1;
hence x
in a & y
in (f
.
{x}) by
A12,
A13,
A17;
let c be
set;
assume c
c= a & y
in (f
. c);
then b
c= c by
A14;
hence x
in c by
A17,
ZFMISC_1: 31;
end;
hence thesis by
A1,
Th23;
end;
definition
let f be
Function;
::
COHSP_1:def19
func
LinTrace f ->
set means
:
Def19: for x be
object holds x
in it iff ex y,z be
object st x
=
[y, z] &
[
{y}, z]
in (
Trace f);
uniqueness
proof
let X1,X2 be
set;
assume
A1: not thesis;
then
consider x be
object such that
A2: not (x
in X1 iff x
in X2) by
TARSKI: 2;
x
in X2 iff not ex y,z be
object st x
=
[y, z] &
[
{y}, z]
in (
Trace f) by
A1,
A2;
hence thesis by
A1;
end;
existence
proof
defpred
P[
object] means ex y,z be
object st $1
=
[y, z] &
[
{y}, z]
in (
Trace f);
set C1 = (
dom f), C2 = (
rng f);
consider X be
set such that
A3: for x be
object holds x
in X iff x
in
[:(
union C1), (
union C2):] &
P[x] from
XBOOLE_0:sch 1;
take X;
let x be
object;
now
given y,z be
object such that
A4: x
=
[y, z] and
A5:
[
{y}, z]
in (
Trace f);
A6:
{y}
in C1 by
A5,
Th31;
then
A7: (f
.
{y})
in C2 by
FUNCT_1:def 3;
z
in (f
.
{y}) by
A5,
Th31;
then
A8: z
in (
union C2) by
A7,
TARSKI:def 4;
y
in
{y} by
TARSKI:def 1;
then y
in (
union C1) by
A6,
TARSKI:def 4;
hence x
in
[:(
union C1), (
union C2):] by
A4,
A8,
ZFMISC_1: 87;
end;
hence thesis by
A3;
end;
end
theorem ::
COHSP_1:50
Th50: for f be
Function, x,y be
object holds
[x, y]
in (
LinTrace f) iff
[
{x}, y]
in (
Trace f)
proof
let f be
Function, x,y be
object;
now
given v,z be
object such that
A1:
[x, y]
=
[v, z] and
A2:
[
{v}, z]
in (
Trace f);
x
= v by
A1,
XTUPLE_0: 1;
hence
[
{x}, y]
in (
Trace f) by
A1,
A2,
XTUPLE_0: 1;
end;
hence thesis by
Def19;
end;
theorem ::
COHSP_1:51
Th51: for f be
Function st (f
.
{} )
=
{} holds for x,y be
object st
{x}
in (
dom f) & y
in (f
.
{x}) holds
[x, y]
in (
LinTrace f)
proof
let f be
Function;
assume
A1: (f
.
{} )
=
{} ;
let x,y be
object;
set a =
{x};
[x, y]
in (
LinTrace f) iff
[
{x}, y]
in (
Trace f) by
Th50;
then
[x, y]
in (
LinTrace f) iff
{x}
in (
dom f) & y
in (f
.
{x}) & for b be
set st b
in (
dom f) & b
c= a & y
in (f
. b) holds a
= b by
Th31;
hence thesis by
A1,
ZFMISC_1: 33;
end;
theorem ::
COHSP_1:52
Th52: for f be
Function, x,y be
object st
[x, y]
in (
LinTrace f) holds
{x}
in (
dom f) & y
in (f
.
{x})
proof
let f be
Function, x,y be
object;
assume
[x, y]
in (
LinTrace f);
then
[
{x}, y]
in (
Trace f) by
Th50;
hence thesis by
Th31;
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
proof
(
LinTrace f)
c=
[:(
union C1), (
union C2):]
proof
let x be
object;
assume x
in (
LinTrace f);
then
consider y,z be
object such that
A1: x
=
[y, z] and
A2:
[
{y}, z]
in (
Trace f) by
Def19;
A3: y
in
{y} by
TARSKI:def 1;
(
dom f)
= C1 by
FUNCT_2:def 1;
then
{y}
in C1 by
A2,
Th31;
then
A4: y
in (
union C1) by
A3,
TARSKI:def 4;
z
in (
union C2) by
A2,
ZFMISC_1: 87;
hence thesis by
A1,
A4,
ZFMISC_1: 87;
end;
hence thesis;
end;
end
registration
let f be
Function;
cluster (
LinTrace f) ->
Relation-like;
coherence
proof
let x be
object;
assume x
in (
LinTrace f);
then ex y,z be
object st x
=
[y, z] &
[
{y}, z]
in (
Trace f) by
Def19;
hence thesis;
end;
end
definition
let C1,C2 be
Coherence_Space;
::
COHSP_1:def20
func
LinCoh (C1,C2) ->
set means
:
Def20: for x be
set holds x
in it iff ex f be
U-linear
Function of C1, C2 st x
= (
LinTrace f);
uniqueness
proof
let X1,X2 be
set;
assume
A1: not thesis;
then
consider x be
object such that
A2: not (x
in X1 iff x
in X2) by
TARSKI: 2;
x
in X2 iff not ex f be
U-linear
Function of C1, C2 st x
= (
LinTrace f) by
A1,
A2;
hence thesis by
A1;
end;
existence
proof
defpred
P[
object] means ex f be
U-linear
Function of C1, C2 st $1
= (
LinTrace f);
consider X be
set such that
A3: for x be
object holds x
in X iff x
in (
bool
[:(
union C1), (
union C2):]) &
P[x] from
XBOOLE_0:sch 1;
take X;
let x be
set;
thus thesis by
A3;
end;
end
theorem ::
COHSP_1:53
Th53: for C1,C2 be
Coherence_Space holds for f be
c=-monotone
Function of C1, C2 holds for x1,x2 be
object st
{x1, x2}
in C1 holds for y1,y2 be
object st
[x1, y1]
in (
LinTrace f) &
[x2, y2]
in (
LinTrace f) holds
{y1, y2}
in C2
proof
let C1,C2 be
Coherence_Space;
let f be
c=-monotone
Function of C1, C2;
A1: (
dom f)
= C1 by
FUNCT_2:def 1;
let a1,a2 be
object;
assume
{a1, a2}
in C1;
then
reconsider a =
{a1, a2} as
Element of C1;
A2:
{a2}
c= a by
ZFMISC_1: 7;
then
{a2}
in C1 by
CLASSES1:def 1;
then
A3: (f
.
{a2})
c= (f
. a) by
A1,
A2,
Def11;
let y1,y2 be
object;
assume
[a1, y1]
in (
LinTrace f) &
[a2, y2]
in (
LinTrace f);
then
A4: y1
in (f
.
{a1}) & y2
in (f
.
{a2}) by
Th52;
A5:
{a1}
c= a by
ZFMISC_1: 7;
then
{a1}
in C1 by
CLASSES1:def 1;
then (f
.
{a1})
c= (f
. a) by
A1,
A5,
Def11;
then
{y1, y2}
c= (f
. a) by
A3,
A4,
ZFMISC_1: 32;
hence thesis by
CLASSES1:def 1;
end;
theorem ::
COHSP_1:54
Th54: for C1,C2 be
Coherence_Space holds for f be
cap-distributive
Function of C1, C2 holds for x1,x2 be
set st
{x1, x2}
in C1 holds for y be
object st
[x1, y]
in (
LinTrace f) &
[x2, y]
in (
LinTrace f) holds x1
= x2
proof
let C1,C2 be
Coherence_Space;
let f be
cap-distributive
Function of C1, C2;
let a1,a2 be
set;
set a =
{a1, a2};
assume
A1: a
in C1;
let y be
object;
A2: a
= (
{a1}
\/
{a2}) by
ENUMSET1: 1;
assume
[a1, y]
in (
LinTrace f) &
[a2, y]
in (
LinTrace f);
then
[
{a1}, y]
in (
Trace f) &
[
{a2}, y]
in (
Trace f) by
Th50;
then
{a1}
=
{a2} by
A1,
A2,
Th35;
hence thesis by
ZFMISC_1: 3;
end;
theorem ::
COHSP_1:55
Th55: for C1,C2 be
Coherence_Space holds for f,g be
U-linear
Function of C1, C2 st (
LinTrace f)
= (
LinTrace g) holds f
= g
proof
let C1,C2 be
Coherence_Space;
let f,g be
U-linear
Function of C1, C2;
assume
A1: (
LinTrace f)
= (
LinTrace g);
(
Trace f)
= (
Trace g)
proof
let a,y be
object;
reconsider aa = a as
set by
TARSKI: 1;
hereby
assume
A2:
[a, y]
in (
Trace f);
then
consider x be
set such that
A3: aa
=
{x} by
Th49;
[x, y]
in (
LinTrace f) by
A2,
A3,
Th50;
hence
[a, y]
in (
Trace g) by
A1,
A3,
Th50;
end;
assume
A4:
[a, y]
in (
Trace g);
then
consider x be
set such that
A5: aa
=
{x} by
Th49;
[x, y]
in (
LinTrace g) by
A4,
A5,
Th50;
hence thesis by
A1,
A5,
Th50;
end;
hence thesis by
Th37;
end;
Lm6: for C1,C2 be
Coherence_Space holds for X be
Subset of
[:(
union C1), (
union C2):] st (for a,b be
set st
{a, b}
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2) & (for a,b be
set st
{a, b}
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b) holds ex f be
U-linear
Function of C1, C2 st X
= (
LinTrace f) & for a be
Element of C1 holds (f
. a)
= (X
.: a)
proof
let C1,C2 be
Coherence_Space;
let X be
Subset of
[:(
union C1), (
union C2):] such that
A1: for a,b be
set st
{a, b}
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2 and
A2: for a,b be
set st
{a, b}
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b;
deffunc
f(
set) = (X
.: $1);
consider f be
Function such that
A3: (
dom f)
= C1 & for a be
set st a
in C1 holds (f
. a)
=
f(a) from
FUNCT_1:sch 5;
A4:
now
let a,y be
set;
assume that
A5: a
in (
dom f) and
A6: y
in (f
. a);
reconsider a9 = a as
Element of C1 by
A3,
A5;
y
in (X
.: a9) by
A3,
A6;
then
consider x be
object such that
A7:
[x, y]
in X and
A8: x
in a9 by
RELAT_1:def 13;
reconsider x as
set by
TARSKI: 1;
take x;
{x}
c= a9 by
A8,
ZFMISC_1: 31;
then
{x}
in C1 by
CLASSES1:def 1;
then x
in
{x} & (f
.
{x})
= (X
.:
{x}) by
A3,
TARSKI:def 1;
hence x
in a & y
in (f
.
{x}) by
A7,
A8,
RELAT_1:def 13;
let c be
set;
assume that
A9: c
c= a and
A10: y
in (f
. c);
c
c= a9 by
A9;
then c
in (
dom f) by
A3,
CLASSES1:def 1;
then y
in (X
.: c) by
A3,
A10;
then
consider z be
object such that
A11:
[z, y]
in X and
A12: z
in c by
RELAT_1:def 13;
{x, z}
c= a9 by
A8,
A9,
A12,
ZFMISC_1: 32;
then
{x, z}
in C1 by
CLASSES1:def 1;
hence x
in c by
A2,
A7,
A11,
A12;
end;
A13: (
rng f)
c= C2
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
rng f);
then
consider a be
object such that
A14: a
in (
dom f) and
A15: x
= (f
. a) by
FUNCT_1:def 3;
reconsider a as
Element of C1 by
A3,
A14;
A16: x
= (X
.: a) by
A3,
A15;
now
let z,y be
set;
assume z
in xx;
then
consider z1 be
object such that
A17:
[z1, z]
in X and
A18: z1
in a by
A16,
RELAT_1:def 13;
assume y
in xx;
then
consider y1 be
object such that
A19:
[y1, y]
in X and
A20: y1
in a by
A16,
RELAT_1:def 13;
A21: z1 is
set & y1 is
set by
TARSKI: 1;
{z1, y1}
in C1 by
A18,
A20,
COH_SP: 6;
hence
{z, y}
in C2 by
A1,
A17,
A19,
A21;
end;
hence thesis by
COH_SP: 6;
end;
f is
c=-monotone
proof
let a,b be
set;
assume that
A22: a
in (
dom f) & b
in (
dom f) and
A23: a
c= b;
reconsider a, b as
Element of C1 by
A3,
A22;
A24: (f
. a)
= (X
.: a) by
A3;
(X
.: a)
c= (X
.: b) by
A23,
RELAT_1: 123;
hence thesis by
A3,
A24;
end;
then
reconsider f as
U-linear
Function of C1, C2 by
A3,
A13,
A4,
Th23,
FUNCT_2:def 1,
RELSET_1: 4;
take f;
thus X
= (
LinTrace f)
proof
let a,b be
object;
hereby
assume
A25:
[a, b]
in X;
then a
in (
union C1) by
ZFMISC_1: 87;
then
consider a9 be
set such that
A26: a
in a9 and
A27: a9
in C1 by
TARSKI:def 4;
{a}
c= a9 by
A26,
ZFMISC_1: 31;
then
reconsider aa =
{a} as
Element of C1 by
A27,
CLASSES1:def 1;
A28: (f
. aa)
= (X
.: aa) & (f
.
{} )
=
{} by
A3,
Th18;
a
in
{a} by
TARSKI:def 1;
then b
in (X
.: aa) by
A25,
RELAT_1:def 13;
hence
[a, b]
in (
LinTrace f) by
A3,
A28,
Th51;
end;
assume
A29:
[a, b]
in (
LinTrace f);
then b
in (f
.
{a}) by
Th52;
then b
in (X
.:
{a}) by
A3,
A29,
Th52;
then ex x be
object st
[x, b]
in X & x
in
{a} by
RELAT_1:def 13;
hence thesis by
TARSKI:def 1;
end;
thus thesis by
A3;
end;
theorem ::
COHSP_1:56
Th56: for C1,C2 be
Coherence_Space holds for X be
Subset of
[:(
union C1), (
union C2):] st (for a,b be
set st
{a, b}
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2) & (for a,b be
set st
{a, b}
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b) holds ex f be
U-linear
Function of C1, C2 st X
= (
LinTrace f)
proof
let C1,C2 be
Coherence_Space;
let X be
Subset of
[:(
union C1), (
union C2):];
assume
A1: not thesis;
then ex f be
U-linear
Function of C1, C2 st X
= (
LinTrace f) & for a be
Element of C1 holds (f
. a)
= (X
.: a) by
Lm6;
hence thesis by
A1;
end;
theorem ::
COHSP_1:57
for C1,C2 be
Coherence_Space holds for f be
U-linear
Function of C1, C2 holds for a be
Element of C1 holds (f
. a)
= ((
LinTrace f)
.: a)
proof
let C1,C2 be
Coherence_Space;
let f be
U-linear
Function of C1, C2;
let a be
Element of C1;
set X = (
LinTrace f);
(for a,b be
set st
{a, b}
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2) & for a,b be
set st
{a, b}
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b by
Th53,
Th54;
then
consider g be
U-linear
Function of C1, C2 such that
A1: X
= (
LinTrace g) and
A2: for a be
Element of C1 holds (g
. a)
= (X
.: a) by
Lm6;
(g
. a)
= (X
.: a) by
A2;
hence thesis by
A1,
Th55;
end;
theorem ::
COHSP_1:58
for C1,C2 be
Coherence_Space holds ex f be
U-linear
Function of C1, C2 st (
LinTrace f)
=
{}
proof
let C1,C2 be
Coherence_Space;
reconsider X =
{} as
Subset of
[:(
union C1), (
union C2):] by
XBOOLE_1: 2;
(for a,b be
set st
{a, b}
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2) & for a,b be
set st
{a, b}
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b;
hence thesis by
Th56;
end;
theorem ::
COHSP_1:59
Th59: for C1,C2 be
Coherence_Space holds for x be
set, y be
set st x
in (
union C1) & y
in (
union C2) holds ex f be
U-linear
Function of C1, C2 st (
LinTrace f)
=
{
[x, y]}
proof
let C1,C2 be
Coherence_Space;
let a,y be
set;
assume that
A1: a
in (
union C1) and
A2: y
in (
union C2);
[a, y]
in
[:(
union C1), (
union C2):] by
A1,
A2,
ZFMISC_1: 87;
then
reconsider X =
{
[a, y]} as
Subset of
[:(
union C1), (
union C2):] by
ZFMISC_1: 31;
A3:
now
let a1,b be
set;
assume
{a1, b}
in C1;
let y1,y2 be
object;
assume that
A4:
[a1, y1]
in X and
A5:
[b, y2]
in X;
[b, y2]
=
[a, y] by
A5,
TARSKI:def 1;
then
A6: y2
= y by
XTUPLE_0: 1;
[a1, y1]
=
[a, y] by
A4,
TARSKI:def 1;
then y1
= y by
XTUPLE_0: 1;
then
{y1, y2}
=
{y} by
A6,
ENUMSET1: 29;
hence
{y1, y2}
in C2 by
A2,
COH_SP: 4;
end;
now
let a1,b be
set;
assume
{a1, b}
in C1;
let y1 be
object;
assume
[a1, y1]
in X &
[b, y1]
in X;
then
[a1, y1]
=
[a, y] &
[b, y1]
=
[a, y] by
TARSKI:def 1;
hence a1
= b by
XTUPLE_0: 1;
end;
hence thesis by
A3,
Th56;
end;
theorem ::
COHSP_1:60
for C1,C2 be
Coherence_Space holds for x be
set, y be
set st x
in (
union C1) holds for f be
U-linear
Function of C1, C2 st (
LinTrace f)
=
{
[x, y]} holds for a be
Element of C1 holds (x
in a implies (f
. a)
=
{y}) & ( not x
in a implies (f
. a)
=
{} )
proof
let C1,C2 be
Coherence_Space;
let a,y be
set;
assume a
in (
union C1);
then
reconsider a9 =
{a} as
Element of C1 by
COH_SP: 4;
let f be
U-linear
Function of C1, C2;
assume
A1: (
LinTrace f)
=
{
[a, y]};
let b be
Element of C1;
[a, y]
in (
LinTrace f) by
A1,
TARSKI:def 1;
then
A2: y
in (f
.
{a}) by
Th52;
hereby
A3: (f
. b)
c=
{y}
proof
let x be
object;
assume x
in (f
. b);
then
consider c be
Element of C1 such that
A4:
[c, x]
in (
Trace f) and c
c= b by
Th40;
consider d be
set such that
A5: c
=
{d} by
A4,
Th49;
[d, x]
in (
LinTrace f) by
A4,
A5,
Th50;
then
[d, x]
=
[a, y] by
A1,
TARSKI:def 1;
then x
= y by
XTUPLE_0: 1;
hence thesis by
TARSKI:def 1;
end;
assume a
in b;
then
A6: a9
c= b by
ZFMISC_1: 31;
(
dom f)
= C1 by
FUNCT_2:def 1;
then (f
. a9)
c= (f
. b) by
A6,
Def11;
then
{y}
c= (f
. b) by
A2,
ZFMISC_1: 31;
hence (f
. b)
=
{y} by
A3;
end;
assume that
A7: not a
in b and
A8: (f
. b)
<>
{} ;
reconsider B = (f
. b) as non
empty
set by
A8;
set z = the
Element of B;
consider c be
Element of C1 such that
A9:
[c, z]
in (
Trace f) and
A10: c
c= b by
Th40;
consider d be
set such that
A11: c
=
{d} by
A9,
Th49;
d
in c by
A11,
TARSKI:def 1;
then
A12: d
in b by
A10;
[d, z]
in (
LinTrace f) by
A9,
A11,
Th50;
then
[d, z]
=
[a, y] by
A1,
TARSKI:def 1;
hence thesis by
A7,
A12,
XTUPLE_0: 1;
end;
theorem ::
COHSP_1:61
Th61: for C1,C2 be
Coherence_Space holds for f be
U-linear
Function of C1, C2 holds for X be
Subset of (
LinTrace f) holds ex g be
U-linear
Function of C1, C2 st (
LinTrace g)
= X
proof
let C1,C2 be
Coherence_Space;
let f be
U-linear
Function of C1, C2;
let X be
Subset of (
LinTrace f);
A1: for a,b be
set st
{a, b}
in C1 holds for y be
object st
[a, y]
in X &
[b, y]
in X holds a
= b by
Th54;
X is
Subset of
[:(
union C1), (
union C2):] & for a,b be
set st
{a, b}
in C1 holds for y1,y2 be
object st
[a, y1]
in X &
[b, y2]
in X holds
{y1, y2}
in C2 by
Th53,
XBOOLE_1: 1;
hence thesis by
A1,
Th56;
end;
theorem ::
COHSP_1:62
Th62: for C1,C2 be
Coherence_Space holds for A be
set st for x,y be
set st x
in A & y
in A holds ex f be
U-linear
Function of C1, C2 st (x
\/ y)
= (
LinTrace f) holds ex f be
U-linear
Function of C1, C2 st (
union A)
= (
LinTrace f)
proof
let C1,C2 be
Coherence_Space;
let A be
set such that
A1: for x,y be
set st x
in A & y
in A holds ex f be
U-linear
Function of C1, C2 st (x
\/ y)
= (
LinTrace f);
set X = (
union A);
A2:
now
let a,b be
set such that
A3:
{a, b}
in C1;
let y1,y2 be
object;
assume
[a, y1]
in X;
then
consider x1 be
set such that
A4:
[a, y1]
in x1 and
A5: x1
in A by
TARSKI:def 4;
assume
[b, y2]
in X;
then
consider x2 be
set such that
A6:
[b, y2]
in x2 and
A7: x2
in A by
TARSKI:def 4;
A8: x1
c= (x1
\/ x2) & x2
c= (x1
\/ x2) by
XBOOLE_1: 7;
ex f be
U-linear
Function of C1, C2 st (x1
\/ x2)
= (
LinTrace f) by
A1,
A5,
A7;
hence
{y1, y2}
in C2 by
A3,
A4,
A6,
A8,
Th53;
end;
A9:
now
let a,b be
set such that
A10:
{a, b}
in C1;
let y be
object;
assume
[a, y]
in X;
then
consider x1 be
set such that
A11:
[a, y]
in x1 and
A12: x1
in A by
TARSKI:def 4;
assume
[b, y]
in X;
then
consider x2 be
set such that
A13:
[b, y]
in x2 and
A14: x2
in A by
TARSKI:def 4;
A15: x1
c= (x1
\/ x2) & x2
c= (x1
\/ x2) by
XBOOLE_1: 7;
ex f be
U-linear
Function of C1, C2 st (x1
\/ x2)
= (
LinTrace f) by
A1,
A12,
A14;
hence a
= b by
A10,
A11,
A13,
A15,
Th54;
end;
X
c=
[:(
union C1), (
union C2):]
proof
let x be
object;
assume x
in X;
then
consider y be
set such that
A16: x
in y and
A17: y
in A by
TARSKI:def 4;
(y
\/ y)
= y;
then ex f be
U-linear
Function of C1, C2 st y
= (
LinTrace f) by
A1,
A17;
hence thesis by
A16;
end;
hence thesis by
A2,
A9,
Th56;
end;
registration
let C1,C2 be
Coherence_Space;
cluster (
LinCoh (C1,C2)) -> non
empty
subset-closed
binary_complete;
coherence
proof
set C = (
LinCoh (C1,C2));
set f = the
U-linear
Function of C1, C2;
(
LinTrace f)
in C by
Def20;
hence C is non
empty;
thus C is
subset-closed
proof
let a,b be
set;
assume a
in C;
then
A1: ex f be
U-linear
Function of C1, C2 st a
= (
LinTrace f) by
Def20;
assume b
c= a;
then ex g be
U-linear
Function of C1, C2 st (
LinTrace g)
= b by
A1,
Th61;
hence thesis by
Def20;
end;
let A be
set;
assume
A2: for a,b be
set st a
in A & b
in A holds (a
\/ b)
in C;
now
let x,y be
set;
assume x
in A & y
in A;
then (x
\/ y)
in C by
A2;
hence ex f be
U-linear
Function of C1, C2 st (x
\/ y)
= (
LinTrace f) by
Def20;
end;
then ex f be
U-linear
Function of C1, C2 st (
union A)
= (
LinTrace f) by
Th62;
hence thesis by
Def20;
end;
end
theorem ::
COHSP_1:63
for C1,C2 be
Coherence_Space holds (
union (
LinCoh (C1,C2)))
=
[:(
union C1), (
union C2):]
proof
let C1,C2 be
Coherence_Space;
thus (
union (
LinCoh (C1,C2)))
c=
[:(
union C1), (
union C2):]
proof
let x be
object;
assume x
in (
union (
LinCoh (C1,C2)));
then
consider a be
set such that
A1: x
in a and
A2: a
in (
LinCoh (C1,C2)) by
TARSKI:def 4;
ex f be
U-linear
Function of C1, C2 st a
= (
LinTrace f) by
A2,
Def20;
hence thesis by
A1;
end;
let x,y be
object;
assume
A3:
[x, y]
in
[:(
union C1), (
union C2):];
then
A4: y
in (
union C2) by
ZFMISC_1: 87;
x
in (
union C1) by
A3,
ZFMISC_1: 87;
then ex f be
U-linear
Function of C1, C2 st (
LinTrace f)
=
{
[x, y]} by
A4,
Th59;
then
[x, y]
in
{
[x, y]} &
{
[x, y]}
in (
LinCoh (C1,C2)) by
Def20,
TARSKI:def 1;
hence thesis by
TARSKI:def 4;
end;
theorem ::
COHSP_1:64
for C1,C2 be
Coherence_Space holds for x1,x2 be
set, y1,y2 be
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
let C1,C2 be
Coherence_Space;
let x1,x2,y1,y2 be
set;
hereby
assume
[
[x1, y1],
[x2, y2]]
in (
Web (
LinCoh (C1,C2)));
then
{
[x1, y1],
[x2, y2]}
in (
LinCoh (C1,C2)) by
COH_SP: 5;
then
consider f be
U-linear
Function of C1, C2 such that
A1:
{
[x1, y1],
[x2, y2]}
= (
LinTrace f) by
Def20;
[x1, y1]
in (
LinTrace f) by
A1,
TARSKI:def 2;
then
A2:
[
{x1}, y1]
in (
Trace f) by
Th50;
then
A3:
{x1}
in (
dom f) by
Th31;
[x2, y2]
in (
LinTrace f) by
A1,
TARSKI:def 2;
then
A4:
[
{x2}, y2]
in (
Trace f) by
Th50;
then
A5:
{x2}
in (
dom f) by
Th31;
A6: x1
in
{x1} & x2
in
{x2} by
TARSKI:def 1;
A7: (
Trace f)
in (
StabCoh (C1,C2)) by
Def18;
A8: (
dom f)
= C1 by
FUNCT_2:def 1;
{
[
{x1}, y1],
[
{x2}, y2]}
c= (
Trace f) by
A2,
A4,
ZFMISC_1: 32;
then
{
[
{x1}, y1],
[
{x2}, y2]}
in (
StabCoh (C1,C2)) by
A7,
CLASSES1:def 1;
then
[
[
{x1}, y1],
[
{x2}, y2]]
in (
Web (
StabCoh (C1,C2))) by
COH_SP: 5;
then not (
{x1}
\/
{x2})
in C1 & y1
in (
union C2) & y2
in (
union C2) or
[y1, y2]
in (
Web C2) & (y1
= y2 implies
{x1}
=
{x2}) by
A3,
A5,
A8,
Th48;
then not
{x1, x2}
in C1 & y1
in (
union C2) & y2
in (
union C2) or
[y1, y2]
in (
Web C2) & (y1
= y2 implies x1
= x2) by
ENUMSET1: 1,
ZFMISC_1: 3;
hence 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)) by
A3,
A5,
A8,
A6,
COH_SP: 5,
TARSKI:def 4;
end;
assume x1
in (
union C1) & x2
in (
union C1);
then
reconsider a =
{x1}, b =
{x2} as
Element of C1 by
COH_SP: 4;
assume 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);
then not
{x1, x2}
in C1 & y1
in (
union C2) & y2
in (
union C2) or
[y1, y2]
in (
Web C2) & (y1
= y2 implies a
= b) by
COH_SP: 5;
then not (a
\/ b)
in C1 & y1
in (
union C2) & y2
in (
union C2) or
[y1, y2]
in (
Web C2) & (y1
= y2 implies a
= b) by
ENUMSET1: 1;
then
[
[a, y1],
[b, y2]]
in (
Web (
StabCoh (C1,C2))) by
Th48;
then
{
[a, y1],
[b, y2]}
in (
StabCoh (C1,C2)) by
COH_SP: 5;
then
consider f be
U-stable
Function of C1, C2 such that
A9:
{
[a, y1],
[b, y2]}
= (
Trace f) by
Def18;
now
let a1 be
set, y be
object;
assume
[a1, y]
in (
Trace f);
then
[a1, y]
=
[a, y1] or
[a1, y]
=
[b, y2] by
A9,
TARSKI:def 2;
then a1
=
{x1} or a1
=
{x2} by
XTUPLE_0: 1;
hence ex x be
set st a1
=
{x};
end;
then f is
U-linear by
Th49;
then
A10: (
LinTrace f)
in (
LinCoh (C1,C2)) by
Def20;
{
[x1, y1],
[x2, y2]}
c= (
LinTrace f)
proof
let x,y be
object;
assume
[x, y]
in
{
[x1, y1],
[x2, y2]};
then
[x, y]
=
[x1, y1] &
[a, y1]
in (
Trace f) or
[x, y]
=
[x2, y2] &
[b, y2]
in (
Trace f) by
A9,
TARSKI:def 2;
hence thesis by
Th50;
end;
then
{
[x1, y1],
[x2, y2]}
in (
LinCoh (C1,C2)) by
A10,
CLASSES1:def 1;
hence thesis by
COH_SP: 5;
end;
begin
definition
let C be
Coherence_Space;
::
COHSP_1:def21
func
'not' C ->
set equals { a where a be
Subset of (
union C) : for b be
Element of C holds ex x be
set st (a
/\ b)
c=
{x} };
correctness ;
end
theorem ::
COHSP_1:65
Th65: for C be
Coherence_Space, x be
set holds x
in (
'not' C) iff x
c= (
union C) & for a be
Element of C holds ex z be
set st (x
/\ a)
c=
{z}
proof
let C be
Coherence_Space, x be
set;
x
in (
'not' C) iff ex X be
Subset of (
union C) st x
= X & for a be
Element of C holds ex z be
set st (X
/\ a)
c=
{z};
hence thesis;
end;
registration
let C be
Coherence_Space;
cluster (
'not' C) -> non
empty
subset-closed
binary_complete;
coherence
proof
reconsider a =
{} as
Subset of (
union C) by
XBOOLE_1: 2;
now
let b be
Element of C;
take x =
{} ;
thus (a
/\ b)
c=
{x};
end;
then a
in (
'not' C);
hence (
'not' C) is non
empty;
hereby
let a,b be
set;
assume a
in (
'not' C);
then
consider aa be
Subset of (
union C) such that
A1: a
= aa and
A2: for b be
Element of C holds ex x be
set st (aa
/\ b)
c=
{x};
assume
A3: b
c= a;
then
reconsider bb = b as
Subset of (
union C) by
A1,
XBOOLE_1: 1;
now
let c be
Element of C;
consider x be
set such that
A4: (aa
/\ c)
c=
{x} by
A2;
take x;
(b
/\ c)
c= (a
/\ c) by
A3,
XBOOLE_1: 26;
hence (bb
/\ c)
c=
{x} by
A1,
A4;
end;
hence b
in (
'not' C);
end;
let A be
set such that
A5: for a,b be
set st a
in A & b
in A holds (a
\/ b)
in (
'not' C);
A
c= (
bool (
union C))
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in A;
then (xx
\/ xx)
in (
'not' C) by
A5;
then ex a be
Subset of (
union C) st x
= a & for b be
Element of C holds ex x be
set st (a
/\ b)
c=
{x};
hence thesis;
end;
then (
union A)
c= (
union (
bool (
union C))) by
ZFMISC_1: 77;
then
reconsider a = (
union A) as
Subset of (
union C) by
ZFMISC_1: 81;
now
let c be
Element of C;
per cases ;
suppose
A6: (a
/\ c)
=
{} ;
take x =
{} ;
thus (a
/\ c)
c=
{x} by
A6;
end;
suppose (a
/\ c)
<>
{} ;
then
reconsider X = (a
/\ c) as non
empty
set;
set x = the
Element of X;
reconsider y = x as
set;
take y;
thus (a
/\ c)
c=
{y}
proof
let z be
object;
assume
A7: z
in (a
/\ c);
then
A8: z
in c by
XBOOLE_0:def 4;
x
in a by
XBOOLE_0:def 4;
then
consider w be
set such that
A9: x
in w and
A10: w
in A by
TARSKI:def 4;
z
in a by
A7,
XBOOLE_0:def 4;
then
consider v be
set such that
A11: z
in v and
A12: v
in A by
TARSKI:def 4;
(w
\/ v)
in (
'not' C) by
A5,
A12,
A10;
then
consider aa be
Subset of (
union C) such that
A13: (w
\/ v)
= aa and
A14: for b be
Element of C holds ex x be
set st (aa
/\ b)
c=
{x};
consider t be
set such that
A15: (aa
/\ c)
c=
{t} by
A14;
x
in c & x
in aa by
A9,
A13,
XBOOLE_0:def 3,
XBOOLE_0:def 4;
then
A16: x
in (aa
/\ c) by
XBOOLE_0:def 4;
z
in aa by
A11,
A13,
XBOOLE_0:def 3;
then z
in (aa
/\ c) by
A8,
XBOOLE_0:def 4;
then z
in
{t} by
A15;
hence thesis by
A15,
A16,
TARSKI:def 1;
end;
end;
end;
hence thesis;
end;
end
theorem ::
COHSP_1:66
Th66: for C be
Coherence_Space holds (
union (
'not' C))
= (
union C)
proof
let C be
Coherence_Space;
hereby
let x be
object;
assume x
in (
union (
'not' C));
then
consider a be
set such that
A1: x
in a and
A2: a
in (
'not' C) by
TARSKI:def 4;
a
c= (
union C) by
A2,
Th65;
hence x
in (
union C) by
A1;
end;
let x be
object;
assume x
in (
union C);
then
A3:
{x}
c= (
union C) by
ZFMISC_1: 31;
for a be
Element of C holds ex z be
set st (
{x}
/\ a)
c=
{z}
proof
let a be
Element of C;
consider z be
object such that
A4: (
{x}
/\ a)
c=
{z} by
XBOOLE_1: 17;
reconsider z as
set by
TARSKI: 1;
take z;
thus thesis by
A4;
end;
then x
in
{x} &
{x}
in (
'not' C) by
A3,
ZFMISC_1: 31;
hence thesis by
TARSKI:def 4;
end;
theorem ::
COHSP_1:67
Th67: for C be
Coherence_Space, x,y be
set st x
<> y &
{x, y}
in C holds not
{x, y}
in (
'not' C)
proof
let C be
Coherence_Space, x,y be
set;
assume that
A1: x
<> y and
A2:
{x, y}
in C &
{x, y}
in (
'not' C);
consider z be
set such that
A3: (
{x, y}
/\
{x, y})
c=
{z} by
A2,
Th65;
x
= z by
A3,
ZFMISC_1: 20;
hence contradiction by
A1,
A3,
ZFMISC_1: 20;
end;
theorem ::
COHSP_1:68
Th68: for C be
Coherence_Space, x,y be
set st
{x, y}
c= (
union C) & not
{x, y}
in C holds
{x, y}
in (
'not' C)
proof
let C be
Coherence_Space, x,y be
set;
assume that
A1:
{x, y}
c= (
union C) and
A2: not
{x, y}
in C;
now
let a be
Element of C;
x
in a or not x
in a;
then
consider z be
set such that
A3: x
in a & z
= x or not x
in a & z
= y;
take z;
thus (
{x, y}
/\ a)
c=
{z}
proof
let v be
object;
assume
A4: v
in (
{x, y}
/\ a);
then
A5: v
in
{x, y} by
XBOOLE_0:def 4;
A6: v
in a by
A4,
XBOOLE_0:def 4;
per cases by
A5,
TARSKI:def 2;
suppose v
= x;
hence thesis by
A3,
A4,
TARSKI:def 1,
XBOOLE_0:def 4;
end;
suppose
A7: v
= y;
then x
in a implies
{x, y}
c= a by
A6,
ZFMISC_1: 32;
hence thesis by
A2,
A3,
A7,
CLASSES1:def 1,
TARSKI:def 1;
end;
end;
end;
hence thesis by
A1;
end;
theorem ::
COHSP_1:69
for C be
Coherence_Space holds for x,y be
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
let C be
Coherence_Space, x,y be
set;
A1:
{x, y}
c= (
union C) & not
{x, y}
in C implies
{x, y}
in (
'not' C) by
Th68;
A2: (
union (
'not' C))
= (
union C) by
Th66;
x
<> y &
{x, y}
in C implies not
{x, y}
in (
'not' C) by
Th67;
hence
[x, y]
in (
Web (
'not' C)) implies x
in (
union C) & y
in (
union C) & (x
= y or not
[x, y]
in (
Web C)) by
A2,
COH_SP: 5,
ZFMISC_1: 87;
assume that
A3: x
in (
union C) and
A4: y
in (
union C) and
A5: x
= y or not
[x, y]
in (
Web C);
x
= y &
{x}
in (
'not' C) &
{x}
=
{x, y} or not
{x, y}
in C by
A2,
A3,
A5,
COH_SP: 4,
COH_SP: 5,
ENUMSET1: 29;
hence thesis by
A1,
A3,
A4,
COH_SP: 5,
ZFMISC_1: 32;
end;
Lm7: for C be
Coherence_Space holds (
'not' (
'not' C))
c= C
proof
let C be
Coherence_Space;
let x be
object;
assume x
in (
'not' (
'not' C));
then
consider a be
Subset of (
union (
'not' C)) such that
A1: x
= a and
A2: for b be
Element of (
'not' C) holds ex x be
set st (a
/\ b)
c=
{x};
A3: (
union (
'not' C))
= (
union C) by
Th66;
now
let x,y be
set;
assume that
A4: x
in a and
A5: y
in a and
A6: not
{x, y}
in C;
{x, y}
c= (
union C) by
A3,
A4,
A5,
ZFMISC_1: 32;
then
{x, y}
in (
'not' C) by
A6,
Th68;
then
consider z be
set such that
A7: (a
/\
{x, y})
c=
{z} by
A2;
y
in
{x, y} by
TARSKI:def 2;
then y
in (a
/\
{x, y}) by
A5,
XBOOLE_0:def 4;
then
A8: y
= z by
A7,
TARSKI:def 1;
x
in
{x, y} by
TARSKI:def 2;
then x
in (a
/\
{x, y}) by
A4,
XBOOLE_0:def 4;
then x
= z by
A7,
TARSKI:def 1;
then
{x, y}
=
{x} by
A8,
ENUMSET1: 29;
hence contradiction by
A3,
A4,
A6,
COH_SP: 4;
end;
hence thesis by
A1,
COH_SP: 6;
end;
theorem ::
COHSP_1:70
Th70: for C be
Coherence_Space holds (
'not' (
'not' C))
= C
proof
let C be
Coherence_Space;
thus (
'not' (
'not' C))
c= C by
Lm7;
let a be
object;
reconsider aa = a as
set by
TARSKI: 1;
assume
A1: a
in C;
A2: (
union C)
= (
union (
'not' C)) & (
union (
'not' C))
= (
union (
'not' (
'not' C))) by
Th66;
now
let x,y be
set;
assume that
A3: x
in aa and
A4: y
in aa;
A5: x
in (
union C) by
A1,
A3,
TARSKI:def 4;
{x, y}
c= aa by
A3,
A4,
ZFMISC_1: 32;
then
{x, y}
in C by
A1,
CLASSES1:def 1;
then
A6: x
<> y implies not
{x, y}
in (
'not' C) by
Th67;
y
in (
union C) by
A1,
A4,
TARSKI:def 4;
then
A7:
{x, y}
c= (
union C) by
A5,
ZFMISC_1: 32;
{x, x}
=
{x} by
ENUMSET1: 29;
hence
{x, y}
in (
'not' (
'not' C)) by
A2,
A5,
A7,
A6,
Th68,
COH_SP: 4;
end;
hence thesis by
COH_SP: 6;
end;
theorem ::
COHSP_1:71
(
'not'
{
{} })
=
{
{} }
proof
(
union (
'not'
{
{} }))
= (
union
{
{} }) by
Th66
.=
{} by
ZFMISC_1: 25;
hence (
'not'
{
{} })
c=
{
{} } by
ZFMISC_1: 1,
ZFMISC_1: 82;
{}
in (
'not'
{
{} }) by
COH_SP: 1;
hence thesis by
ZFMISC_1: 31;
end;
theorem ::
COHSP_1:72
for X be
set holds (
'not' (
FlatCoh X))
= (
bool X) & (
'not' (
bool X))
= (
FlatCoh X)
proof
let X be
set;
thus (
'not' (
FlatCoh X))
= (
bool X)
proof
hereby
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
'not' (
FlatCoh X));
then xx
c= (
union (
FlatCoh X)) by
Th65;
then xx
c= X by
Th2;
hence x
in (
bool X);
end;
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
A1:
now
let a be
Element of (
FlatCoh X);
per cases by
Th1;
suppose a
=
{} ;
then (xx
/\ a)
c=
{
0 };
hence ex z be
set st (xx
/\ a)
c=
{z};
end;
suppose ex z be
set st a
=
{z} & z
in X;
then
consider z be
set such that
A2: a
=
{z} and z
in X;
take z;
thus (xx
/\ a)
c=
{z} by
A2,
XBOOLE_1: 17;
end;
end;
assume x
in (
bool X);
then xx
c= X;
then xx
c= (
union (
FlatCoh X)) by
Th2;
hence thesis by
A1;
end;
hence thesis by
Th70;
end;
begin
definition
let x,y be
set;
::
COHSP_1:def22
func x
U+ y ->
set equals (
Union (
disjoin
<*x, y*>));
correctness ;
end
theorem ::
COHSP_1:73
Th73: for x,y be
set holds (x
U+ y)
= (
[:x,
{1}:]
\/
[:y,
{2}:])
proof
let x,y be
set;
(
len
<*x, y*>)
= 2 by
FINSEQ_1: 44;
then
A1: (
dom
<*x, y*>)
=
{1, 2} by
FINSEQ_1: 2,
FINSEQ_1:def 3;
now
let z be
object;
A2: (z
`2 )
in
{1, 2} iff (z
`2 )
= 1 or (z
`2 )
= 2 by
TARSKI:def 2;
A3: z
in
[:x,
{1}:] iff (z
`1 )
in x & (z
`2 )
= 1 & z
=
[(z
`1 ), (z
`2 )] by
MCART_1: 13,
MCART_1: 21,
ZFMISC_1: 106;
A4: z
in
[:y,
{2}:] iff (z
`1 )
in y & (z
`2 )
= 2 & z
=
[(z
`1 ), (z
`2 )] by
MCART_1: 13,
MCART_1: 21,
ZFMISC_1: 106;
z
in (x
U+ y) iff (z
`2 )
in
{1, 2} & (z
`1 )
in (
<*x, y*>
. (z
`2 )) & z
=
[(z
`1 ), (z
`2 )] by
A1,
CARD_3: 22;
hence z
in (x
U+ y) iff z
in (
[:x,
{1}:]
\/
[:y,
{2}:]) by
A2,
A3,
A4,
FINSEQ_1: 44,
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
COHSP_1:74
Th74: for x be
set holds (x
U+
{} )
=
[:x,
{1}:] & (
{}
U+ x)
=
[:x,
{2}:]
proof
let x be
set;
thus (x
U+
{} )
= (
[:x,
{1}:]
\/
[:
{} ,
{2}:]) by
Th73
.= (
[:x,
{1}:]
\/
{} ) by
ZFMISC_1: 90
.=
[:x,
{1}:];
thus (
{}
U+ x)
= (
[:
{} ,
{1}:]
\/
[:x,
{2}:]) by
Th73
.= (
{}
\/
[:x,
{2}:]) by
ZFMISC_1: 90
.=
[:x,
{2}:];
end;
theorem ::
COHSP_1:75
Th75: for x,y,z be
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)
proof
let x,y,z be
set;
assume z
in (x
U+ y);
then z
in (
[:x,
{1}:]
\/
[:y,
{2}:]) by
Th73;
then z
in
[:x,
{1}:] or z
in
[:y,
{2}:] by
XBOOLE_0:def 3;
hence thesis by
MCART_1: 13,
MCART_1: 21;
end;
theorem ::
COHSP_1:76
Th76: for x,y be
set, z be
object holds
[z, 1]
in (x
U+ y) iff z
in x
proof
let x,y be
set, z be
object;
(x
U+ y)
= (
[:x,
{1}:]
\/
[:y,
{2}:]) by
Th73;
then
[z, 1]
in (x
U+ y) iff
[z, 1]
in
[:x,
{1}:] or
[z, 1]
in
[:y,
{2}:] & 1
<> 2 by
XBOOLE_0:def 3;
hence thesis by
ZFMISC_1: 106;
end;
theorem ::
COHSP_1:77
Th77: for x,y be
set, z be
object holds
[z, 2]
in (x
U+ y) iff z
in y
proof
let x,y be
set, z be
object;
(x
U+ y)
= (
[:x,
{1}:]
\/
[:y,
{2}:]) by
Th73;
then
[z, 2]
in (x
U+ y) iff
[z, 2]
in
[:x,
{1}:] & 1
<> 2 or
[z, 2]
in
[:y,
{2}:] by
XBOOLE_0:def 3;
hence thesis by
ZFMISC_1: 106;
end;
theorem ::
COHSP_1:78
Th78: for x1,y1,x2,y2 be
set holds (x1
U+ y1)
c= (x2
U+ y2) iff x1
c= x2 & y1
c= y2
proof
let x1,y1,x2,y2 be
set;
hereby
assume
A1: (x1
U+ y1)
c= (x2
U+ y2);
thus x1
c= x2
proof
let a be
object;
assume a
in x1;
then
[a, 1]
in (x1
U+ y1) by
Th76;
hence thesis by
A1,
Th76;
end;
thus y1
c= y2
proof
let a be
object;
assume a
in y1;
then
[a, 2]
in (x1
U+ y1) by
Th77;
hence thesis by
A1,
Th77;
end;
end;
assume
A2: x1
c= x2 & y1
c= y2;
let a be
object;
assume
A3: a
in (x1
U+ y1);
then
A4: (a
`2 )
= 1 & (a
`1 )
in x1 or (a
`2 )
= 2 & (a
`1 )
in y1 by
Th75;
a
=
[(a
`1 ), (a
`2 )] by
A3,
Th75;
hence thesis by
A2,
A4,
Th76,
Th77;
end;
theorem ::
COHSP_1:79
Th79: for x,y,z be
set st z
c= (x
U+ y) holds ex x1,y1 be
set st z
= (x1
U+ y1) & x1
c= x & y1
c= y
proof
let x,y,z be
set;
assume
A1: z
c= (x
U+ y);
take x1 = (
proj1 (z
/\
[:x,
{1}:])), y1 = (
proj1 (z
/\
[:y,
{2}:]));
A2: (x
U+ y)
= (
[:x,
{1}:]
\/
[:y,
{2}:]) by
Th73;
thus z
= (x1
U+ y1)
proof
hereby
let a be
object;
assume
A3: a
in z;
then
A4: a
=
[(a
`1 ), (a
`2 )] by
A1,
Th75;
a
in
[:x,
{1}:] or a
in
[:y,
{2}:] by
A1,
A2,
A3,
XBOOLE_0:def 3;
then a
in (z
/\
[:x,
{1}:]) & (a
`2 )
= 1 or a
in (z
/\
[:y,
{2}:]) & (a
`2 )
= 2 by
A3,
A4,
XBOOLE_0:def 4,
ZFMISC_1: 106;
then (a
`1 )
in x1 & (a
`2 )
= 1 or (a
`1 )
in y1 & (a
`2 )
= 2 by
A4,
XTUPLE_0:def 12;
hence a
in (x1
U+ y1) by
A4,
Th76,
Th77;
end;
let a be
object;
assume
A5: a
in (x1
U+ y1);
then
A6: a
=
[(a
`1 ), (a
`2 )] by
Th75;
per cases by
A5,
Th75;
suppose
A7: (a
`2 )
= 1 & (a
`1 )
in x1;
then
consider b be
object such that
A8:
[(a
`1 ), b]
in (z
/\
[:x,
{1}:]) by
XTUPLE_0:def 12;
[(a
`1 ), b]
in z &
[(a
`1 ), b]
in
[:x,
{1}:] by
A8,
XBOOLE_0:def 4;
hence thesis by
A6,
A7,
ZFMISC_1: 106;
end;
suppose
A9: (a
`2 )
= 2 & (a
`1 )
in y1;
then
consider b be
object such that
A10:
[(a
`1 ), b]
in (z
/\
[:y,
{2}:]) by
XTUPLE_0:def 12;
[(a
`1 ), b]
in z &
[(a
`1 ), b]
in
[:y,
{2}:] by
A10,
XBOOLE_0:def 4;
hence thesis by
A6,
A9,
ZFMISC_1: 106;
end;
end;
(z
/\
[:y,
{2}:])
c=
[:y,
{2}:] by
XBOOLE_1: 17;
then
A11: y1
c= (
proj1
[:y,
{2}:]) by
XTUPLE_0: 8;
(z
/\
[:x,
{1}:])
c=
[:x,
{1}:] by
XBOOLE_1: 17;
then x1
c= (
proj1
[:x,
{1}:]) by
XTUPLE_0: 8;
hence thesis by
A11,
FUNCT_5: 9;
end;
theorem ::
COHSP_1:80
Th80: for x1,y1,x2,y2 be
set holds (x1
U+ y1)
= (x2
U+ y2) iff x1
= x2 & y1
= y2 by
Th78;
theorem ::
COHSP_1:81
Th81: for x1,y1,x2,y2 be
set holds ((x1
U+ y1)
\/ (x2
U+ y2))
= ((x1
\/ x2)
U+ (y1
\/ y2))
proof
let x1,y1,x2,y2 be
set;
set X1 =
[:x1,
{1}:], X2 =
[:x2,
{1}:];
set Y1 =
[:y1,
{2}:], Y2 =
[:y2,
{2}:];
set X =
[:(x1
\/ x2),
{1}:], Y =
[:(y1
\/ y2),
{2}:];
A1: X
= (X1
\/ X2) by
ZFMISC_1: 97;
A2: ((x1
\/ x2)
U+ (y1
\/ y2))
= (X
\/ Y) & Y
= (Y1
\/ Y2) by
Th73,
ZFMISC_1: 97;
(x1
U+ y1)
= (X1
\/ Y1) & (x2
U+ y2)
= (X2
\/ Y2) by
Th73;
hence ((x1
U+ y1)
\/ (x2
U+ y2))
= (((X1
\/ Y1)
\/ X2)
\/ Y2) by
XBOOLE_1: 4
.= ((X
\/ Y1)
\/ Y2) by
A1,
XBOOLE_1: 4
.= ((x1
\/ x2)
U+ (y1
\/ y2)) by
A2,
XBOOLE_1: 4;
end;
theorem ::
COHSP_1:82
Th82: for x1,y1,x2,y2 be
set holds ((x1
U+ y1)
/\ (x2
U+ y2))
= ((x1
/\ x2)
U+ (y1
/\ y2))
proof
let x1,y1,x2,y2 be
set;
set X1 =
[:x1,
{1}:], X2 =
[:x2,
{1}:];
set Y1 =
[:y1,
{2}:], Y2 =
[:y2,
{2}:];
set X =
[:(x1
/\ x2),
{1}:], Y =
[:(y1
/\ y2),
{2}:];
A1: X
= (X1
/\ X2) by
ZFMISC_1: 99;
A2:
{1}
misses
{2} by
ZFMISC_1: 11;
then Y1
misses X2 by
ZFMISC_1: 104;
then
A3: Y
= (Y1
/\ Y2) & (Y1
/\ X2)
=
{} by
ZFMISC_1: 99;
X1
misses Y2 by
A2,
ZFMISC_1: 104;
then
A4: (X1
/\ Y2)
=
{} ;
(x1
U+ y1)
= (X1
\/ Y1) & (x2
U+ y2)
= (X2
\/ Y2) by
Th73;
hence ((x1
U+ y1)
/\ (x2
U+ y2))
= (((X1
\/ Y1)
/\ X2)
\/ ((X1
\/ Y1)
/\ Y2)) by
XBOOLE_1: 23
.= ((X
\/ (Y1
/\ X2))
\/ ((X1
\/ Y1)
/\ Y2)) by
A1,
XBOOLE_1: 23
.= (X
\/ ((X1
/\ Y2)
\/ Y)) by
A3,
XBOOLE_1: 23
.= ((x1
/\ x2)
U+ (y1
/\ y2)) by
A4,
Th73;
end;
definition
let C1,C2 be
Coherence_Space;
::
COHSP_1:def23
func C1
"/\" C2 ->
set equals the set of all (a
U+ b) where a be
Element of C1, b be
Element of C2;
correctness ;
::
COHSP_1:def24
func C1
"\/" C2 ->
set equals ( the set of all (a
U+
{} ) where a be
Element of C1
\/ the set of all (
{}
U+ b) where b be
Element of C2);
correctness ;
end
theorem ::
COHSP_1:83
Th83: for C1,C2 be
Coherence_Space holds for x be
object holds x
in (C1
"/\" C2) iff ex a be
Element of C1, b be
Element of C2 st x
= (a
U+ b);
theorem ::
COHSP_1:84
Th84: for C1,C2 be
Coherence_Space holds for x,y be
set holds (x
U+ y)
in (C1
"/\" C2) iff x
in C1 & y
in C2
proof
let C1,C2 be
Coherence_Space, x,y be
set;
now
given a be
Element of C1, b be
Element of C2 such that
A1: (x
U+ y)
= (a
U+ b);
take a, b;
thus x
= a & y
= b by
A1,
Th80;
end;
hence thesis;
end;
theorem ::
COHSP_1:85
Th85: for C1,C2 be
Coherence_Space holds (
union (C1
"/\" C2))
= ((
union C1)
U+ (
union C2))
proof
let C1,C2 be
Coherence_Space;
thus (
union (C1
"/\" C2))
c= ((
union C1)
U+ (
union C2))
proof
let x be
object;
assume x
in (
union (C1
"/\" C2));
then
consider a be
set such that
A1: x
in a and
A2: a
in (C1
"/\" C2) by
TARSKI:def 4;
consider a1 be
Element of C1, a2 be
Element of C2 such that
A3: a
= (a1
U+ a2) by
A2;
a1
c= (
union C1) & a2
c= (
union C2) by
ZFMISC_1: 74;
then a
c= ((
union C1)
U+ (
union C2)) by
A3,
Th78;
hence thesis by
A1;
end;
let z be
object;
assume
A4: z
in ((
union C1)
U+ (
union C2));
then
A5: z
=
[(z
`1 ), (z
`2 )] by
Th75;
per cases by
A4,
Th75;
suppose
A6: (z
`2 )
= 1 & (z
`1 )
in (
union C1);
set b = the
Element of C2;
consider a be
set such that
A7: (z
`1 )
in a and
A8: a
in C1 by
A6,
TARSKI:def 4;
reconsider a as
Element of C1 by
A8;
A9: (a
U+ b)
in (C1
"/\" C2);
z
in (a
U+ b) by
A5,
A6,
A7,
Th76;
hence thesis by
A9,
TARSKI:def 4;
end;
suppose
A10: (z
`2 )
= 2 & (z
`1 )
in (
union C2);
set b = the
Element of C1;
consider a be
set such that
A11: (z
`1 )
in a and
A12: a
in C2 by
A10,
TARSKI:def 4;
reconsider a as
Element of C2 by
A12;
A13: (b
U+ a)
in (C1
"/\" C2);
z
in (b
U+ a) by
A5,
A10,
A11,
Th77;
hence thesis by
A13,
TARSKI:def 4;
end;
end;
theorem ::
COHSP_1:86
Th86: for C1,C2 be
Coherence_Space holds for x,y be
set holds (x
U+ y)
in (C1
"\/" C2) iff x
in C1 & y
=
{} or x
=
{} & y
in C2
proof
let C1,C2 be
Coherence_Space, x,y be
set;
A1:
now
given a be
Element of C1 such that
A2: (x
U+ y)
= (a
U+
{} );
x
= a by
A2,
Th80;
hence x
in C1 & y
=
{} by
A2,
Th80;
end;
A3:
now
given a be
Element of C2 such that
A4: (x
U+ y)
= (
{}
U+ a);
y
= a by
A4,
Th80;
hence y
in C2 & x
=
{} by
A4,
Th80;
end;
(x
U+ y)
in (C1
"\/" C2) iff (x
U+ y)
in the set of all (a
U+
{} ) where a be
Element of C1 or (x
U+ y)
in the set of all (
{}
U+ b) where b be
Element of C2 by
XBOOLE_0:def 3;
hence thesis by
A1,
A3;
end;
theorem ::
COHSP_1:87
Th87: for C1,C2 be
Coherence_Space holds for x be
set st x
in (C1
"\/" C2) holds ex a be
Element of C1, b be
Element of C2 st x
= (a
U+ b) & (a
=
{} or b
=
{} )
proof
let C1,C2 be
Coherence_Space, x be
set;
assume x
in (C1
"\/" C2);
then x
in the set of all (a
U+
{} ) where a be
Element of C1 or x
in the set of all (
{}
U+ b) where b be
Element of C2 by
XBOOLE_0:def 3;
then
{}
in C2 & (ex a be
Element of C1 st x
= (a
U+
{} )) or
{}
in C1 & ex b be
Element of C2 st x
= (
{}
U+ b) by
COH_SP: 1;
hence thesis;
end;
theorem ::
COHSP_1:88
for C1,C2 be
Coherence_Space holds (
union (C1
"\/" C2))
= ((
union C1)
U+ (
union C2))
proof
let C1,C2 be
Coherence_Space;
thus (
union (C1
"\/" C2))
c= ((
union C1)
U+ (
union C2))
proof
let x be
object;
assume x
in (
union (C1
"\/" C2));
then
consider a be
set such that
A1: x
in a and
A2: a
in (C1
"\/" C2) by
TARSKI:def 4;
consider a1 be
Element of C1, a2 be
Element of C2 such that
A3: a
= (a1
U+ a2) and a1
=
{} or a2
=
{} by
A2,
Th87;
a1
c= (
union C1) & a2
c= (
union C2) by
ZFMISC_1: 74;
then a
c= ((
union C1)
U+ (
union C2)) by
A3,
Th78;
hence thesis by
A1;
end;
let z be
object;
assume
A4: z
in ((
union C1)
U+ (
union C2));
then
A5: z
=
[(z
`1 ), (z
`2 )] by
Th75;
per cases by
A4,
Th75;
suppose
A6: (z
`2 )
= 1 & (z
`1 )
in (
union C1);
reconsider b =
{} as
Element of C2 by
COH_SP: 1;
consider a be
set such that
A7: (z
`1 )
in a and
A8: a
in C1 by
A6,
TARSKI:def 4;
reconsider a as
Element of C1 by
A8;
A9: (a
U+ b)
in (C1
"\/" C2) by
Th86;
z
in (a
U+ b) by
A5,
A6,
A7,
Th76;
hence thesis by
A9,
TARSKI:def 4;
end;
suppose
A10: (z
`2 )
= 2 & (z
`1 )
in (
union C2);
reconsider b =
{} as
Element of C1 by
COH_SP: 1;
consider a be
set such that
A11: (z
`1 )
in a and
A12: a
in C2 by
A10,
TARSKI:def 4;
reconsider a as
Element of C2 by
A12;
A13: (b
U+ a)
in (C1
"\/" C2) by
Th86;
z
in (b
U+ a) by
A5,
A10,
A11,
Th77;
hence thesis by
A13,
TARSKI:def 4;
end;
end;
registration
let C1,C2 be
Coherence_Space;
cluster (C1
"/\" C2) -> non
empty
subset-closed
binary_complete;
coherence
proof
set a9 = the
Element of C1, b9 = the
Element of C2;
(a9
U+ b9)
in (C1
"/\" C2);
hence (C1
"/\" C2) is non
empty;
hereby
let a,b be
set;
assume a
in (C1
"/\" C2);
then
consider aa be
Element of C1, bb be
Element of C2 such that
A1: a
= (aa
U+ bb);
assume b
c= a;
then
consider x1,y1 be
set such that
A2: b
= (x1
U+ y1) and
A3: x1
c= aa & y1
c= bb by
A1,
Th79;
x1
in C1 & y1
in C2 by
A3,
CLASSES1:def 1;
hence b
in (C1
"/\" C2) by
A2;
end;
let A be
set such that
A4: for a,b be
set st a
in A & b
in A holds (a
\/ b)
in (C1
"/\" C2);
set A2 = { b where b be
Element of C2 : ex a be
Element of C1 st (a
U+ b)
in A };
now
let x,y be
set;
assume x
in A2;
then
consider ax be
Element of C2 such that
A5: x
= ax and
A6: ex b be
Element of C1 st (b
U+ ax)
in A;
consider bx be
Element of C1 such that
A7: (bx
U+ ax)
in A by
A6;
assume y
in A2;
then
consider ay be
Element of C2 such that
A8: y
= ay and
A9: ex b be
Element of C1 st (b
U+ ay)
in A;
consider by1 be
Element of C1 such that
A10: (by1
U+ ay)
in A by
A9;
((bx
U+ ax)
\/ (by1
U+ ay))
in (C1
"/\" C2) by
A4,
A7,
A10;
then ((bx
\/ by1)
U+ (ax
\/ ay))
in (C1
"/\" C2) by
Th81;
hence (x
\/ y)
in C2 by
A5,
A8,
Th84;
end;
then
A11: (
union A2)
in C2 by
Def1;
set A1 = { a where a be
Element of C1 : ex b be
Element of C2 st (a
U+ b)
in A };
A12: ((
union A1)
U+ (
union A2))
= (
union A)
proof
hereby
let x be
object;
assume
A13: x
in ((
union A1)
U+ (
union A2));
then
A14: x
=
[(x
`1 ), (x
`2 )] by
Th75;
per cases by
A13,
Th75;
suppose
A15: (x
`2 )
= 1 & (x
`1 )
in (
union A1);
then
consider a be
set such that
A16: (x
`1 )
in a and
A17: a
in A1 by
TARSKI:def 4;
consider ax be
Element of C1 such that
A18: a
= ax and
A19: ex b be
Element of C2 st (ax
U+ b)
in A by
A17;
consider bx be
Element of C2 such that
A20: (ax
U+ bx)
in A by
A19;
x
in (ax
U+ bx) by
A14,
A15,
A16,
A18,
Th76;
hence x
in (
union A) by
A20,
TARSKI:def 4;
end;
suppose
A21: (x
`2 )
= 2 & (x
`1 )
in (
union A2);
then
consider a be
set such that
A22: (x
`1 )
in a and
A23: a
in A2 by
TARSKI:def 4;
consider bx be
Element of C2 such that
A24: a
= bx and
A25: ex a be
Element of C1 st (a
U+ bx)
in A by
A23;
consider ax be
Element of C1 such that
A26: (ax
U+ bx)
in A by
A25;
x
in (ax
U+ bx) by
A14,
A21,
A22,
A24,
Th77;
hence x
in (
union A) by
A26,
TARSKI:def 4;
end;
end;
let x be
object;
assume x
in (
union A);
then
consider a be
set such that
A27: x
in a and
A28: a
in A by
TARSKI:def 4;
(a
\/ a)
in (C1
"/\" C2) by
A4,
A28;
then
consider aa be
Element of C1, bb be
Element of C2 such that
A29: a
= (aa
U+ bb);
bb
in A2 by
A28,
A29;
then
A30: bb
c= (
union A2) by
ZFMISC_1: 74;
aa
in A1 by
A28,
A29;
then aa
c= (
union A1) by
ZFMISC_1: 74;
then (aa
U+ bb)
c= ((
union A1)
U+ (
union A2)) by
A30,
Th78;
hence thesis by
A27,
A29;
end;
now
let x,y be
set;
assume x
in A1;
then
consider ax be
Element of C1 such that
A31: x
= ax and
A32: ex b be
Element of C2 st (ax
U+ b)
in A;
consider bx be
Element of C2 such that
A33: (ax
U+ bx)
in A by
A32;
assume y
in A1;
then
consider ay be
Element of C1 such that
A34: y
= ay and
A35: ex b be
Element of C2 st (ay
U+ b)
in A;
consider by1 be
Element of C2 such that
A36: (ay
U+ by1)
in A by
A35;
((ax
U+ bx)
\/ (ay
U+ by1))
in (C1
"/\" C2) by
A4,
A33,
A36;
then ((ax
\/ ay)
U+ (bx
\/ by1))
in (C1
"/\" C2) by
Th81;
hence (x
\/ y)
in C1 by
A31,
A34,
Th84;
end;
then (
union A1)
in C1 by
Def1;
hence thesis by
A11,
A12;
end;
cluster (C1
"\/" C2) -> non
empty
subset-closed
binary_complete;
coherence
proof
set a9 = the
Element of C1;
(a9
U+
{} )
in (C1
"\/" C2) by
Th86;
hence (C1
"\/" C2) is non
empty;
hereby
let a,b be
set;
assume a
in (C1
"\/" C2);
then
consider aa be
Element of C1, bb be
Element of C2 such that
A37: a
= (aa
U+ bb) and
A38: aa
=
{} or bb
=
{} by
Th87;
assume b
c= a;
then
consider x1,y1 be
set such that
A39: b
= (x1
U+ y1) and
A40: x1
c= aa & y1
c= bb by
A37,
Th79;
A41: x1
in C1 & y1
in C2 by
A40,
CLASSES1:def 1;
x1
=
{} or y1
=
{} by
A38,
A40;
hence b
in (C1
"\/" C2) by
A39,
A41,
Th86;
end;
let A be
set;
set A1 = { a where a be
Element of C1 : ex b be
Element of C2 st (a
U+ b)
in A };
set A2 = { b where b be
Element of C2 : ex a be
Element of C1 st (a
U+ b)
in A };
assume
A42: for a,b be
set st a
in A & b
in A holds (a
\/ b)
in (C1
"\/" C2);
now
let x,y be
set;
assume x
in A2;
then
consider ax be
Element of C2 such that
A43: x
= ax and
A44: ex b be
Element of C1 st (b
U+ ax)
in A;
consider bx be
Element of C1 such that
A45: (bx
U+ ax)
in A by
A44;
assume y
in A2;
then
consider ay be
Element of C2 such that
A46: y
= ay and
A47: ex b be
Element of C1 st (b
U+ ay)
in A;
consider by1 be
Element of C1 such that
A48: (by1
U+ ay)
in A by
A47;
((bx
U+ ax)
\/ (by1
U+ ay))
in (C1
"\/" C2) by
A42,
A45,
A48;
then ((bx
\/ by1)
U+ (ax
\/ ay))
in (C1
"\/" C2) by
Th81;
then (x
\/ y)
in C2 or (x
\/ y)
=
{} by
A43,
A46,
Th86;
hence (x
\/ y)
in C2 by
COH_SP: 1;
end;
then
A49: (
union A2)
in C2 by
Def1;
A50: ((
union A1)
U+ (
union A2))
= (
union A)
proof
hereby
let x be
object;
assume
A51: x
in ((
union A1)
U+ (
union A2));
then
A52: x
=
[(x
`1 ), (x
`2 )] by
Th75;
per cases by
A51,
Th75;
suppose
A53: (x
`2 )
= 1 & (x
`1 )
in (
union A1);
then
consider a be
set such that
A54: (x
`1 )
in a and
A55: a
in A1 by
TARSKI:def 4;
consider ax be
Element of C1 such that
A56: a
= ax and
A57: ex b be
Element of C2 st (ax
U+ b)
in A by
A55;
consider bx be
Element of C2 such that
A58: (ax
U+ bx)
in A by
A57;
x
in (ax
U+ bx) by
A52,
A53,
A54,
A56,
Th76;
hence x
in (
union A) by
A58,
TARSKI:def 4;
end;
suppose
A59: (x
`2 )
= 2 & (x
`1 )
in (
union A2);
then
consider a be
set such that
A60: (x
`1 )
in a and
A61: a
in A2 by
TARSKI:def 4;
consider bx be
Element of C2 such that
A62: a
= bx and
A63: ex a be
Element of C1 st (a
U+ bx)
in A by
A61;
consider ax be
Element of C1 such that
A64: (ax
U+ bx)
in A by
A63;
x
in (ax
U+ bx) by
A52,
A59,
A60,
A62,
Th77;
hence x
in (
union A) by
A64,
TARSKI:def 4;
end;
end;
let x be
object;
assume x
in (
union A);
then
consider a be
set such that
A65: x
in a and
A66: a
in A by
TARSKI:def 4;
(a
\/ a)
in (C1
"\/" C2) by
A42,
A66;
then
consider aa be
Element of C1, bb be
Element of C2 such that
A67: a
= (aa
U+ bb) and aa
=
{} or bb
=
{} by
Th87;
bb
in A2 by
A66,
A67;
then
A68: bb
c= (
union A2) by
ZFMISC_1: 74;
aa
in A1 by
A66,
A67;
then aa
c= (
union A1) by
ZFMISC_1: 74;
then (aa
U+ bb)
c= ((
union A1)
U+ (
union A2)) by
A68,
Th78;
hence thesis by
A65,
A67;
end;
A69:
now
assume (
union A1)
<>
{} ;
then
reconsider AA = (
union A1) as non
empty
set;
set aa = the
Element of AA;
consider x be
set such that
A70: aa
in x and
A71: x
in A1 by
TARSKI:def 4;
consider ax be
Element of C1 such that
A72: x
= ax and
A73: ex b be
Element of C2 st (ax
U+ b)
in A by
A71;
consider bx be
Element of C2 such that
A74: (ax
U+ bx)
in A by
A73;
assume (
union A2)
<>
{} ;
then
reconsider AA = (
union A2) as non
empty
set;
set bb = the
Element of AA;
consider y be
set such that
A75: bb
in y and
A76: y
in A2 by
TARSKI:def 4;
consider by1 be
Element of C2 such that
A77: y
= by1 and
A78: ex a be
Element of C1 st (a
U+ by1)
in A by
A76;
consider ay be
Element of C1 such that
A79: (ay
U+ by1)
in A by
A78;
((ax
U+ bx)
\/ (ay
U+ by1))
in (C1
"\/" C2) by
A42,
A74,
A79;
then ((ax
\/ ay)
U+ (bx
\/ by1))
in (C1
"\/" C2) by
Th81;
hence contradiction by
A70,
A72,
A75,
A77,
Th86;
end;
now
let x,y be
set;
assume x
in A1;
then
consider ax be
Element of C1 such that
A80: x
= ax and
A81: ex b be
Element of C2 st (ax
U+ b)
in A;
consider bx be
Element of C2 such that
A82: (ax
U+ bx)
in A by
A81;
assume y
in A1;
then
consider ay be
Element of C1 such that
A83: y
= ay and
A84: ex b be
Element of C2 st (ay
U+ b)
in A;
consider by1 be
Element of C2 such that
A85: (ay
U+ by1)
in A by
A84;
((ax
U+ bx)
\/ (ay
U+ by1))
in (C1
"\/" C2) by
A42,
A82,
A85;
then ((ax
\/ ay)
U+ (bx
\/ by1))
in (C1
"\/" C2) by
Th81;
then (x
\/ y)
in C1 or (x
\/ y)
=
{} by
A80,
A83,
Th86;
hence (x
\/ y)
in C1 by
COH_SP: 1;
end;
then (
union A1)
in C1 by
Def1;
hence thesis by
A49,
A69,
A50,
Th86;
end;
end
reserve C1,C2 for
Coherence_Space;
theorem ::
COHSP_1:89
for x,y be
set holds
[
[x, 1],
[y, 1]]
in (
Web (C1
"/\" C2)) iff
[x, y]
in (
Web C1)
proof
let x,y be
set;
A1:
[
[x, 1],
[y, 1]]
in (
Web (C1
"/\" C2)) iff
{
[x, 1],
[y, 1]}
in (C1
"/\" C2) by
COH_SP: 5;
A2:
[x, y]
in (
Web C1) iff
{x, y}
in C1 by
COH_SP: 5;
A3:
[:
{x, y},
{1}:]
=
{
[x, 1],
[y, 1]} by
ZFMISC_1: 30;
(
{x, y}
U+
{} )
=
[:
{x, y},
{1}:] &
{}
in C2 by
Th74,
COH_SP: 1;
hence thesis by
A1,
A2,
A3,
Th84;
end;
theorem ::
COHSP_1:90
for x,y be
set holds
[
[x, 2],
[y, 2]]
in (
Web (C1
"/\" C2)) iff
[x, y]
in (
Web C2)
proof
let x,y be
set;
A1:
[
[x, 2],
[y, 2]]
in (
Web (C1
"/\" C2)) iff
{
[x, 2],
[y, 2]}
in (C1
"/\" C2) by
COH_SP: 5;
A2:
[x, y]
in (
Web C2) iff
{x, y}
in C2 by
COH_SP: 5;
A3:
[:
{x, y},
{2}:]
=
{
[x, 2],
[y, 2]} by
ZFMISC_1: 30;
(
{}
U+
{x, y})
=
[:
{x, y},
{2}:] &
{}
in C1 by
Th74,
COH_SP: 1;
hence thesis by
A1,
A2,
A3,
Th84;
end;
theorem ::
COHSP_1:91
for x,y be
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
let x,y be
set;
assume x
in (
union C1) & y
in (
union C2);
then
{x}
in C1 &
{y}
in C2 by
COH_SP: 4;
then (
{x}
U+
{y})
in (C1
"/\" C2);
then (
[:
{x},
{1}:]
\/
[:
{y},
{2}:])
in (C1
"/\" C2) by
Th73;
then (
{
[x, 1]}
\/
[:
{y},
{2}:])
in (C1
"/\" C2) by
ZFMISC_1: 29;
then (
{
[x, 1]}
\/
{
[y, 2]})
in (C1
"/\" C2) by
ZFMISC_1: 29;
then
A1:
{
[x, 1],
[y, 2]}
in (C1
"/\" C2) by
ENUMSET1: 1;
hence
[
[x, 1],
[y, 2]]
in (
Web (C1
"/\" C2)) by
COH_SP: 5;
thus thesis by
A1,
COH_SP: 5;
end;
theorem ::
COHSP_1:92
for x,y be
set holds
[
[x, 1],
[y, 1]]
in (
Web (C1
"\/" C2)) iff
[x, y]
in (
Web C1)
proof
let x,y be
set;
A1:
[
[x, 1],
[y, 1]]
in (
Web (C1
"\/" C2)) iff
{
[x, 1],
[y, 1]}
in (C1
"\/" C2) by
COH_SP: 5;
A2:
[x, y]
in (
Web C1) iff
{x, y}
in C1 by
COH_SP: 5;
(
{x, y}
U+
{} )
=
[:
{x, y},
{1}:] &
[:
{x, y},
{1}:]
=
{
[x, 1],
[y, 1]} by
Th74,
ZFMISC_1: 30;
hence thesis by
A1,
A2,
Th86;
end;
theorem ::
COHSP_1:93
for x,y be
set holds
[
[x, 2],
[y, 2]]
in (
Web (C1
"\/" C2)) iff
[x, y]
in (
Web C2)
proof
let x,y be
set;
A1:
[
[x, 2],
[y, 2]]
in (
Web (C1
"\/" C2)) iff
{
[x, 2],
[y, 2]}
in (C1
"\/" C2) by
COH_SP: 5;
A2:
[x, y]
in (
Web C2) iff
{x, y}
in C2 by
COH_SP: 5;
(
{}
U+
{x, y})
=
[:
{x, y},
{2}:] &
[:
{x, y},
{2}:]
=
{
[x, 2],
[y, 2]} by
Th74,
ZFMISC_1: 30;
hence thesis by
A1,
A2,
Th86;
end;
theorem ::
COHSP_1:94
for x,y be
set holds not
[
[x, 1],
[y, 2]]
in (
Web (C1
"\/" C2)) & not
[
[y, 2],
[x, 1]]
in (
Web (C1
"\/" C2))
proof
let x,y be
set;
A1: (
{x}
U+
{y})
= (
[:
{x},
{1}:]
\/
[:
{y},
{2}:]) by
Th73
.= (
{
[x, 1]}
\/
[:
{y},
{2}:]) by
ZFMISC_1: 29
.= (
{
[x, 1]}
\/
{
[y, 2]}) by
ZFMISC_1: 29
.=
{
[x, 1],
[y, 2]} by
ENUMSET1: 1;
A2: not (
{x}
U+
{y})
in (C1
"\/" C2) by
Th86;
hence not
[
[x, 1],
[y, 2]]
in (
Web (C1
"\/" C2)) by
A1,
COH_SP: 5;
thus thesis by
A2,
A1,
COH_SP: 5;
end;
theorem ::
COHSP_1:95
(
'not' (C1
"/\" C2))
= ((
'not' C1)
"\/" (
'not' C2))
proof
set C = (C1
"/\" C2);
thus (
'not' (C1
"/\" C2))
c= ((
'not' C1)
"\/" (
'not' C2))
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
A1: (
union C)
= ((
union C1)
U+ (
union C2)) by
Th85;
assume
A2: x
in (
'not' (C1
"/\" C2));
then xx
c= (
union C) by
Th65;
then
consider x1,x2 be
set such that
A3: x
= (x1
U+ x2) and
A4: x1
c= (
union C1) and
A5: x2
c= (
union C2) by
A1,
Th79;
now
reconsider b =
{} as
Element of C2 by
COH_SP: 1;
let a be
Element of C1;
(a
U+ b)
in C;
then
consider z be
set such that
A6: (xx
/\ (a
U+ b))
c=
{z} by
A2,
Th65;
((x1
/\ a)
U+ (x2
/\ b))
c=
{z} by
A3,
A6,
Th82;
then
[:(x1
/\ a),
{1}:]
c= (
[:(x1
/\ a),
{1}:]
\/
[:(x2
/\ b),
{2}:]) & (
[:(x1
/\ a),
{1}:]
\/
[:(x2
/\ b),
{2}:])
c=
{z} by
Th73,
XBOOLE_1: 7;
then
A7:
[:(x1
/\ a),
{1}:]
c=
{z};
now
thus (x1
/\ a)
=
{} implies (x1
/\ a)
c=
{
0 };
assume (x1
/\ a)
<>
{} ;
then
reconsider A = (x1
/\ a) as non
empty
set;
set z1 = the
Element of A;
reconsider zz = z1 as
set;
take zz;
thus (x1
/\ a)
c=
{zz}
proof
let y be
object;
A8: 1
in
{1} by
TARSKI:def 1;
assume y
in (x1
/\ a);
then
[y, 1]
in
[:(x1
/\ a),
{1}:] by
A8,
ZFMISC_1: 87;
then
A9:
[y, 1]
= z by
A7,
TARSKI:def 1;
[z1, 1]
in
[:(x1
/\ a),
{1}:] by
A8,
ZFMISC_1: 87;
then
[z1, 1]
= z by
A7,
TARSKI:def 1;
then y
= z1 by
A9,
XTUPLE_0: 1;
hence thesis by
TARSKI:def 1;
end;
end;
hence ex z be
set st (x1
/\ a)
c=
{z};
end;
then
reconsider x1 as
Element of (
'not' C1) by
A4,
Th65;
now
reconsider a =
{} as
Element of C1 by
COH_SP: 1;
let b be
Element of C2;
(a
U+ b)
in C;
then
consider z be
set such that
A10: (xx
/\ (a
U+ b))
c=
{z} by
A2,
Th65;
((x1
/\ a)
U+ (x2
/\ b))
c=
{z} by
A3,
A10,
Th82;
then
[:(x2
/\ b),
{2}:]
c= (
[:(x1
/\ a),
{1}:]
\/
[:(x2
/\ b),
{2}:]) & (
[:(x1
/\ a),
{1}:]
\/
[:(x2
/\ b),
{2}:])
c=
{z} by
Th73,
XBOOLE_1: 7;
then
A11:
[:(x2
/\ b),
{2}:]
c=
{z};
now
thus (x2
/\ b)
=
{} implies (x2
/\ b)
c=
{
0 };
assume (x2
/\ b)
<>
{} ;
then
reconsider A = (x2
/\ b) as non
empty
set;
set z1 = the
Element of A;
reconsider zz = z1 as
set;
take zz;
thus (x2
/\ b)
c=
{zz}
proof
let y be
object;
A12: 2
in
{2} by
TARSKI:def 1;
assume y
in (x2
/\ b);
then
[y, 2]
in
[:(x2
/\ b),
{2}:] by
A12,
ZFMISC_1: 87;
then
A13:
[y, 2]
= z by
A11,
TARSKI:def 1;
[z1, 2]
in
[:(x2
/\ b),
{2}:] by
A12,
ZFMISC_1: 87;
then
[z1, 2]
= z by
A11,
TARSKI:def 1;
then y
= z1 by
A13,
XTUPLE_0: 1;
hence thesis by
TARSKI:def 1;
end;
end;
hence ex z be
set st (x2
/\ b)
c=
{z};
end;
then
reconsider x2 as
Element of (
'not' C2) by
A5,
Th65;
now
thus x1
in (
'not' C1) & x2
in (
'not' C2);
assume x1
<>
{} & x2
<>
{} ;
then
reconsider x1, x2 as non
empty
set;
set y1 = the
Element of x1, y2 = the
Element of x2;
(
union (
'not' C2))
= (
union C2) by
Th66;
then y2
in (
union C2) by
TARSKI:def 4;
then
A14:
{y2}
in C2 by
COH_SP: 4;
(
union (
'not' C1))
= (
union C1) by
Th66;
then y1
in (
union C1) by
TARSKI:def 4;
then
{y1}
in C1 by
COH_SP: 4;
then (
{y1}
U+
{y2})
in C by
A14;
then
consider z be
set such that
A15: (xx
/\ (
{y1}
U+
{y2}))
c=
{z} by
A2,
Th65;
A16: ((x1
/\
{y1})
U+ (x2
/\
{y2}))
c=
{z} by
A3,
A15,
Th82;
y2
in
{y2} by
TARSKI:def 1;
then y2
in (x2
/\
{y2}) by
XBOOLE_0:def 4;
then
[y2, 2]
in ((x1
/\
{y1})
U+ (x2
/\
{y2})) by
Th77;
then
A17:
[y2, 2]
= z by
A16,
TARSKI:def 1;
y1
in
{y1} by
TARSKI:def 1;
then y1
in (x1
/\
{y1}) by
XBOOLE_0:def 4;
then
[y1, 1]
in ((x1
/\
{y1})
U+ (x2
/\
{y2})) by
Th76;
then
[y1, 1]
= z by
A16,
TARSKI:def 1;
hence contradiction by
A17,
XTUPLE_0: 1;
end;
hence thesis by
A3,
Th86;
end;
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in ((
'not' C1)
"\/" (
'not' C2));
then
consider x1 be
Element of (
'not' C1), x2 be
Element of (
'not' C2) such that
A18: x
= (x1
U+ x2) and
A19: x1
=
{} or x2
=
{} by
Th87;
A20: for a be
Element of C holds ex z be
set st (xx
/\ a)
c=
{z}
proof
let a be
Element of C;
consider a1 be
Element of C1, a2 be
Element of C2 such that
A21: a
= (a1
U+ a2) by
Th83;
A22: (xx
/\ a)
= ((x1
/\ a1)
U+ (x2
/\ a2)) by
A18,
A21,
Th82;
consider z2 be
set such that
A23: (x2
/\ a2)
c=
{z2} by
Th65;
consider z1 be
set such that
A24: (x1
/\ a1)
c=
{z1} by
Th65;
x1
=
{} or x1
<>
{} ;
then
consider z be
set such that
A25: z
=
[z2, 2] & x1
=
{} or z
=
[z1, 1] & x1
<>
{} ;
take z;
let y be
object;
assume
A26: y
in (xx
/\ a);
then
A27: y
=
[(y
`1 ), (y
`2 )] by
A22,
Th75;
A28: (y
`2 )
= 1 & (y
`1 )
in (x1
/\ a1) or (y
`2 )
= 2 & (y
`1 )
in (x2
/\ a2) by
A22,
A26,
Th75;
per cases by
A25;
suppose
A29: z
=
[z2, 2] & x1
=
{} ;
then (y
`1 )
= z2 by
A23,
A28,
TARSKI:def 1;
hence thesis by
A27,
A28,
A29,
TARSKI:def 1;
end;
suppose
A30: z
=
[z1, 1] & x1
<>
{} ;
then (y
`1 )
= z1 by
A19,
A24,
A28,
TARSKI:def 1;
hence thesis by
A19,
A27,
A28,
A30,
TARSKI:def 1;
end;
end;
x2
c= (
union (
'not' C2)) by
ZFMISC_1: 74;
then
A31: x2
c= (
union C2) by
Th66;
x1
c= (
union (
'not' C1)) by
ZFMISC_1: 74;
then x1
c= (
union C1) by
Th66;
then xx
c= ((
union C1)
U+ (
union C2)) by
A18,
A31,
Th78;
then xx
c= (
union C) by
Th85;
hence thesis by
A20;
end;
definition
let C1,C2 be
Coherence_Space;
::
COHSP_1:def25
func C1
[*] C2 ->
set equals (
union the set of all (
bool
[:a, b:]) where a be
Element of C1, b be
Element of C2);
correctness ;
end
theorem ::
COHSP_1:96
Th96: for C1,C2 be
Coherence_Space, x be
set holds x
in (C1
[*] C2) iff ex a be
Element of C1, b be
Element of C2 st x
c=
[:a, b:]
proof
let C1,C2 be
Coherence_Space, x be
set;
hereby
assume x
in (C1
[*] C2);
then
consider y be
set such that
A1: x
in y and
A2: y
in the set of all (
bool
[:a, b:]) where a be
Element of C1, b be
Element of C2 by
TARSKI:def 4;
consider a be
Element of C1, b be
Element of C2 such that
A3: y
= (
bool
[:a, b:]) by
A2;
take a, b;
thus x
c=
[:a, b:] by
A1,
A3;
end;
given a9 be
Element of C1, b9 be
Element of C2 such that
A4: x
c=
[:a9, b9:];
(
bool
[:a9, b9:])
in the set of all (
bool
[:a, b:]) where a be
Element of C1, b be
Element of C2;
hence thesis by
A4,
TARSKI:def 4;
end;
registration
let C1,C2 be
Coherence_Space;
cluster (C1
[*] C2) -> non
empty;
coherence
proof
set a1 = the
Element of C1, a2 = the
Element of C2;
[:a1, a2:]
in (C1
[*] C2) by
Th96;
hence thesis;
end;
end
theorem ::
COHSP_1:97
Th97: for C1,C2 be
Coherence_Space, a be
Element of (C1
[*] C2) holds (
proj1 a)
in C1 & (
proj2 a)
in C2 & a
c=
[:(
proj1 a), (
proj2 a):]
proof
let C1,C2 be
Coherence_Space, a be
Element of (C1
[*] C2);
consider a1 be
Element of C1, a2 be
Element of C2 such that
A1: a
c=
[:a1, a2:] by
Th96;
(
proj1 a)
c= a1 & (
proj2 a)
c= a2 by
A1,
FUNCT_5: 11;
hence (
proj1 a)
in C1 & (
proj2 a)
in C2 by
CLASSES1:def 1;
let x be
object;
assume
A2: x
in a;
then
A3: x
=
[(x
`1 ), (x
`2 )] by
A1,
MCART_1: 21;
then (x
`1 )
in (
proj1 a) & (x
`2 )
in (
proj2 a) by
A2,
XTUPLE_0:def 12,
XTUPLE_0:def 13;
hence thesis by
A3,
ZFMISC_1: 87;
end;
registration
let C1,C2 be
Coherence_Space;
cluster (C1
[*] C2) ->
subset-closed
binary_complete;
coherence
proof
thus (C1
[*] C2) is
subset-closed
proof
let a,b be
set;
assume a
in (C1
[*] C2);
then
consider a1 be
Element of C1, a2 be
Element of C2 such that
A1: a
c=
[:a1, a2:] by
Th96;
assume b
c= a;
then b
c=
[:a1, a2:] by
A1;
hence thesis by
Th96;
end;
let A be
set;
set A1 = { (
proj1 a) where a be
Element of (C1
[*] C2) : a
in A };
set A2 = { (
proj2 a) where a be
Element of (C1
[*] C2) : a
in A };
assume
A2: for a,b be
set st a
in A & b
in A holds (a
\/ b)
in (C1
[*] C2);
now
let a1,b1 be
set;
assume a1
in A2;
then
consider a be
Element of (C1
[*] C2) such that
A3: a1
= (
proj2 a) and
A4: a
in A;
assume b1
in A2;
then
consider b be
Element of (C1
[*] C2) such that
A5: b1
= (
proj2 b) and
A6: b
in A;
(a
\/ b)
in (C1
[*] C2) by
A2,
A4,
A6;
then (
proj2 (a
\/ b))
in C2 by
Th97;
hence (a1
\/ b1)
in C2 by
A3,
A5,
XTUPLE_0: 27;
end;
then
A7: (
union A2)
in C2 by
Def1;
A8: (
union A)
c=
[:(
union A1), (
union A2):]
proof
let x be
object;
assume x
in (
union A);
then
consider a be
set such that
A9: x
in a and
A10: a
in A by
TARSKI:def 4;
A11: (a
\/ a)
in (C1
[*] C2) by
A2,
A10;
then (
proj2 a)
in A2 by
A10;
then
A12: (
proj2 a)
c= (
union A2) by
ZFMISC_1: 74;
a
c=
[:(
proj1 a), (
proj2 a):] by
A11,
Th97;
then
A13: x
in
[:(
proj1 a), (
proj2 a):] by
A9;
(
proj1 a)
in A1 by
A10,
A11;
then (
proj1 a)
c= (
union A1) by
ZFMISC_1: 74;
then
[:(
proj1 a), (
proj2 a):]
c=
[:(
union A1), (
union A2):] by
A12,
ZFMISC_1: 96;
hence thesis by
A13;
end;
now
let a1,b1 be
set;
assume a1
in A1;
then
consider a be
Element of (C1
[*] C2) such that
A14: a1
= (
proj1 a) and
A15: a
in A;
assume b1
in A1;
then
consider b be
Element of (C1
[*] C2) such that
A16: b1
= (
proj1 b) and
A17: b
in A;
(a
\/ b)
in (C1
[*] C2) by
A2,
A15,
A17;
then (
proj1 (a
\/ b))
in C1 by
Th97;
hence (a1
\/ b1)
in C1 by
A14,
A16,
XTUPLE_0: 23;
end;
then (
union A1)
in C1 by
Def1;
hence thesis by
A7,
A8,
Th96;
end;
end
theorem ::
COHSP_1:98
for C1,C2 be
Coherence_Space holds (
union (C1
[*] C2))
=
[:(
union C1), (
union C2):]
proof
let C1,C2 be
Coherence_Space;
thus (
union (C1
[*] C2))
c=
[:(
union C1), (
union C2):]
proof
let x be
object;
assume x
in (
union (C1
[*] C2));
then
consider a be
set such that
A1: x
in a and
A2: a
in (C1
[*] C2) by
TARSKI:def 4;
consider a1 be
Element of C1, a2 be
Element of C2 such that
A3: a
c=
[:a1, a2:] by
A2,
Th96;
a1
c= (
union C1) & a2
c= (
union C2) by
ZFMISC_1: 74;
then
[:a1, a2:]
c=
[:(
union C1), (
union C2):] by
ZFMISC_1: 96;
then a
c=
[:(
union C1), (
union C2):] by
A3;
hence thesis by
A1;
end;
let x,y be
object;
assume
A4:
[x, y]
in
[:(
union C1), (
union C2):];
then x
in (
union C1) by
ZFMISC_1: 87;
then
consider a1 be
set such that
A5: x
in a1 and
A6: a1
in C1 by
TARSKI:def 4;
y
in (
union C2) by
A4,
ZFMISC_1: 87;
then
consider a2 be
set such that
A7: y
in a2 and
A8: a2
in C2 by
TARSKI:def 4;
A9:
[:a1, a2:]
in (C1
[*] C2) by
A6,
A8,
Th96;
[x, y]
in
[:a1, a2:] by
A5,
A7,
ZFMISC_1: 87;
hence thesis by
A9,
TARSKI:def 4;
end;
theorem ::
COHSP_1:99
for x1,y1,x2,y2 be
set holds
[
[x1, x2],
[y1, y2]]
in (
Web (C1
[*] C2)) iff
[x1, y1]
in (
Web C1) &
[x2, y2]
in (
Web C2)
proof
let x1,y1,x2,y2 be
set;
A1:
{
[x1, x2],
[y1, y2]}
c=
[:
{x1, y1},
{x2, y2}:]
proof
let x,y be
object;
assume
[x, y]
in
{
[x1, x2],
[y1, y2]};
then
[x, y]
=
[x1, x2] & x1
in
{x1, y1} & x2
in
{x2, y2} or
[x, y]
=
[y1, y2] & y1
in
{x1, y1} & y2
in
{x2, y2} by
TARSKI:def 2;
hence thesis by
ZFMISC_1: 87;
end;
A2: (
proj1
{
[x1, x2],
[y1, y2]})
=
{x1, y1} & (
proj2
{
[x1, x2],
[y1, y2]})
=
{x2, y2} by
FUNCT_5: 13;
hereby
assume
[
[x1, x2],
[y1, y2]]
in (
Web (C1
[*] C2));
then
{
[x1, x2],
[y1, y2]}
in (C1
[*] C2) by
COH_SP: 5;
then
{x1, y1}
in C1 &
{x2, y2}
in C2 by
A2,
Th97;
hence
[x1, y1]
in (
Web C1) &
[x2, y2]
in (
Web C2) by
COH_SP: 5;
end;
assume
[x1, y1]
in (
Web C1) &
[x2, y2]
in (
Web C2);
then
{x1, y1}
in C1 &
{x2, y2}
in C2 by
COH_SP: 5;
then
{
[x1, x2],
[y1, y2]}
in (C1
[*] C2) by
A1,
Th96;
hence thesis by
COH_SP: 5;
end;