:: Continuous, Stable, and Linear Maps of Coherence Spaces
:: by Grzegorz Bancerek
::
:: Received August 30, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, FUNCT_1, SUBSET_1, TARSKI, COH_SP, FINSET_1, RELAT_1,
CLASSES1, ZFMISC_1, FINSUB_1, CARD_1, ARYTM_3, ARYTM_1, MSSUBFAM,
FUNCOP_1, PBOOLE, MCART_1, CARD_3, XBOOLEAN, FINSEQ_1, LATTICES, EQREL_1,
COHSP_1, NAT_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1,
CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, REAL_1, NAT_1, MCART_1, RELAT_1,
FUNCT_1, FINSEQ_1, FINSET_1, FINSUB_1, CLASSES1, COH_SP, PBOOLE, CARD_3,
PARTFUN1, FUNCT_2, FUNCOP_1;
constructors FINSUB_1, REAL_1, NAT_1, CARD_3, PBOOLE, BORSUK_1, COH_SP,
XTUPLE_0, XREAL_0, NUMBERS, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1,
XREAL_0, NAT_1, FINSEQ_1, ORDINAL1, CARD_1, RELAT_1, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions XBOOLE_0, TARSKI, RELAT_1, COH_SP, CLASSES1, FINSUB_1;
equalities TARSKI;
expansions XBOOLE_0, TARSKI, CLASSES1;
theorems TARSKI, ENUMSET1, ZFMISC_1, RELAT_1, COH_SP, FUNCT_1, FUNCT_2,
FINSEQ_1, FINSET_1, FINSUB_1, FUNCOP_1, MCART_1, CARD_1, CLASSES1,
CARD_2, CARD_3, FUNCT_5, CARD_5, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
PARTFUN1, XTUPLE_0;
schemes NAT_1, SUBSET_1, FUNCT_1, FINSET_1, XBOOLE_0, CARD_2, XFAMILY;
begin :: Directed Sets
Lm1: for X,Y be non empty set for f be Function of X,Y for x be Element of X
holds for y being set st y in f.x holds y in union Y by TARSKI:def 4;
definition
let X be set;
redefine attr X is binary_complete means :: redefines binary_complete (COH_SP, definition)
:Def1:
for A being set st for a,b
being set st a in A & b in A holds a \/ b in X holds union A in X;
compatibility
proof
thus X is binary_complete implies for A being set st for a,b being set st
a in A & b in A holds a \/ b in X holds union A in X
proof
assume
A1: for A being set st A c= X & for a,b being 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 being 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 being set st for a,b being set st a in A & b in A holds a \/
b in X holds union A in X;
hence for A being set st A c= X & for a,b being 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;
func FlatCoh X -> set equals
CohSp id X;
correctness;
func Sub_of_Fin X -> Subset of X means
: Def3:
for x being set holds x in it iff x in X & x is finite;
existence
proof
defpred P[set] means $1 is finite;
thus ex W being 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 being 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 Th1:
for X,x being set holds x in FlatCoh X iff x = {} or ex y being
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 being 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 being set st x = {y} & y in X;
hence thesis by A2,COH_SP:1,def 3;
end;
theorem Th2:
for X being 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 being set such that
A1: x in y and
A2: y in FlatCoh X by TARSKI:def 4;
ex z being 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
for X being 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
Web {{}} = {}
proof
union {{}} = {} by ZFMISC_1:25;
hence thesis;
end;
scheme
MinimalElementwrtIncl { a, A() -> set, P[set] }: ex a being set st a in A()
& P[a] & for b being set st b in A() & P[b] & b c= a holds b = a
provided
A1: a() in A() & P[a()] and
A2: a() is finite
proof
reconsider a = a() as finite set by A2;
defpred p[set] means $1 c= a() & P[$1];
consider X being set such that
A3: for x being 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 being set st P[x,y] & P[y,x] holds x = y;
A6: for x,y,z being 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 being set such that
A8: x in X & for y being 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;
attr X is c=directed means
for Y being finite Subset of X ex a being set st union Y c= a & a in X;
attr X is c=filtered means
for Y being finite Subset of X ex a being set st
(for y being set st y in Y holds a c= y) & a in X;
end;
registration
cluster c=directed -> non empty for set;
coherence
proof
let X be set;
assume
for Y being finite Subset of X ex a being set st union Y c= a & a in X;
then ex a being 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 being finite Subset of X ex a being set st (for y being set
st y in Y holds a c= y) & a in X;
then
ex a being set st (for y being set st y in {}X holds a c= y) & a in X;
hence thesis;
end;
end;
theorem Th5:
for X being set st X is c=directed for a,b being set st a in X &
b in X ex c being set st a \/ b c= c & c in X
proof
let X be set;
assume
A1: for Y being finite Subset of X ex a being 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 Th6:
for X being non empty set st for a,b being set st a in X & b in X
ex c being set st a \/ b c= c & c in X holds X is c=directed
proof
let X be non empty set such that
A1: for a,b being set st a in X & b in X ex c being set st a \/ b c= c &
c in X;
set a = the Element of X;
defpred P[set] means ex a being 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 being set such that
A4: union B c= a and
A5: a in X;
consider c being 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
for X being set st X is c=filtered for a,b being set st a in X & b in
X ex c being set st c c= a /\ b & c in X
proof
let X be set;
assume
A1: for Y being finite Subset of X ex a being set st (for y being set st
y in Y holds a c= y) & a in X;
let a,b be set;
assume a in X & b in X;
then {a,b} c= X by ZFMISC_1:32;
then consider c being set such that
A2: for y being 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 Th8:
for X being non empty set st for a,b being set st a in X & b in X
ex c being set st c c= a /\ b & c in X holds X is c=filtered
proof
let X be non empty set such that
A1: for a,b being set st a in X & b in X ex c being set st c c= a /\ b &
c in X;
set a = the Element of X;
defpred P[set] means ex a being set st (for y being 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 being set such that
A4: for y being set st y in B holds a c= y and
A5: a in X;
consider c being 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 being 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 Th9:
for x being 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
for x,y being 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
for x,y being 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 Th12:
for X being 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;
redefine func Fin a -> preBoolean non empty Subset of C; :: redefines Fin (FINSUB_1, definition)
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 Th13:
for X being non empty set, Y being set st X is c=directed & Y c=
union X & Y is finite ex Z being set st Z in X & Y c= Z
proof
let X be non empty set, Y be set;
set x = the Element of X;
defpred P[Nat] means for Y being set st Y c= union X & Y is
finite & card Y = $1 ex Z being 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 being 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 being set such that
A11: Z in X and
A12: Y\{y} c= Z by A3,A5,A7;
consider V being 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 being 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;
attr X is d.union-closed means
:Def6:
for A being 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 Th14:
for C being Coherence_Space, A being 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 being 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;
redefine func union A -> Element of C; :: redefines union (TARSKI, definition)
coherence by Def6;
end;
definition
let X, Y be set;
pred X includes_lattice_of Y means
for a,b being set st a in Y & b in Y holds a /\ b in X & a \/ b in X;
end;
theorem
for X being 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 being set st a in X & b in X holds a /\ b in X & a \/ b in X;
for a,b being set st a in X & b in X ex c being set st a \/ b c= c & c
in X by A1;
hence X is c=directed by Th6;
for a,b being set st a in X & b in X ex c being set st c c= a /\ b & c
in X by A1;
hence thesis by Th8;
end;
definition
let X, x, y be set;
pred X includes_lattice_of x, y means
X includes_lattice_of {x, y};
end;
theorem Th16:
for X,x,y being set holds X includes_lattice_of x, y iff x in X
& y in X & x /\ y in X & x \/ y in X
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 being 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 :: Continuous, Stable, and Linear Functions
definition
let f be Function;
attr f is union-distributive means
: Def9:
for A being Subset of dom f st
union A in dom f holds f.union A = union (f.:A);
attr f is d.union-distributive means
: Def10:
for A being Subset of dom f st
A is c=directed & union A in dom f holds f.union A = union (f.:A);
end;
definition
let f be Function;
attr f is c=-monotone means
: Def11:
for a, b being set st a in dom f & b in dom f & a c= b holds f.a c= f.b;
attr f is cap-distributive means
: Def12:
for a,b being 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 being 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
for f being Function st f is union-distributive for x,y being set st x
in dom f & y in dom f & x \/ y in dom f holds f.(x \/ y) = (f.x) \/ (f.y)
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 Th18:
for f being Function st f is union-distributive holds f.{} = {}
proof
let f be Function such that
A1: for A being 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 being 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
:: cluster union-distributive cap-distributive Function;
::end;
definition
let f be Function;
attr f is U-continuous means
: Def13:
dom f is d.union-closed & f is d.union-distributive;
end;
definition
let f be Function;
attr f is U-stable means
: Def14:
dom f is multiplicative & f is U-continuous cap-distributive;
end;
definition
let f be Function;
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 Th19:
for X being 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 Th20:
for f being U-continuous Function st dom f is subset-closed for
a being set st a in dom f holds f.a = union (f.:Fin a)
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 Th21:
for f being Function st dom f is subset-closed holds f is
U-continuous iff dom f is d.union-closed & f is c=-monotone & for a, y being
set st a in dom f & y in f.a ex b being set st b is finite & b c= a & y in f.b
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 is 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 being 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 being 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 being set such that
A8: x in b and
A9: b in A by TARSKI:def 4;
ex c being 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 being 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 being set such that
A11: y in B and
A12: B in f.:A by A4,A7,TARSKI:def 4;
consider b being 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 being 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 being set st a in dom f & b in dom f & a c= b holds f.a c= f.b and
A16: for a, y being set st a in dom f & y in f.a ex b being set st b is
finite & b c= a & y in f.b;
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 being set such that
A19: b is finite & b c= union A9 and
A20: x in f.b by A16,A18;
consider c being 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 being 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 Th22:
for f being Function st dom f is subset-closed d.union-closed
holds f is U-stable iff f is c=-monotone & for a, y being set st a in dom f & y
in f.a ex b being set st b is finite & b c= a & y in f.b & for c being set st c
c= a & y in f.c holds b c= c
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 being 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 is Subset of b: y in f.c} by A6;
then reconsider A = {c where c is 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 being Subset of b st x = c & y in f.c;
hence thesis;
end;
A8: for x,y,z being set st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1;
A9: for x,y being set st P[x,y] & P[y,x] holds x = y;
reconsider A as finite non empty set by A7;
A10: A <> {};
consider c being set such that
A11: c in A & for y being set st y in A & y <> c holds not P[y,c] from
CARD_2:sch 3(A10,A9,A8);
ex d being 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 being 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 being set st a in dom f & y in f.a ex b being set st b is
finite & b c= a & y in f.b & for c being set st c c= a & y in f.c holds b c= c;
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 being set st b is finite & b c= a & y in f.b & for c being set
st c c= a & y in f.c holds b c= c by A22;
hence ex b being 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 being set such that
c is finite and
c c= a \/ b and
A31: x in f.c and
A32: for d being 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 Th23:
for f being Function st dom f is subset-closed d.union-closed
holds f is U-linear iff f is c=-monotone &
for a, y being set st a in dom f & y
in f.a ex x being set st x in a & y in f.{x} & for b being set st b c= a & y in
f.b holds x in b
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 being set such that
b is finite and
A6: b c= a and
A7: y in f.b and
A8: for c being 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 is 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 being 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 being 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 being set such that
A14: y in Y and
A15: Y in f.:A by A7,A13,TARSKI:def 4;
consider X being 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 being 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 being set st a in dom f & y in f.a ex x being set st x in
a & y in f.{x} & for b being set st b c= a & y in f.b holds x in b;
now
let a, y be set;
assume a in dom f & y in f.a;
then consider x being set such that
A21: x in a & y in f.{x} and
A22: for b being 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 being set such that
A24: x in union A and
A25: y in f.{x} and
for b being set st b c= union A & y in f.b holds x in b by A20,A23;
consider a being 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 being 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 :: Graph of Continuous Function
definition
let f be Function;
func graph f -> set means
: Def16:
for x being set holds x in it iff ex y
being finite set, z being set st x = [y,z] & y in dom f & z in f.y;
existence
proof
defpred P[object] means
ex y being finite set, z being set st $1 = [y,z] & y
in dom f & z in f.y;
consider X being set such that
A1: for x being 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 being finite set, z being 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 being object such that
A6: not (x in X1 iff x in X2) by TARSKI:2;
x in X2 iff not ex y being finite set, z being 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;
redefine func graph f -> Subset of [:C1, union C2:]; :: redefines graph (COHSP_1, definition)
coherence
proof
graph f c= [:C1, union C2:]
proof
let x be object;
assume x in graph f;
then consider y being finite set, z being 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 being finite set, z being set st x = [y,z] & y in dom f & z in f
.y by Def16;
hence thesis;
end;
end;
theorem Th24:
for f being Function, x,y being set holds [x,y] in graph f iff x
is finite & x in dom f & y in f.x
proof
let f be Function, x,y be set;
now
given y9 being finite set, z being 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 Th25:
for f being c=-monotone Function for a,b being set st b in dom f
& a c= b & b is finite for y being set st [a,y] in graph f holds [b,y] in graph
f
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 Th26:
for C1, C2 being Coherence_Space for f being Function of C1,C2
for a being Element of C1 for y1,y2 being set st [a,y1] in graph f & [a,y2] in
graph f holds {y1,y2} in C2
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
for C1, C2 being Coherence_Space for f being c=-monotone Function of
C1,C2 for a,b being Element of C1 st a \/ b in C1 for y1,y2 being set st [a,y1]
in graph f & [b,y2] in graph f holds {y1,y2} in C2
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 Th28:
for C1, C2 being Coherence_Space for f,g being 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 being 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 being Coherence_Space for X being Subset of [:C1, union C2:]
st (for x being set st x in X holds x`1 is finite) & (for a,b being finite
Element of C1 st a c= b for y being set st [a,y] in X holds [b,y] in X) & (for
a being finite Element of C1 for y1,y2 being set st [a,y1] in X & [a,y2] in X
holds {y1,y2} in C2) ex f being U-continuous Function of C1,C2 st X = graph f &
for a being 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 being set st x in X holds x`1 is finite and
A2: for a,b being finite Element of C1 st a c= b for y being set st [a,y
] in X holds [b,y] in X and
A3: for a being finite Element of C1 for y1,y2 being set st [a,y1] in X
& [a,y2] in X holds {y1,y2} in C2;
deffunc f(set) = X.:Fin $1;
consider f being Function such that
A4: dom f = C1 & for a being 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 being 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 being 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 being 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 being 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 being 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
for C1, C2 being Coherence_Space for X being Subset of [:C1, union C2
:] st (for x being set st x in X holds x`1 is finite) & (for a,b being finite
Element of C1 st a c= b for y being set st [a,y] in X holds [b,y] in X) & (for
a being finite Element of C1 for y1,y2 being set st [a,y1] in X & [a,y2] in X
holds {y1,y2} in C2) ex f being U-continuous Function of C1,C2 st X = graph f
proof
let C1, C2 be Coherence_Space;
let X be Subset of [:C1, union C2:];
assume
A1: not thesis;
then ex f being U-continuous Function of C1,C2 st X = graph f & for a being
Element of C1 holds f.a = X.:Fin a by Lm4;
hence thesis by A1;
end;
theorem
for C1, C2 being Coherence_Space for f being U-continuous Function of
C1,C2 for a being Element of C1 holds f.a = (graph f).:Fin a
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 being finite set, z being 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 being finite Element of C1 st a c= b for y being set st [a,y] in
X holds [b,y] in X by Th25;
for a being finite Element of C1 for y1,y2 being set st [a,y1] in X & [a
,y2] in X holds {y1,y2} in C2 by Th26;
then consider g being U-continuous Function of C1,C2 such that
A3: X = graph g and
A4: for a being 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 :: Trace of Stable Function
definition
let f be Function;
func Trace f -> set means
: Def17:
for x being set holds x in it iff ex a, y
being set st x = [a,y] & a in dom f & y in f.a & for b being set st b in dom f
& b c= a & y in f.b holds a = b;
existence
proof
defpred P[object] means
ex a, y being set st $1 = [a,y] & a in dom f & y in f
.a & for b being set st b in dom f & b c= a & y in f.b holds a = b;
consider T being set such that
A1: for x being 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 being set such that
A2: x = [a,y] and
A3: a in dom f and
A4: y in f.a and
for b being 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 being object such that
A6: not (x in T1 iff x in T2) by TARSKI:2;
x in T2 iff not ex a, y being set st x = [a,y] & a in dom f & y in f.a
& for b being set st b in dom f & b c= a & y in f.b holds a = b by A5,A6;
hence contradiction by A5;
end;
end;
theorem Th31:
for f being Function
for a being set, y being object holds [a,y] in Trace f
iff a in dom f & y in f.a & for b being set st b in dom f & b c= a & y in f.b
holds a = b
proof
let f be Function, a9 be set, y9 be object;
now
given a, y being set such that
A1: [a9,y9] = [a,y] and
A2: a in dom f & y in f.a & for b being set st b in dom f & b c= a & y
in f. b holds a = b;
a9 = a & y9 = y by A1,XTUPLE_0:1;
hence a9 in dom f & y9 in f.a9 & for b being 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;
redefine func Trace f -> Subset of [:C1, union C2:]; :: redefines Trace (COHSP_1, definition)
coherence
proof
Trace f c= [:C1, union C2:]
proof
let x be object;
assume x in Trace f;
then consider a, y being set such that
A1: x = [a,y] and
A2: a in dom f and
A3: y in f.a and
for b being 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 being set st x = [a,y] & a in dom f & y in f.a & for b being
set st b in dom f & b c= a & y in f.b holds a = b by Def17;
hence thesis;
end;
end;
theorem
for f being 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 being set such that
A2: [x,z] = [a,y] and
A3: a in dom f and
A4: y in f.a and
A5: for b being set st b in dom f & b c= a & y in f.b holds a = b by Def17;
consider b being 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 Th33:
for f being U-continuous Function st dom f is subset-closed for
a, y being set st [a,y] in Trace f holds a is finite
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 Th34:
for C1, C2 being Coherence_Space for f being c=-monotone
Function of C1,C2 for a1,a2 being set st a1 \/ a2 in C1
for y1,y2 being 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 Th35:
for C1, C2 being Coherence_Space for f being cap-distributive
Function of C1,C2 for a1,a2 being set st a1 \/ a2 in C1
for y being 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 Th36:
for C1, C2 being Coherence_Space for f,g being U-stable Function
of C1,C2 st Trace f c= Trace g for a being Element of C1 holds f.a c= g.a
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 being set such that
b is finite and
A3: b c= x and
A4: z in f.b and
A5: for c being 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 Th37:
for C1, C2 being Coherence_Space for f,g being 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 being 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 being Coherence_Space for X being Subset of [:C1, union C2:]
st (for x being set st x in X holds x`1 is finite) & (for a,b being Element of
C1 st a \/ b in C1
for y1,y2 being object st [a,y1] in X & [b,y2] in X holds {y1,
y2} in C2) & (for a,b being Element of C1 st a \/ b in C1
for y being object st [a
,y] in X & [b,y] in X holds a = b) ex f being U-stable Function of C1,C2 st X =
Trace f & for a being 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 being set st x in X holds x`1 is finite and
A2: for a,b being Element of C1 st a \/ b in C1
for y1,y2 being object st [
a,y1] in X & [b,y2] in X holds {y1,y2} in C2 and
A3: for a,b being Element of C1 st a \/ b in C1
for y being object st [a,y]
in X & [b,y] in X holds a = b;
deffunc f(set) = X.:Fin $1;
consider f being Function such that
A4: dom f = C1 & for a being 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 being 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 being 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 being 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 being 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 being 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 being 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,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 being 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 Th38:
for C1, C2 being Coherence_Space for X being Subset of [:C1,
union C2:] st (for x being set st x in X holds x`1 is finite) & (for a,b being
Element of C1 st a \/ b in C1
for y1,y2 being object st [a,y1] in X & [b,y2] in X
holds {y1,y2} in C2) & (for a,b being Element of C1 st a \/ b in C1
for y being object
st [a,y] in X & [b,y] in X holds a = b) ex f being U-stable Function of C1,
C2 st X = Trace f
proof
let C1, C2 be Coherence_Space;
let X be Subset of [:C1, union C2:];
assume
A1: not thesis;
then ex f being U-stable Function of C1,C2 st X = Trace f & for a being
Element of C1 holds f.a = X.:Fin a by Lm5;
hence thesis by A1;
end;
theorem
for C1, C2 being Coherence_Space for f being U-stable Function of C1,
C2 for a being Element of C1 holds f.a = (Trace f).:Fin a
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 being set such that
A4: x = [a,y] and
a in dom f and
y in f.a and
for b being 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 being Element of C1 st a \/ b in C1
for y1,y2 being object st [a,
y1] in X & [b,y2] in X holds {y1,y2} in C2)& for a,b being Element of C1 st a
\/ b in C1
for y being object st [a,y] in X & [b,y] in X holds a = b by Th34,Th35;
then consider g being U-stable Function of C1,C2 such that
A5: X = Trace g and
A6: for a being 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 Th40:
for C1,C2 being Coherence_Space, f being U-stable Function of C1
,C2 for a being Element of C1, y being set holds y in f.a iff ex b being
Element of C1 st [b,y] in Trace f & b c= a
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 being set such that
b is finite and
A2: b c= a and
A3: y in f.b and
A4: for c being 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 being 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
for C1, C2 being Coherence_Space ex f being 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 being Element of C1 st a \/ b in C1
for y being object st [a,y] in
X & [b,y] in X holds a = b;
( for x being set st x in X holds x`1 is finite)& for a,b being Element
of C1 st a \/ b in C1
for y1,y2 being object st [a, y1] in X & [b,y2] in X holds {
y1,y2} in C2;
hence thesis by A1,Th38;
end;
theorem Th42:
for C1, C2 being Coherence_Space for a being finite Element of
C1, y being set st y in union C2 ex f being U-stable Function of C1, C2 st
Trace f = {[a,y]}
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
for C1, C2 being Coherence_Space for a being Element of C1, y being
set for f being U-stable Function of C1, C2 st Trace f = {[a,y]} for b being
Element of C1 holds (a c= b implies f.b = {y}) & (not a c= b implies f.b = {})
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 being 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 being 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 Th44:
for C1, C2 being Coherence_Space for f being U-stable Function
of C1,C2 for X being Subset of Trace f ex g being U-stable Function of C1, C2
st Trace g = X
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
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 being set such that
A4: x = [a,y] and
a in dom f and
y in f.a and
for b being 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
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 Th45:
for C1, C2 being Coherence_Space for A being set st for x,y
being set st x in A & y in A ex f being U-stable Function of C1,C2 st x \/ y =
Trace f ex f being U-stable Function of C1,C2 st union A = Trace f
proof
let C1, C2 be Coherence_Space;
let A be set such that
A1: for x,y being set st x in A & y in A ex f being U-stable Function of
C1,C2 st x \/ y = Trace f;
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 being 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 being 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 being 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 being 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 being 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 being 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 being set such that
A17: x in y and
A18: y in A by TARSKI:def 4;
y \/ y = y;
then consider f being U-stable Function of C1,C2 such that
A19: y = Trace f by A1,A18;
consider a, y being set such that
A20: x = [a,y] and
a in dom f and
y in f.a and
for b being 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 being set such that
A21: x in y and
A22: y in A by TARSKI:def 4;
y \/ y = y;
then ex f being 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;
func StabCoh(C1,C2) -> set means
: Def18:
for x being set holds x in it iff
ex f being U-stable Function of C1,C2 st x = Trace f;
uniqueness
proof
let X1, X2 be set;
assume
A1: not thesis;
then consider x being object such that
A2: not (x in X1 iff x in X2) by TARSKI:2;
x in X2 iff not ex f being 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 being U-stable Function of C1,C2 st $1 = Trace f;
consider X being set such that
A3: for x being 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 being U-stable Function of C1,C2 st a = Trace f by Def18;
assume b c= a;
then ex g being 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 being 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 being U-stable Function of C1,C2 st x \/ y = Trace f by Def18;
end;
then ex f being U-stable Function of C1,C2 st union A = Trace f by Th45;
hence thesis by Def18;
end;
end;
theorem Th46:
for C1,C2 being Coherence_Space, f being 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 being set such that
A2: [x1,x2] = [a,y] and
A3: a in dom f and
A4: y in f.a and
for b being 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
for C1,C2 being 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 being set such that
A1: x in a and
A2: a in StabCoh(C1,C2) by TARSKI:def 4;
ex f being 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 being 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 Th48:
for C1,C2 being Coherence_Space for a,b being finite Element of
C1, y1,y2 being set holds [[a,y1],[b,y2]] in Web StabCoh(C1,C2) iff not a \/ b
in C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in Web C2 & (y1 = y2 implies
a = b)
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 being 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 being 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 :: Trace of Linear Functions
theorem Th49:
for C1, C2 being Coherence_Space for f being U-stable Function
of C1,C2 holds f is U-linear iff
for a being set, y being object st [a,y] in Trace f ex x
being 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 being set such that
A5: x in a and
A6: y in f.{x} and
for b being 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 being set,y being object
st [a,y] in Trace f ex x being 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 being set such that
b is finite and
A12: b c= a and
A13: y in f.b and
A14: for c being 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 being 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;
func LinTrace f -> set means
: Def19:
for x being object holds x in it iff ex y
,z being object st x = [y,z] & [{y},z] in Trace f;
uniqueness
proof
let X1, X2 be set;
assume
A1: not thesis;
then consider x being object such that
A2: not (x in X1 iff x in X2) by TARSKI:2;
x in X2 iff
not ex y,z being 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 being object st $1 = [y,z] & [{y},z] in Trace f;
set C1 = dom f, C2 = rng f;
consider X being set such that
A3: for x being 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 being 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 Th50:
for f being Function, x,y being 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 being 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 Th51:
for f being Function st f.{} = {} for x,y being 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 being 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 Th52:
for f being Function, x,y being 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;
redefine func LinTrace f -> Subset of [:union C1, union C2:]; :: redefines LinTrace (COHSP_1, definition)
coherence
proof
LinTrace f c= [:union C1, union C2:]
proof
let x be object;
assume x in LinTrace f;
then consider y,z being 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 being object st x = [y,z] & [{y},z] in Trace f by Def19;
hence thesis;
end;
end;
definition
let C1, C2 be Coherence_Space;
func LinCoh(C1,C2) -> set means
: Def20:
for x being set holds x in it iff
ex f being U-linear Function of C1,C2 st x = LinTrace f;
uniqueness
proof
let X1, X2 be set;
assume
A1: not thesis;
then consider x being object such that
A2: not (x in X1 iff x in X2) by TARSKI:2;
x in X2 iff not ex f being 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 being U-linear Function of C1,C2 st $1 =
LinTrace f;
consider X being set such that
A3: for x being 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 Th53:
for C1, C2 being Coherence_Space for f being c=-monotone
Function of C1,C2
for x1,x2 being object st {x1,x2} in C1
for y1,y2 being 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 Th54:
for C1, C2 being Coherence_Space for f being cap-distributive
Function of C1,C2
for x1,x2 being set st {x1,x2} in C1 for y being 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 Th55:
for C1, C2 being Coherence_Space for f,g being 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 being 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 being 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 being Coherence_Space for X being Subset of [:union C1, union
C2:] st (for a,b being set st {a,b} in C1
for y1,y2 being object st [a,y1] in X &
[b,y2] in X holds {y1,y2} in C2) & (for a,b being set st {a,b} in C1
for y being object st [a,y] in X & [b,y] in X holds a = b)
ex f being U-linear Function
of C1,C2 st X = LinTrace f & for a being 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 being set st {a,b} in C1
for y1,y2 being object st [a,y1] in X
& [b,y2] in X holds {y1,y2} in C2 and
A2: for a,b being set st {a,b} in C1
for y being object st [a,y] in X & [b,
y] in X holds a = b;
deffunc f(set) = X.:$1;
consider f being Function such that
A3: dom f = C1 & for a being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 Th56:
for C1, C2 being Coherence_Space for X being Subset of [:union
C1, union C2:] st (for a,b being set st {a,b} in C1
for y1,y2 being object st [a,
y1] in X & [b,y2] in X holds {y1,y2} in C2) & (for a,b being set st {a,b} in C1
for y being object st [a,y] in X & [b,y] in X holds a = b)
ex f being U-linear
Function of C1,C2 st X = LinTrace f
proof
let C1, C2 be Coherence_Space;
let X be Subset of [:union C1, union C2:];
assume
A1: not thesis;
then ex f being U-linear Function of C1,C2 st X = LinTrace f & for a being
Element of C1 holds f.a = X.:a by Lm6;
hence thesis by A1;
end;
theorem
for C1, C2 being Coherence_Space for f being U-linear Function of C1,
C2 for a being Element of C1 holds f.a = (LinTrace f).:a
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 being set st {a,b} in C1
for y1,y2 being object st [a,y1] in X &
[b,y2] in X holds {y1,y2} in C2)& for a,b being set st {a,b} in C1
for y being
object st [a,y] in X & [b,y] in X holds a = b by Th53,Th54;
then consider g being U-linear Function of C1,C2 such that
A1: X = LinTrace g and
A2: for a being Element of C1 holds g.a = X.:a by Lm6;
g.a = X.:a by A2;
hence thesis by A1,Th55;
end;
theorem
for C1, C2 being Coherence_Space ex f being 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 being set st {a,b} in C1
for y1,y2 being object st [a,y1] in X &
[ b,y2] in X holds {y1,y2} in C2)& for a,b being set st {a,b} in C1 for y being
object st [a,y] in X & [b,y] in X holds a = b;
hence thesis by Th56;
end;
theorem Th59:
for C1, C2 being Coherence_Space for x being set, y being set st
x in union C1 & y in union C2 ex f being U-linear Function of C1, C2 st
LinTrace f = {[x,y]}
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
for C1, C2 being Coherence_Space for x being set, y being set st x in
union C1 for f being U-linear Function of C1, C2 st LinTrace f = {[x,y]} for a
being Element of C1 holds (x in a implies f.a = {y}) & (not x in a implies f.a
= {})
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 being Element of C1 such that
A4: [c,x] in Trace f and
c c= b by Th40;
consider d being 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 being Element of C1 such that
A9: [c,z] in Trace f and
A10: c c= b by Th40;
consider d being 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 Th61:
for C1, C2 being Coherence_Space for f being U-linear Function
of C1,C2 for X being Subset of LinTrace f ex g being U-linear Function of C1,
C2 st LinTrace g = X
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
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
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 Th62:
for C1, C2 being Coherence_Space for A being set st for x,y
being set st x in A & y in A ex f being U-linear Function of C1,C2 st x \/ y =
LinTrace f ex f being U-linear Function of C1,C2 st union A = LinTrace f
proof
let C1, C2 be Coherence_Space;
let A be set such that
A1: for x,y being set st x in A & y in A ex f being U-linear Function of
C1,C2 st x \/ y = LinTrace f;
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 being 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 being 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 being 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 being 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 being 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 being 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 being set such that
A16: x in y and
A17: y in A by TARSKI:def 4;
y \/ y = y;
then ex f being 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 being U-linear Function of C1,C2 st a = LinTrace f by Def20;
assume b c= a;
then ex g being 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 being 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 being U-linear Function of C1,C2 st x \/ y = LinTrace f by
Def20;
end;
then ex f being U-linear Function of C1,C2 st union A = LinTrace f by Th62;
hence thesis by Def20;
end;
end;
theorem
for C1,C2 being 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 being set such that
A1: x in a and
A2: a in LinCoh(C1,C2) by TARSKI:def 4;
ex f being 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 being 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
for C1,C2 being Coherence_Space for x1,x2 being set, y1,y2 being set
holds [[x1,y1],[x2,y2]] in Web LinCoh(C1,C2) iff x1 in union C1 & x2 in union
C1 & (not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in Web
C2 & (y1 = y2 implies x1 = x2))
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 being 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 being 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 being 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 :: Negation of Coherence Spaces
definition
let C be Coherence_Space;
func 'not' C -> set equals
{a where a is Subset of union C: for b being
Element of C ex x being set st a /\ b c= {x}};
correctness;
end;
theorem Th65:
for C being Coherence_Space, x being set holds x in 'not' C iff
x c= union C & for a being Element of C ex z being set st x /\ a c= {z}
proof
let C be Coherence_Space, x be set;
x in 'not' C iff ex X being Subset of union C st x = X & for a being
Element of C ex z being 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 being Subset of union C such that
A1: a = aa and
A2: for b being Element of C ex x being 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 being 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 being 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 being Subset of union C st x = a & for b being Element of C ex
x being 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 being 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 being 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 being Subset of union C such that
A13: w \/ v = aa and
A14: for b being Element of C ex x being set st aa /\ b c= {x};
consider t being set such that
A15: aa /\ c c= {t} by A14;
x in c & x in aa by A9,A13,XBOOLE_0:def 3,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 Th66:
for C being 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 being 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 being Element of C
ex z being set st {x} /\ a c= {z}
proof let a be Element of C;
consider z being 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 Th67:
for C being Coherence_Space, x,y being 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 being 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 Th68:
for C being Coherence_Space, x,y being set st {x,y} c= union C &
not {x,y} in C holds {x,y} in 'not' C
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 being 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
for C being Coherence_Space for x,y being set holds [x,y] in Web 'not'
C iff x in union C & y in union C & (x = y or not [x,y] in Web C)
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,5
,ENUMSET1:29;
hence thesis by A1,A3,A4,COH_SP:5,ZFMISC_1:32;
end;
Lm7: for C being 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 being Subset of union 'not' C such that
A1: x = a and
A2: for b being Element of 'not' C ex x being 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 being 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 Th70:
for C being 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
'not' {{}} = {{}}
proof
union 'not' {{}} = union {{}} by Th66
.= {} by ZFMISC_1:25;
hence 'not' {{}} c= {{}} by ZFMISC_1:1,82;
{} in 'not' {{}} by COH_SP:1;
hence thesis by ZFMISC_1:31;
end;
theorem
for X being 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 being set st xx /\ a c= {z};
end;
suppose
ex z being set st a = {z} & z in X;
then consider z being 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 :: Product and Coproduct on Coherence Spaces
definition
let x,y be set;
func x U+ y -> set equals
Union disjoin <*x,y*>;
correctness;
end;
theorem Th73:
for x,y being 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,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,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,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,XBOOLE_0:def
3;
end;
hence thesis by TARSKI:2;
end;
theorem Th74:
for x being 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 Th75:
for x,y,z being set st z in x U+ y holds z = [z`1,z`2] & (z`2 =
1 & z`1 in x or z`2 = 2 & z`1 in y)
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,21;
end;
theorem Th76:
for x,y being set, z being 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 Th77:
for x,y being set, z being 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 Th78:
for x1,y1, x2,y2 being 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 Th79:
for x,y, z being set st z c= x U+ y ex x1,y1 being set st z = x1
U+ y1 & x1 c= x & y1 c= y
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 being 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 being 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 Th80:
for x1,y1, x2,y2 being set holds x1 U+ y1 = x2 U+ y2 iff x1 = x2 & y1 = y2
by Th78;
theorem Th81:
for x1,y1, x2,y2 being 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 Th82:
for x1,y1, x2,y2 being 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;
func C1 "/\" C2 -> set equals
the set of all a U+ b where a is Element of C1, b is Element
of C2;
correctness;
func C1 "\/" C2 -> set equals
(the set of all a U+ {} where a is Element of C1) \/
(the set of all {} U+ b where b is Element of C2);
correctness;
end;
theorem Th83:
for C1,C2 being Coherence_Space for x being object holds x in C1
"/\" C2 iff ex a being Element of C1, b being Element of C2 st x = a U+ b;
theorem Th84:
for C1,C2 being Coherence_Space for x,y being set holds x U+ y
in C1 "/\" C2 iff x in C1 & y in C2
proof
let C1,C2 be Coherence_Space, x,y be set;
now
given a being Element of C1, b being 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 Th85:
for C1,C2 being 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 being set such that
A1: x in a and
A2: a in C1 "/\" C2 by TARSKI:def 4;
consider a1 being Element of C1, a2 being 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 being 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 being 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 Th86:
for C1,C2 being Coherence_Space for x,y being set holds x U+ y
in C1 "\/" C2 iff x in C1 & y = {} or x = {} & y in C2
proof
let C1,C2 be Coherence_Space, x,y be set;
A1: now
given a being 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 being 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 is Element of C1 or x U+ y in the set of all
{} U+ b where b is Element of C2 by XBOOLE_0:def 3;
hence thesis by A1,A3;
end;
theorem Th87:
for C1,C2 being Coherence_Space for x being set st x in C1 "\/"
C2 ex a being Element of C1, b being Element of C2 st x = a U+ b & (a = {} or b
= {})
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 is Element of C1 or x in the set of
all {}
U+ b where b is Element of C2 by XBOOLE_0:def 3;
then
{} in C2 & (ex a being Element of C1 st x = a U+ {}) or {} in C1 & ex b
being Element of C2 st x = {} U+ b by COH_SP:1;
hence thesis;
end;
theorem
for C1,C2 being 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 being set such that
A1: x in a and
A2: a in C1 "\/" C2 by TARSKI:def 4;
consider a1 being Element of C1, a2 being 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 being 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 being 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 being Element of C1, bb being Element of C2 such that
A1: a = aa U+ bb;
assume b c= a;
then consider x1,y1 being 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 being set st a in A & b in A holds a \/ b in C1 "/\" C2;
set A2 = {b where b is Element of C2: ex a being Element of C1 st a U+ b
in A};
now
let x,y be set;
assume x in A2;
then consider ax being Element of C2 such that
A5: x = ax and
A6: ex b being Element of C1 st b U+ ax in A;
consider bx being Element of C1 such that
A7: bx U+ ax in A by A6;
assume y in A2;
then consider ay being Element of C2 such that
A8: y = ay and
A9: ex b being Element of C1 st b U+ ay in A;
consider by1 being 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 is Element of C1: ex b being 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 being set such that
A16: x`1 in a and
A17: a in A1 by TARSKI:def 4;
consider ax being Element of C1 such that
A18: a = ax and
A19: ex b being Element of C2 st ax U+ b in A by A17;
consider bx being 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 being set such that
A22: x`1 in a and
A23: a in A2 by TARSKI:def 4;
consider bx being Element of C2 such that
A24: a = bx and
A25: ex a being Element of C1 st a U+ bx in A by A23;
consider ax being 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 being 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 being Element of C1, bb being 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 being Element of C1 such that
A31: x = ax and
A32: ex b being Element of C2 st ax U+ b in A;
consider bx being Element of C2 such that
A33: ax U+ bx in A by A32;
assume y in A1;
then consider ay being Element of C1 such that
A34: y = ay and
A35: ex b being Element of C2 st ay U+ b in A;
consider by1 being 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 being Element of C1, bb being 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 being 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 is Element of C1: ex b being Element of C2 st a U+ b
in A};
set A2 = {b where b is Element of C2: ex a being Element of C1 st a U+ b
in A};
assume
A42: for a,b being 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 being Element of C2 such that
A43: x = ax and
A44: ex b being Element of C1 st b U+ ax in A;
consider bx being Element of C1 such that
A45: bx U+ ax in A by A44;
assume y in A2;
then consider ay being Element of C2 such that
A46: y = ay and
A47: ex b being Element of C1 st b U+ ay in A;
consider by1 being 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 being set such that
A54: x`1 in a and
A55: a in A1 by TARSKI:def 4;
consider ax being Element of C1 such that
A56: a = ax and
A57: ex b being Element of C2 st ax U+ b in A by A55;
consider bx being 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 being set such that
A60: x`1 in a and
A61: a in A2 by TARSKI:def 4;
consider bx being Element of C2 such that
A62: a = bx and
A63: ex a being Element of C1 st a U+ bx in A by A61;
consider ax being 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 being 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 being Element of C1, bb being 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 being set such that
A70: aa in x and
A71: x in A1 by TARSKI:def 4;
consider ax being Element of C1 such that
A72: x = ax and
A73: ex b being Element of C2 st ax U+ b in A by A71;
consider bx being 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 being set such that
A75: bb in y and
A76: y in A2 by TARSKI:def 4;
consider by1 being Element of C2 such that
A77: y = by1 and
A78: ex a being Element of C1 st a U+ by1 in A by A76;
consider ay being 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 being Element of C1 such that
A80: x = ax and
A81: ex b being Element of C2 st ax U+ b in A;
consider bx being Element of C2 such that
A82: ax U+ bx in A by A81;
assume y in A1;
then consider ay being Element of C1 such that
A83: y = ay and
A84: ex b being Element of C2 st ay U+ b in A;
consider by1 being 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
for x,y being 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
for x,y being 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
for x,y being set st x in union C1 & y in union C2 holds [[x,1],[y,2]]
in Web (C1 "/\" C2) & [[y,2],[x,1]] in Web (C1 "/\" C2)
proof
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
for x,y being 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
for x,y being 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
for x,y being set holds not [[x,1],[y,2]] in Web (C1 "\/" C2) & not [[
y,2],[x,1]] in Web (C1 "\/" C2)
proof
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
'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 being 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 being 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 being 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 being 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 being 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 being 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 being Element of 'not' C1, x2 being Element of 'not' C2 such
that
A18: x = x1 U+ x2 and
A19: x1 = {} or x2 = {} by Th87;
A20: for a being Element of C ex z being set st xx /\ a c= {z}
proof
let a be Element of C;
consider a1 being Element of C1, a2 being 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 being set such that
A23: x2/\a2 c= {z2} by Th65;
consider z1 being set such that
A24: x1/\a1 c= {z1} by Th65;
x1 = {} or x1 <> {};
then consider z being 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;
func C1 [*] C2 -> set equals
union the set of all bool [:a,b:] where a is Element of C1, b
is Element of C2;
correctness;
end;
theorem Th96:
for C1,C2 being Coherence_Space, x being set holds x in C1 [*]
C2 iff ex a being Element of C1, b being Element of C2 st x c= [:a,b:]
proof
let C1,C2 be Coherence_Space, x be set;
hereby
assume x in C1[*]C2;
then consider y being set such that
A1: x in y and
A2: y in the set of all
bool [:a,b:] where a is Element of C1, b is Element of C2 by TARSKI:def 4;
consider a being Element of C1, b being 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 being Element of C1, b9 being Element of C2 such that
A4: x c= [:a9,b9:];
bool [:a9,b9:] in the set of all
bool [:a,b:] where a is Element of C1, b is 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 Th97:
for C1,C2 being Coherence_Space, a being Element of C1 [*] C2
holds proj1 a in C1 & proj2 a in C2 & a c= [:proj1 a, proj2 a:]
proof
let C1,C2 be Coherence_Space, a be Element of C1 [*] C2;
consider a1 being Element of C1, a2 being 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,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 being Element of C1, a2 being 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 is Element of C1[*]C2: a in A};
set A2 = {proj2 a where a is Element of C1[*]C2: a in A};
assume
A2: for a,b being 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 being Element of C1[*]C2 such that
A3: a1 = proj2 a and
A4: a in A;
assume b1 in A2;
then consider b being 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 being 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 being Element of C1[*]C2 such that
A14: a1 = proj1 a and
A15: a in A;
assume b1 in A1;
then consider b being 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
for C1,C2 being 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 being set such that
A1: x in a and
A2: a in C1 [*] C2 by TARSKI:def 4;
consider a1 being Element of C1, a2 being 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 being 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 being 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
for x1,y1, x2,y2 being set holds [[x1,x2],[y1,y2]] in Web (C1 [*] C2)
iff [x1,y1] in Web C1 & [x2,y2] in Web C2
proof
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;