Copyright (c) 1996 Association of Mizar Users
environ
vocabulary FUNCT_1, RELAT_1, RELAT_2, LATTICE3, ORDERS_1, SUBSET_1, QUANTAL1,
BOOLE, WAYBEL_0, YELLOW_0, LATTICES, ORDINAL2, FUNCT_5, TARSKI, MCART_1,
PRE_TOPC, SEQM_3, REALSET1, BHSP_3, FINSET_1, WELLORD1, CAT_1, YELLOW_2,
FINSUB_1, WELLORD2, YELLOW_1, FILTER_2, LATTICE2, WAYBEL_1, WAYBEL_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, FINSUB_1, FUNCT_1,
TOLER_1, FINSET_1, PARTFUN1, FUNCT_2, PRE_TOPC, STRUCT_0, REALSET1,
ORDERS_1, ORDERS_3, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2,
WAYBEL_1, YELLOW_3, YELLOW_4;
constructors FINSUB_1, ORDERS_3, YELLOW_3, YELLOW_4, WAYBEL_1, TOLER_1,
MEMBERED, PRE_TOPC;
clusters STRUCT_0, LATTICE3, FINSET_1, WAYBEL_0, YELLOW_0, YELLOW_2, YELLOW_3,
YELLOW_4, WAYBEL_1, RELSET_1, FINSUB_1, SUBSET_1, RELAT_1, FUNCT_2,
PARTFUN1;
requirements SUBSET, BOOLE;
definitions WAYBEL_1, YELLOW_0, LATTICE3, ORDERS_3, TARSKI, WAYBEL_0,
XBOOLE_0;
theorems BORSUK_1, FINSUB_1, FUNCT_1, FUNCT_2, LATTICE3, MCART_1, ORDERS_1,
ORDERS_3, PRE_TOPC, RELAT_1, STRUCT_0, TARSKI, WAYBEL_0, YELLOW_0,
ZFMISC_1, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4, WELLORD1,
FUNCT_5, REALSET1, TEX_1, XBOOLE_1;
schemes FINSET_1, SUPINF_2, YELLOW_3, FUNCT_2;
begin :: Preliminaries
definition let X, Y be non empty set,
f be Function of X, Y,
Z be non empty Subset of X;
cluster f.:Z -> non empty;
coherence
proof
consider x being Element of Z;
A1: dom f = X by FUNCT_2:def 1;
then f.x in rng f by FUNCT_1:def 5;
hence thesis by A1,FUNCT_1:def 12;
end;
end;
definition
cluster reflexive connected -> with_infima with_suprema (non empty RelStr);
coherence
proof
let L be non empty RelStr such that
A1: L is reflexive connected;
thus L is with_infima
proof
let x, y be Element of L;
per cases by A1,WAYBEL_0:def 29;
suppose
A2: x <= y;
take z = x;
thus z <= x & z <= y by A1,A2,YELLOW_0:def 1;
thus thesis;
suppose
A3: y <= x;
take z = y;
thus z <= x & z <= y by A1,A3,YELLOW_0:def 1;
thus thesis;
end;
let x, y be Element of L;
per cases by A1,WAYBEL_0:def 29;
suppose
A4: x <= y;
take z = y;
thus z >= x & z >= y by A1,A4,YELLOW_0:def 1;
thus thesis;
suppose
A5: y <= x;
take z = x;
thus z >= x & z >= y by A1,A5,YELLOW_0:def 1;
thus thesis;
end;
end;
definition let C be Chain;
cluster [#]C -> directed;
coherence;
end;
theorem Th1:
for L being up-complete Semilattice
for D being non empty directed Subset of L, x being Element of L
holds ex_sup_of {x} "/\" D,L
proof
let L be up-complete Semilattice,
D be non empty directed Subset of L,
x be Element of L;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
ex_sup_of xx "/\" D,L by WAYBEL_0:75;
hence ex_sup_of {x} "/\" D,L;
end;
theorem
for L being up-complete sup-Semilattice
for D being non empty directed Subset of L, x being Element of L
holds ex_sup_of {x} "\/" D,L
proof
let L be up-complete sup-Semilattice,
D be non empty directed Subset of L,
x be Element of L;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
ex_sup_of xx "\/" D,L by WAYBEL_0:75;
hence ex_sup_of {x} "\/" D,L;
end;
theorem Th3:
for L being up-complete sup-Semilattice
for A, B being non empty directed Subset of L
holds A is_<=_than sup (A "\/" B)
proof
let L be up-complete sup-Semilattice,
A, B be non empty directed Subset of L;
A1: A "\/" B = { x "\/" y where x, y is Element of L : x in A & y in B }
by YELLOW_4:def 3;
ex_sup_of A "\/" B,L by WAYBEL_0:75;
then A2: A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def 9;
let x be Element of L such that
A3: x in A;
consider b being Element of B;
x "\/" b in A "\/" B by A1,A3;
then A4: x "\/" b <= sup (A "\/" B) by A2,LATTICE3:def 9;
ex xx being Element of L st x <= xx & b <= xx &
for c being Element of L st x <= c & b <= c holds xx <= c
by LATTICE3:def 10;
then x <= x "\/" b by LATTICE3:def 13;
hence x <= sup (A "\/" B) by A4,YELLOW_0:def 2;
end;
theorem Th4:
for L being up-complete sup-Semilattice
for A, B being non empty directed Subset of L
holds sup (A "\/" B) = sup A "\/" sup B
proof
let L be up-complete sup-Semilattice,
A, B be non empty directed Subset of L;
A1: ex_sup_of A "\/" B,L by WAYBEL_0:75;
A2: ex_sup_of A,L & ex_sup_of B,L by WAYBEL_0:75;
then A is_<=_than sup A & B is_<=_than sup B by YELLOW_0:30;
then A "\/" B is_<=_than sup A "\/" sup B by YELLOW_4:27;
then A3: sup (A "\/" B) <= sup A "\/" sup B by A1,YELLOW_0:def 9;
A is_<=_than sup (A "\/" B) & B is_<=_than sup (A "\/" B) by Th3;
then sup A <= sup (A "\/" B) & sup B <= sup (A "\/" B) by A2,YELLOW_0:30;
then A4: sup A "\/" sup B <= sup (A "\/" B) "\/" sup (A "\/" B) by YELLOW_3:3;
sup (A "\/" B) <= sup (A "\/" B);
then sup (A "\/" B) "\/" sup (A "\/" B) = sup (A "\/" B) by YELLOW_0:24;
hence thesis by A3,A4,ORDERS_1:25;
end;
theorem Th5:
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds
{ sup ({x} "/\" proj2 D) where x is Element of L : x in proj1 D }
= { sup X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D }
proof
let L be up-complete Semilattice,
D be non empty directed Subset of [:L,L:];
defpred P[set] means
ex x being Element of L st $1 = {x} "/\" proj2 D & x in proj1 D;
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L
by YELLOW_3:21,22;
thus { sup ({x} "/\" proj2 D) where x is Element of L : x in proj1 D }
c= { sup X where X is non empty directed Subset of L: P[X] }
proof
let q be set;
assume q in {sup ({x} "/\" proj2 D) where x is Element of L : x in
proj1 D};
then consider x being Element of L such that
A1: q = sup ({x} "/\" D2) & x in D1;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
xx "/\" D2 is non empty directed;
hence q in { sup X where X is non empty directed Subset of L: P[X] }
by A1;
end;
let q be set;
assume q in { sup X where X is non empty directed Subset of L: P[X] };
then consider X being non empty directed Subset of L such that
A2: q = sup X & P[X];
thus q in { sup ({x} "/\" proj2 D) where x is Element of L : x in proj1 D}
by A2;
end;
theorem Th6:
for L being Semilattice, D being non empty directed Subset of [:L,L:] holds
union {X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D}
= proj1 D "/\" proj2 D
proof
let L be Semilattice,
D be non empty directed Subset of [:L,L:];
set D1 = proj1 D,
D2 = proj2 D;
defpred P[set] means
ex x being Element of L st $1 = {x} "/\" proj2 D & x in proj1 D;
A1: D1 "/\" D2 = { x "/\" y where x, y is Element of L : x in D1 & y in D2 }
by YELLOW_4:def 4;
thus union {X where X is non empty directed Subset of L: P[X]} c= D1 "/\"
D2
proof
let q be set;
assume q in union {X where X is non empty directed Subset of L: P[X]};
then consider w being set such that
A2: q in w & w in {X where X is non empty directed Subset of L: P[X]}
by TARSKI:def 4;
consider e being non empty directed Subset of L such that
A3: w = e & P[e] by A2;
consider p being Element of L such that
A4: e = {p} "/\" D2 & p in D1 by A3;
{p} "/\" D2 = { p "/\"
y where y is Element of L : y in D2 } by YELLOW_4:42;
then consider y being Element of L such that
A5: q = p "/\" y & y in D2 by A2,A3,A4;
thus q in D1 "/\" D2 by A1,A4,A5;
end;
let q be set;
assume q in D1 "/\" D2;
then consider x, y being Element of L such that
A6: q = x "/\" y & x in D1 & y in D2 by A1;
{x} "/\" D2 = { x "/\"
d where d is Element of L : d in D2 } by YELLOW_4:42;
then A7: q in {x} "/\" D2 by A6;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
reconsider T = D2 as non empty directed Subset of L by YELLOW_3:21,22;
xx "/\" T is non empty directed;
then {x} "/\" D2 in {X where X is non empty directed Subset of L: P[X]}
by A6;
hence q in union {X where X is non empty directed Subset of L: P[X]}
by A7,TARSKI:def 4;
end;
theorem Th7:
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds
ex_sup_of union {X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L
proof
let L be up-complete Semilattice,
D be non empty directed Subset of [:L,L:];
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L
by YELLOW_3:21,22;
set A = {X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" D2 & x in D1};
union A c= the carrier of L
proof
let q be set;
assume q in union A;
then consider r being set such that
A1: q in r & r in A by TARSKI:def 4;
consider s being non empty directed Subset of L such that
A2: r = s &
ex x being Element of L st s = {x} "/\" D2 & x in D1 by A1;
thus q in the carrier of L by A1,A2;
end;
then reconsider S = union A as Subset of L;
S = D1 "/\" D2 by Th6;
hence thesis by WAYBEL_0:75;
end;
theorem Th8:
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds
ex_sup_of {sup X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L
proof
let L be up-complete Semilattice,
D be non empty directed Subset of [:L,L:];
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L
by YELLOW_3:21,22;
defpred P[set] means
ex x being Element of L st $1 = {x} "/\" D2 & x in D1;
set A = {sup X where X is non empty directed Subset of L: P[X]};
A c= the carrier of L
proof
let q be set;
assume q in A;
then consider X being non empty directed Subset of L such that
A1: q = sup X & P[X];
thus q in the carrier of L by A1;
end;
then reconsider A as Subset of L;
set R = {X where X is non empty directed Subset of L: P[X]};
union R c= the carrier of L
proof
let q be set;
assume q in union R;
then consider r being set such that
A2: q in r & r in R by TARSKI:def 4;
consider s being non empty directed Subset of L such that
A3: r = s &
ex x being Element of L st s = {x} "/\" D2 & x in D1 by A2;
thus q in the carrier of L by A2,A3;
end;
then reconsider UR = union R as Subset of L;
set a = sup UR;
A4: ex_sup_of UR,L by Th7;
A5: A is_<=_than a
proof
let b be Element of L;
assume b in A;
then consider X being non empty directed Subset of L such that
A6: b = sup X & P[X];
A7: ex_sup_of X,L by WAYBEL_0:75;
X in R by A6;
then X c= UR by ZFMISC_1:92;
hence b <= a by A4,A6,A7,YELLOW_0:34;
end;
for b being Element of L st A is_<=_than b holds a <= b
proof
let b be Element of L such that
A8: A is_<=_than b;
UR is_<=_than b
proof
let k be Element of L;
assume k in UR;
then consider k1 being set such that
A9: k in k1 and
A10: k1 in R by TARSKI:def 4;
consider s being non empty directed Subset of L such that
A11: k1 = s and
A12: P[s] by A10;
consider x being Element of L such that
A13: s = {x} "/\" D2 & x in D1 by A12;
{x} "/\" D2 = {x "/\" d2 where d2 is Element of L: d2 in D2}
by YELLOW_4:42;
then consider d2 being Element of L such that
A14: k = x "/\" d2 & d2 in D2 by A9,A11,A13;
sup s in A by A12;
then A15: sup s <= b by A8,LATTICE3:def 9;
ex_sup_of s,L by A13,Th1;
then x "/\" d2 <= sup s by A9,A11,A14,YELLOW_4:1;
hence k <= b by A14,A15,YELLOW_0:def 2;
end;
hence a <= b by A4,YELLOW_0:def 9;
end;
hence thesis by A5,YELLOW_0:15;
end;
theorem Th9:
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds
"\/" ({ sup X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D },L)
<= "\/" (union {X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L)
proof
let L be up-complete Semilattice,
D be non empty directed Subset of [:L,L:];
defpred P[set] means
ex x being Element of L st $1 = {x} "/\" proj2 D & x in proj1 D;
A1: ex_sup_of { sup X where X is non empty directed Subset of L: P[X] },L
by Th8;
"\/"(union {X where X is non empty directed Subset of L: P[X]},L)
is_>=_than { sup X where X is non empty directed Subset of L: P[X] }
proof
let a be Element of L;
assume a in { sup X where X is non empty directed Subset of L:
P[X] };
then consider q being non empty directed Subset of L such that
A2: a = sup q & P[q];
A3: ex_sup_of q,L by WAYBEL_0:75;
A4: ex_sup_of union {X where X is non empty directed Subset of L:
P[X]},L by Th7;
q in {X where X is non empty directed Subset of L: P[X]} by A2;
then q c= union {X where X is non empty directed Subset of L: P[X]}
by ZFMISC_1:92;
hence a <= "\/"(union {X where X is non empty directed Subset of L:
P[X]},L) by A2,A3,A4,YELLOW_0:34;
end;
hence thesis by A1,YELLOW_0:def 9;
end;
theorem Th10:
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds
"\/" ({ sup X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L)
= "\/" (union {X where X is non empty directed Subset of L:
ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L)
proof
let L be up-complete Semilattice,
D be non empty directed Subset of [:L,L:];
defpred P[set] means
ex x being Element of L st $1 = {x} "/\" proj2 D & x in proj1 D;
A1: "\/" ({ sup X where X is non empty directed Subset of L: P[X] },L)
<= "\/"(union {X where X is non empty directed Subset of L: P[X]},L)
by Th9;
A2: ex_sup_of union {X where X is non empty directed Subset of L: P[X]},L
by Th7;
union {X where X is non empty directed Subset of L: P[X]}
is_<=_than "\/" ({ "\/"(X,L) where X is non empty directed Subset of L:
P[X] },L)
proof
let a be Element of L;
assume a in union {X where X is non empty directed Subset of L: P[X]};
then consider b being set such that
A3: a in b & b in {X where X is non empty directed Subset of L: P[X]}
by TARSKI:def 4;
consider c being non empty directed Subset of L such that
A4: b = c & P[c] by A3;
ex_sup_of c,L by WAYBEL_0:75;
then A5: a <= "\/"(c,L) by A3,A4,YELLOW_4:1;
A6: ex_sup_of {"\/"(X,L) where X is non empty directed Subset of L:P[X]},L
by Th8;
"\/"(c,L) in { "\/"
(X,L) where X is non empty directed Subset of L: P[X] }
by A4;
then "\/"(c,L) <= "\/" ({ "\/"(X,L) where X is non empty directed Subset
of L:
P[X] },L) by A6,YELLOW_4:1;
hence a <= "\/" ({ "\/"(X,L) where X is non empty directed Subset of L:
P[X] },L) by A5,YELLOW_0:def 2;
end;
then "\/"(union {X where X is non empty directed Subset of L: P[X]},L)
<= "\/" ({ "\/"(X,L) where X is non empty directed Subset of L:
P[X] },L) by A2,YELLOW_0:def 9;
hence thesis by A1,ORDERS_1:25;
end;
definition let S, T be up-complete (non empty reflexive RelStr);
cluster [:S,T:] -> up-complete;
coherence
proof
let X be non empty directed Subset of [:S,T:];
reconsider X1 = proj1 X as non empty directed Subset of S
by YELLOW_3:21,22;
reconsider X2 = proj2 X as non empty directed Subset of T
by YELLOW_3:21,22;
consider x being Element of S such that
A1: x is_>=_than X1 and
A2: for z being Element of S st z is_>=_than X1 holds x <= z
by WAYBEL_0:def 39;
consider y being Element of T such that
A3: y is_>=_than X2 and
A4: for z being Element of T st z is_>=_than X2 holds y <= z
by WAYBEL_0:def 39;
take [x,y];
thus [x,y] is_>=_than X by A1,A3,YELLOW_3:31;
let z be Element of [:S,T:] such that
A5: z is_>=_than X;
the carrier of [:S,T:] = [:the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then A6: z = [z`1,z`2] by MCART_1:23;
then z`1 is_>=_than X1 & z`2 is_>=_than X2 by A5,YELLOW_3:31;
then x <= z`1 & y <= z`2 by A2,A4;
hence [x,y] <= z by A6,YELLOW_3:11;
end;
end;
theorem
for S, T being non empty reflexive antisymmetric RelStr
st [:S,T:] is up-complete holds S is up-complete & T is up-complete
proof
let S, T be non empty reflexive antisymmetric RelStr such that
A1: [:S,T:] is up-complete;
thus S is up-complete
proof
let X be non empty directed Subset of S;
consider D being non empty directed Subset of T;
consider x being Element of [:S,T:] such that
A2: x is_>=_than [:X,D:] and
A3: for y being Element of [:S,T:] st y is_>=_than [:X,D:] holds x <= y
by A1,WAYBEL_0:def 39;
take x`1;
the carrier of [:S,T:] = [:the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then A4: x = [x`1,x`2] by MCART_1:23;
hence x`1 is_>=_than X by A2,YELLOW_3:29;
let y be Element of S such that
A5: y is_>=_than X;
ex_sup_of [:X,D:],[:S,T:] by A1,WAYBEL_0:75;
then ex_sup_of D,T by YELLOW_3:39;
then sup D is_>=_than D by YELLOW_0:def 9;
then [y,sup D] is_>=_than [:X,D:] by A5,YELLOW_3:30;
then x <= [y,sup D] by A3;
hence x`1 <= y by A4,YELLOW_3:11;
end;
let X be non empty directed Subset of T;
consider D being non empty directed Subset of S;
consider x being Element of [:S,T:] such that
A6: x is_>=_than [:D,X:] and
A7: for y being Element of [:S,T:] st y is_>=_than [:D,X:] holds x <= y
by A1,WAYBEL_0:def 39;
take x`2;
the carrier of [:S,T:] = [:the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then A8: x = [x`1,x`2] by MCART_1:23;
hence x`2 is_>=_than X by A6,YELLOW_3:29;
let y be Element of T such that
A9: y is_>=_than X;
ex_sup_of [:D,X:],[:S,T:] by A1,WAYBEL_0:75;
then ex_sup_of D,S by YELLOW_3:39;
then sup D is_>=_than D by YELLOW_0:def 9;
then [sup D,y] is_>=_than [:D,X:] by A9,YELLOW_3:30;
then x <= [sup D,y] by A7;
hence x`2 <= y by A8,YELLOW_3:11;
end;
theorem Th12:
for L being up-complete antisymmetric (non empty reflexive RelStr)
for D being non empty directed Subset of [:L,L:]
holds sup D = [sup proj1 D,sup proj2 D]
proof
let L be up-complete antisymmetric (non empty reflexive RelStr),
D be non empty directed Subset of [:L,L:];
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L
by YELLOW_3:21,22;
reconsider C = the carrier of L as non empty set;
D c= the carrier of [:L,L:]; then
D c= [:the carrier of L, the carrier of L:] by YELLOW_3:def 2; then
reconsider D' = D as non empty Subset of [:C,C:];
A1: ex_sup_of D1,L & ex_sup_of D2,L by WAYBEL_0:75;
A2: ex_sup_of D,[:L,L:] by WAYBEL_0:75;
A3: ex_sup_of [:D1,D2:],[:L,L:] by WAYBEL_0:75;
the carrier of [:L,L:] = [:C,C:] by YELLOW_3:def 2;
then consider d1, d2 being set such that
A4: d1 in C & d2 in C & sup D = [d1,d2] by ZFMISC_1:def 2;
reconsider d1, d2 as Element of L by A4;
A5: D1 is_<=_than d1
proof
let b be Element of L; assume
b in D1;
then consider x being set such that
A6: [b,x] in D by FUNCT_5:def 1;
reconsider x as Element of D2 by A6,FUNCT_5:4;
D is_<=_than [d1,d2] by A2,A4,YELLOW_0:def 9;
then [b,x] <= [d1,d2] by A6,LATTICE3:def 9;
hence b <= d1 by YELLOW_3:11;
end;
D2 is_<=_than d2
proof
let b be Element of L; assume
b in D2;
then consider x being set such that
A7: [x,b] in D by FUNCT_5:def 2;
reconsider x as Element of D1 by A7,FUNCT_5:4;
D is_<=_than [d1,d2] by A2,A4,YELLOW_0:def 9;
then [x,b] <= [d1,d2] by A7,LATTICE3:def 9;
hence b <= d2 by YELLOW_3:11;
end;
then sup D1 <= d1 & sup D2 <= d2 by A1,A5,YELLOW_0:def 9;
then A8: [sup D1,sup D2] <= sup D by A4,YELLOW_3:11;
reconsider D1, D2 as non empty Subset of L;
D' c= [:D1,D2:] by YELLOW_3:1;
then sup D <= sup [:D1,D2:] by A2,A3,YELLOW_0:34;
then sup D <= [sup proj1 D,sup proj2 D] by A1,YELLOW_3:43;
hence [sup proj1 D,sup proj2 D] = sup D by A8,ORDERS_1:25;
end;
theorem Th13:
for S1, S2 being RelStr, D being Subset of S1
for f being map of S1,S2 st f is monotone holds
f.:(downarrow D) c= downarrow (f.:D)
proof
let S1, S2 be RelStr,
D be Subset of S1,
f be map of S1,S2 such that
A1: f is monotone;
let q be set; assume
A2: q in f.:(downarrow D);
then consider x being set such that
A3: x in dom f & x in downarrow D & q = f.x by FUNCT_1:def 12;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A2,A3,STRUCT_0:def 1;
reconsider f1 = f as map of s1,s2;
reconsider x as Element of s1 by A3;
consider y being Element of s1 such that
A4: x <= y & y in D by A3,WAYBEL_0:def 15;
f1.x is Element of s2;
then reconsider q1 = q, fy = f1.y as Element of s2 by A3;
A5: q1 <= fy by A1,A3,A4,ORDERS_3:def 5;
the carrier of s2 <> {};
then dom f = the carrier of s1 by FUNCT_2:def 1;
then f.y in f.:D by A4,FUNCT_1:def 12;
hence q in downarrow (f.:D) by A5,WAYBEL_0:def 15;
end;
theorem Th14:
for S1, S2 being RelStr, D being Subset of S1
for f being map of S1,S2 st f is monotone holds
f.:(uparrow D) c= uparrow (f.:D)
proof
let S1, S2 be RelStr,
D be Subset of S1,
f be map of S1,S2 such that
A1: f is monotone;
let q be set; assume
A2: q in f.:(uparrow D);
then consider x being set such that
A3: x in dom f & x in uparrow D & q = f.x by FUNCT_1:def 12;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A2,A3,STRUCT_0:def 1;
reconsider f1 = f as map of s1,s2;
reconsider x as Element of s1 by A3;
consider y being Element of s1 such that
A4: y <= x & y in D by A3,WAYBEL_0:def 16;
f1.x is Element of s2;
then reconsider q1 = q, fy = f1.y as Element of s2 by A3;
A5: fy <= q1 by A1,A3,A4,ORDERS_3:def 5;
the carrier of s2 <> {};
then dom f = the carrier of s1 by FUNCT_2:def 1;
then f.y in f.:D by A4,FUNCT_1:def 12;
hence q in uparrow (f.:D) by A5,WAYBEL_0:def 16;
end;
definition
cluster trivial -> distributive complemented (non empty reflexive RelStr);
coherence
proof
let L be non empty reflexive RelStr such that
A1: L is trivial;
thus L is distributive
proof
let x,y,z be Element of L;
thus x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\"
z) by A1,REALSET1:def 20;
end;
let x be Element of L;
take y = x;
thus x "\/" y = Top L by A1,REALSET1:def 20;
thus x "/\" y = Bottom L by A1,REALSET1:def 20;
end;
end;
definition
cluster strict non empty trivial LATTICE;
existence
proof
consider B being strict trivial (non empty reflexive RelStr);
take B;
thus thesis;
end;
end;
theorem Th15:
for H being distributive complete LATTICE
for a being Element of H, X being finite Subset of H
holds sup ({a} "/\" X) = a "/\" sup X
proof
let H be distributive complete LATTICE,
a be Element of H,
X be finite Subset of H;
defpred P[set] means
ex A being Subset of H st A = $1 & a "/\" sup A = sup({a} "/\" A);
A1: X is finite;
A2: P[{}]
proof
{} c= the carrier of H by XBOOLE_1:2;
then reconsider A = {} as Subset of H;
take A;
thus A = {};
A3: Bottom H <= a by YELLOW_0:44;
A4: {a} "/\" {}H = {} by YELLOW_4:36;
thus a "/\" sup A = a "/\" Bottom H by YELLOW_0:def 11
.= Bottom H by A3,YELLOW_0:25
.= sup({a} "/\" A) by A4,YELLOW_0:def 11;
end;
A5: for x, B being set st x in X & B c= X & P[B] holds P[B \/ {x}]
proof
let x, B be set such that
A6: x in X & B c= X and
A7: P[B];
consider A being Subset of H such that
A8: A = B & a "/\" sup A = sup({a} "/\" A) by A7;
reconsider x1 = x as Element of H by A6;
B c= the carrier of H & {x1} c= the carrier of H by A6,XBOOLE_1:1;
then B \/ {x} c= the carrier of H by XBOOLE_1:8;
then reconsider C = B \/ {x} as Subset of H;
take C;
thus C = B \/ {x};
A9: ex_sup_of {a} "/\" A,H & ex_sup_of {a "/\" x1},H by YELLOW_0:17;
A10: {a} "/\" C = ({a} "/\" A) \/ ({a} "/\" {x1}) by A8,YELLOW_4:43
.= ({a} "/\" A) \/ {a "/\" x1} by YELLOW_4:46;
ex_sup_of B,H & ex_sup_of {x},H by YELLOW_0:17;
hence a "/\" sup C
= a "/\" ("\/"(B, H) "\/" "\/"({x}, H)) by YELLOW_2:3
.= sup({a} "/\" A) "\/" (a "/\" "\/"({x}, H)) by A8,WAYBEL_1:def 3
.= sup({a} "/\" A) "\/" (a "/\" x1) by YELLOW_0:39
.= sup({a} "/\" A) "\/" sup{a "/\" x1} by YELLOW_0:39
.= sup({a} "/\" C) by A9,A10,YELLOW_2:3;
end;
P[X] from Finite(A1,A2,A5);
hence sup({a} "/\" X) = a "/\" sup X;
end;
theorem
for H being distributive complete LATTICE
for a being Element of H, X being finite Subset of H
holds inf ({a} "\/" X) = a "\/" inf X
proof
let H be distributive complete LATTICE,
a be Element of H,
X be finite Subset of H;
defpred P[set] means
ex A being Subset of H st A = $1 & a "\/" inf A = inf({a} "\/" A);
A1: X is finite;
A2: P[{}]
proof
{} c= the carrier of H by XBOOLE_1:2;
then reconsider A = {} as Subset of H;
take A;
thus A = {};
A3: a <= Top H by YELLOW_0:45;
A4: {a} "\/" {}H = {} by YELLOW_4:9;
thus a "\/" inf A = a "\/" Top H by YELLOW_0:def 12
.= Top H by A3,YELLOW_0:24
.= inf({a} "\/" A) by A4,YELLOW_0:def 12;
end;
A5: for x, B being set st x in X & B c= X & P[B] holds P[B \/ {x}]
proof
let x, B be set such that
A6: x in X & B c= X and
A7: P[B];
consider A being Subset of H such that
A8: A = B & a "\/" inf A = inf({a} "\/" A) by A7;
reconsider x1 = x as Element of H by A6;
B c= the carrier of H & {x1} c= the carrier of H by A6,XBOOLE_1:1;
then B \/ {x} c= the carrier of H by XBOOLE_1:8;
then reconsider C = B \/ {x} as Subset of H;
take C;
thus C = B \/ {x};
A9: ex_inf_of {a} "\/" A,H & ex_inf_of {a "\/" x1},H by YELLOW_0:17;
A10: {a} "\/" C = ({a} "\/" A) \/ ({a} "\/" {x1}) by A8,YELLOW_4:16
.= ({a} "\/" A) \/ {a "\/" x1} by YELLOW_4:19;
ex_inf_of B,H & ex_inf_of {x},H by YELLOW_0:17;
hence a "\/" inf C
= a "\/" ("/\"(B, H) "/\" "/\"({x}, H)) by YELLOW_2:4
.= inf({a} "\/" A) "/\" (a "\/" "/\"({x}, H)) by A8,WAYBEL_1:6
.= inf({a} "\/" A) "/\" (a "\/" x1) by YELLOW_0:39
.= inf({a} "\/" A) "/\" inf{a "\/" x1} by YELLOW_0:39
.= inf({a} "\/" C) by A9,A10,YELLOW_2:4;
end;
P[X] from Finite(A1,A2,A5);
hence inf({a} "\/" X) = a "\/" inf X;
end;
theorem Th17:
for H being complete distributive LATTICE, a being Element of H
for X being finite Subset of H holds a "/\" preserves_sup_of X
proof
let H be complete distributive LATTICE,
a be Element of H,
X be finite Subset of H;
assume ex_sup_of X,H;
thus ex_sup_of a "/\".:X,H by YELLOW_0:17;
thus sup (a"/\".:X) = "\/"({a"/\"y where y is Element of H: y in X},H)
by WAYBEL_1:64
.= sup({a} "/\" X) by YELLOW_4:42
.= a "/\" sup X by Th15
.= a"/\".sup X by WAYBEL_1:def 18;
end;
begin :: The Properties of Nets
scheme ExNet { L() -> non empty RelStr,
N() -> prenet of L(),
F(set) -> Element of L()} :
ex M being prenet of L() st the RelStr of M = the RelStr of N() &
for i being Element of M holds
(the mapping of M).i = F((the mapping of N()).i)
proof
deffunc G(Element of N()) = F((the mapping of N()).$1);
A1: for i being Element of N() holds
G(i) in the carrier of L();
consider f being Function of the carrier of N(), the carrier of L()
such that
A2: for i being Element of N() holds f.i = G(i)
from FunctR_ealEx(A1);
set M = NetStr (# the carrier of N(), the InternalRel of N(), f #);
M is directed
proof
A3: the RelStr of M = the RelStr of N();
A4: [#]N() is directed by WAYBEL_0:def 6;
[#]N() = the carrier of N() by PRE_TOPC:12
.= [#]M by PRE_TOPC:12;
hence [#]M is directed by A3,A4,WAYBEL_0:3;
end;
then reconsider M as prenet of L();
take M;
thus thesis by A2;
end;
theorem Th18:
for L being non empty RelStr
for N being prenet of L st N is eventually-directed
holds rng netmap (N,L) is directed
proof
let L be non empty RelStr,
N be prenet of L such that
A1: N is eventually-directed;
set f = netmap (N,L);
let x, y be Element of L such that
A2: x in rng f and
A3: y in rng f;
consider a being set such that
A4: a in dom f & f.a = x by A2,FUNCT_1:def 5;
consider b being set such that
A5: b in dom f & f.b = y by A3,FUNCT_1:def 5;
A6: dom f = the carrier of N by FUNCT_2:def 1;
reconsider a, b as Element of N by A4,A5;
consider ja being Element of N such that
A7: for k being Element of N st ja <= k holds N.a <= N.k by A1,WAYBEL_0:11;
consider jb being Element of N such that
A8: for k being Element of N st jb <= k holds N.b <= N.k by A1,WAYBEL_0:11;
A9: [#]N = the carrier of N by PRE_TOPC:12;
[#]N is directed by WAYBEL_0:def 6;
then consider c being Element of N such that
A10: c in [#]N & ja <= c & jb <= c by A9,WAYBEL_0:def 1;
take z = f.c;
thus z in rng f by A6,FUNCT_1:def 5;
the mapping of N = netmap(N,L) by WAYBEL_0:def 7;
then N.a = f.a & N.b = f.b & N.c = f.c by WAYBEL_0:def 8;
hence x <= z & y <= z by A4,A5,A7,A8,A10;
end;
theorem Th19:
for L being non empty reflexive RelStr, D being non empty directed Subset of L
for n being Function of D, the carrier of L holds
NetStr (#D,(the InternalRel of L)|_2 D,n#) is prenet of L
proof
let L be non empty reflexive RelStr,
D be non empty directed Subset of L,
n be Function of D, the carrier of L;
set N = NetStr (#D,(the InternalRel of L)|_2 D,n#);
N is directed
proof
let x, y be Element of N;
assume x in [#]N & y in [#]N;
reconsider x1 = x, y1 = y as Element of D;
consider z1 being Element of L such that
A1: z1 in D & x1 <= z1 & y1 <= z1 by WAYBEL_0:def 1;
reconsider z = z1 as Element of N by A1;
take z;
D = [#]N by PRE_TOPC:12;
hence z in [#]N;
N is SubRelStr of L
proof
thus the carrier of N c= the carrier of L;
thus the InternalRel of N c= the InternalRel of L by WELLORD1:15;
end;
then reconsider N as SubRelStr of L;
N is full
proof
thus the InternalRel of N = (the InternalRel of L)|_2 the carrier of N;
end;
hence x <= z & y <= z by A1,YELLOW_0:61;
end;
hence NetStr (#D,(the InternalRel of L)|_2 D,n#) is prenet of L;
end;
theorem Th20:
for L being non empty reflexive RelStr, D being non empty directed Subset of L
for n being Function of D, the carrier of L, N being prenet of L st n = id D &
N = NetStr (#D,(the InternalRel of L)|_2 D,n#) holds N is eventually-directed
proof
let L be non empty reflexive RelStr,
D be non empty directed Subset of L,
n be Function of D, the carrier of L,
N be prenet of L such that
A1: n = id D and
A2: N = NetStr (#D,(the InternalRel of L)|_2 D,n#);
for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds N.i <= N.k
proof
let i be Element of N;
take j = i;
let k be Element of N such that
A3: j <= k;
n.j in the carrier of L & n.k in the carrier of L by A2,FUNCT_2:7;
then reconsider nj = n.j, nk = n.k as Element of L;
k in the carrier of N;
then reconsider k1 = k as Element of L by A2;
A4: N is SubRelStr of L
proof
thus the carrier of N c= the carrier of L by A2;
thus the InternalRel of N c= the InternalRel of L by A2,WELLORD1:15;
end;
A5: nj = j & nk = k by A1,A2,FUNCT_1:35;
then nj <= k1 by A3,A4,YELLOW_0:60;
then N.i <= nk by A2,A5,WAYBEL_0:def 8;
hence N.i <= N.k by A2,WAYBEL_0:def 8;
end;
hence N is eventually-directed by WAYBEL_0:11;
end;
definition let L be non empty RelStr,
N be NetStr over L;
func sup N -> Element of L equals :Def1:
Sup the mapping of N;
coherence;
end;
definition let L be non empty RelStr,
J be set,
f be Function of J,the carrier of L;
func FinSups f -> prenet of L means :Def2:
ex g being Function of Fin J, the carrier of L st
for x being Element of Fin J holds g.x = sup (f.:x) &
it = NetStr (# Fin J, RelIncl Fin J, g #);
existence
proof
deffunc F(Element of Fin J) = sup (f.:$1);
A1: for x being Element of Fin J holds F(x) in the carrier of L;
consider g being Function of Fin J, the carrier of L
such that
A2: for x being Element of Fin J holds g.x = F(x) from FunctR_ealEx(A1);
set M = NetStr (# Fin J, RelIncl Fin J, g #);
M is directed
proof
let x, y be Element of M such that
x in [#]M & y in [#]M;
reconsider x1 = x, y1 = y as Element of Fin J;
reconsider z = x1 \/ y1 as Element of M;
take z;
z in the carrier of M;
hence z in [#]M by PRE_TOPC:12;
A3: InclPoset Fin J = RelStr(#Fin J, RelIncl Fin J#) by YELLOW_1:def 1;
then reconsider x2 = x, y2 = y, z1 = z
as Element of InclPoset Fin J;
x c= z & y c= z by XBOOLE_1:7;
then x2 <= z1 & y2 <= z1 by YELLOW_1:3;
hence x <= z & y <= z by A3,YELLOW_0:1;
end;
then reconsider M as prenet of L;
take M;
thus thesis by A2;
end;
uniqueness
proof
let A, B be prenet of L such that
A4: ex g being Function of Fin J, the carrier of L st
for x being Element of Fin J holds
g.x = sup (f.:x) &
A = NetStr (#Fin J, RelIncl Fin J, g#) and
A5: ex g being Function of Fin J, the carrier of L st
for x being Element of Fin J holds
g.x = sup (f.:x) &
B = NetStr (#Fin J, RelIncl Fin J, g#);
consider g1 being Function of Fin J, the carrier of L
such that
A6: for x being Element of Fin J holds
g1.x = sup (f.:x) &
A = NetStr (#Fin J, RelIncl Fin J, g1#) by A4;
consider g2 being Function of Fin J, the carrier of L
such that
A7: for x being Element of Fin J holds
g2.x = sup (f.:x) &
B = NetStr (#Fin J, RelIncl Fin J, g2#) by A5;
for x being set st x in Fin J holds g1.x = g2.x
proof
let x be set; assume
A8: x in Fin J;
hence g1.x = sup (f.:x) by A6
.= g2.x by A7,A8;
end;
hence A = B by A6,A7,FUNCT_2:18;
end;
end;
theorem
for L being non empty RelStr, J, x being set
for f being Function of J,the carrier of L holds
x is Element of FinSups f iff x is Element of Fin J
proof
let L be non empty RelStr,
J, x be set,
f be Function of J,the carrier of L;
consider g being Function of Fin J, the carrier of L such that
A1: for x being Element of Fin J holds g.x = sup (f.:x) &
FinSups f = NetStr (# Fin J, RelIncl Fin J, g #) by Def2;
thus thesis by A1;
end;
definition let L be complete antisymmetric (non empty reflexive RelStr),
J be set,
f be Function of J,the carrier of L;
cluster FinSups f -> monotone;
coherence
proof
let x, y be Element of FinSups f such that
A1: x <= y;
consider g being Function of Fin J, the carrier of L
such that
A2: for x being Element of Fin J holds g.x = sup (f.:x) &
FinSups f = NetStr (# Fin J, RelIncl Fin J, g #) by Def2;
A3: ex_sup_of f.:x,L by YELLOW_0:17;
A4: ex_sup_of f.:y,L by YELLOW_0:17;
g.x = sup (f.:x) & g.y = sup (f.:y) by A2;
then reconsider fx = g.x as Element of L;
A5: InclPoset Fin J = RelStr(#Fin J, RelIncl Fin J#) by YELLOW_1:def 1;
then reconsider x1 = x, y1 = y
as Element of InclPoset Fin J by A2;
let a, b be Element of L such that
A6: a = netmap(FinSups f,L).x & b = netmap(FinSups f,L).y;
A7: g = netmap(FinSups f,L) by A2,WAYBEL_0:def 7;
x1 <= y1 by A1,A2,A5,YELLOW_0:1;
then x c= y by YELLOW_1:3;
then f.:x c= f.:y by RELAT_1:156;
then sup (f.:x) <= sup (f.:y) by A3,A4,YELLOW_0:34;
then fx <= sup (f.:y) by A2;
hence a <= b by A2,A6,A7;
end;
end;
definition let L be non empty RelStr,
x be Element of L,
N be non empty NetStr over L;
func x "/\" N -> strict NetStr over L means :Def3:
the RelStr of it = the RelStr of N &
for i being Element of it ex y being Element of L st
y = (the mapping of N).i & (the mapping of it).i = x "/\" y;
existence
proof
defpred P[set,set] means
ex y being Element of L st y = (the mapping of N).$1 & $2 = x "/\" y;
A1: for e being Element of N
ex u being Element of L st P[e,u]
proof
let e be Element of N;
take x "/\" (the mapping of N).e, (the mapping of N).e;
thus thesis;
end;
ex g being Function of the carrier of N, the carrier of L st
for i being Element of N holds P[i,g.i] from FuncExD(A1);
then
consider g being Function of the carrier of N, the carrier of L such that
A2: for i being Element of N ex y being Element of L st
y = (the mapping of N).i & g.i = x "/\" y;
take NetStr (#the carrier of N,the InternalRel of N,g#);
thus thesis by A2;
end;
uniqueness
proof
let A, B be strict NetStr over L such that
A3: the RelStr of A = the RelStr of N &
for i being Element of A ex y being Element of L st
y = (the mapping of N).i & (the mapping of A).i = x "/\" y and
A4: the RelStr of B = the RelStr of N &
for i being Element of B ex y being Element of L st
y = (the mapping of N).i & (the mapping of B).i = x "/\" y;
reconsider C = the carrier of A as non empty set by A3;
reconsider f1 = the mapping of A, f2 = the mapping of B as
Function of C, the carrier of L by A3,A4;
for c being Element of C holds f1.c = f2.c
proof
let c be Element of C;
consider ya being Element of L such that
A5: ya = (the mapping of N).c & f1.c = x "/\" ya by A3;
consider yb being Element of L such that
A6: yb = (the mapping of N).c & f2.c = x "/\" yb by A3,A4;
thus f1.c = f2.c by A5,A6;
end;
hence A = B by A3,A4,FUNCT_2:113;
end;
end;
theorem Th22:
for L being non empty RelStr, N being non empty NetStr over L
for x being Element of L, y being set holds
y is Element of N iff y is Element of x "/\" N
proof
let L be non empty RelStr,
N be non empty NetStr over L,
x be Element of L,
y be set;
the RelStr of x "/\" N = the RelStr of N by Def3;
hence y is Element of N iff y is Element of x "/\" N;
end;
definition let L be non empty RelStr,
x be Element of L,
N be non empty NetStr over L;
cluster x "/\" N -> non empty;
coherence
proof
the RelStr of x "/\" N = the RelStr of N by Def3;
hence thesis by STRUCT_0:def 1;
end;
end;
definition let L be non empty RelStr,
x be Element of L,
N be prenet of L;
cluster x "/\" N -> directed;
coherence
proof
A1: the RelStr of x "/\" N = the RelStr of N by Def3;
A2: [#]N is directed by WAYBEL_0:def 6;
[#]N = the carrier of N by PRE_TOPC:12
.= [#](x "/\" N) by A1,PRE_TOPC:12;
hence [#](x "/\" N) is directed by A1,A2,WAYBEL_0:3;
end;
end;
theorem Th23:
for L being non empty RelStr, x being Element of L
for F being non empty NetStr over L
holds rng (the mapping of x "/\" F) = {x} "/\" rng the mapping of F
proof
let L be non empty RelStr,
x be Element of L,
F be non empty NetStr over L;
set f = the mapping of F,
h = the mapping of x "/\" F,
A = rng the mapping of F;
A1: the RelStr of x "/\" F = the RelStr of F by Def3;
A2: {x} "/\" A = {x "/\" y where y is Element of L: y in A} by YELLOW_4:42;
A3: dom f = the carrier of F by FUNCT_2:def 1;
A4: dom h = the carrier of F by A1,FUNCT_2:def 1;
thus rng the mapping of x "/\" F c= {x} "/\" A
proof
let q be set;
assume q in rng h;
then consider a being set such that
A5: a in dom h & q = h.a by FUNCT_1:def 5;
reconsider a as Element of x "/\" F
by A5;
consider y being Element of L such that
A6: y = f.a & h.a = x "/\" y by Def3;
y in A by A1,A3,A6,FUNCT_1:def 5;
hence q in {x} "/\" A by A2,A5,A6;
end;
let q be set;
assume q in {x} "/\" A;
then consider y being Element of L such that
A7: q = x "/\" y & y in A by A2;
consider z being set such that
A8: z in dom f & y = f.z by A7,FUNCT_1:def 5;
reconsider z as Element of x "/\" F by A1,A8;
consider w being Element of L such that
A9: w = f.z & h.z = x "/\" w by Def3;
thus q in rng h by A4,A7,A8,A9,FUNCT_1:def 5;
end;
theorem Th24:
for L being non empty RelStr, J being set
for f being Function of J,the carrier of L
st for x being set holds ex_sup_of f.:x,L
holds rng netmap(FinSups f,L) c= finsups rng f
proof
let L be non empty RelStr,
J be set,
f be Function of J,the carrier of L such that
A1: for x being set holds ex_sup_of f.:x,L;
set h = netmap(FinSups f,L);
A2: finsups rng f = {"\/"(Y,L) where Y is finite Subset of rng f:
ex_sup_of Y,L} by WAYBEL_0:def 27;
consider g being Function of Fin J, the carrier of L such that
A3: for x being Element of Fin J holds g.x = sup (f.:x) &
FinSups f = NetStr (# Fin J, RelIncl Fin J, g #) by Def2;
let q be set;
assume q in rng h;
then consider x being set such that
A4: x in dom h & h.x = q by FUNCT_1:def 5;
reconsider x as Element of Fin J by A3,A4;
g = h by A3,WAYBEL_0:def 7;
then A5: h.x = sup (f.:x) by A3;
A6: f.:x is finite Subset of rng f by RELAT_1:144;
ex_sup_of f.:x,L by A1;
hence q in finsups rng f by A2,A4,A5,A6;
end;
theorem Th25:
for L being non empty reflexive antisymmetric RelStr, J being set
for f being Function of J,the carrier of L
holds rng f c= rng netmap (FinSups f,L)
proof
let L be non empty reflexive antisymmetric RelStr,
J be set,
f be Function of J,the carrier of L;
per cases;
suppose
A1: J is non empty;
let a be set;
assume a in rng f;
then consider b being set such that
A2: b in dom f & a = f.b by FUNCT_1:def 5;
consider g being Function of Fin J, the carrier of L such that
A3: for x being Element of Fin J holds g.x = sup (f.:x) &
FinSups f = NetStr (# Fin J, RelIncl Fin J, g #) by Def2;
A4: g = netmap (FinSups f,L) by A3,WAYBEL_0:def 7;
reconsider b as Element of J by A2;
{b} c= J by A1,ZFMISC_1:37;
then reconsider x = {b} as Element of Fin J by FINSUB_1:def 5;
dom g = Fin J by FUNCT_2:def 1;
then A5: x in dom g;
f.b in rng f by A2,FUNCT_1:def 5;
then reconsider fb = f.b as Element of L;
g.{b} = sup (f.:x) by A3
.= sup {fb} by A2,FUNCT_1:117
.= a by A2,YELLOW_0:39;
hence a in rng netmap (FinSups f,L) by A4,A5,FUNCT_1:def 5;
suppose
A6: J is empty;
dom f = J by FUNCT_2:def 1;
then rng f = {} by A6,RELAT_1:65;
hence thesis by XBOOLE_1:2;
end;
theorem Th26:
for L being non empty reflexive antisymmetric RelStr, J being set
for f being Function of J,the carrier of L st
ex_sup_of rng f,L & ex_sup_of rng netmap (FinSups f,L),L &
for x being Element of Fin J holds ex_sup_of f.:x,L
holds Sup f = sup FinSups f
proof
let L be non empty reflexive antisymmetric RelStr,
J be set,
f be Function of J,the carrier of L such that
A1: ex_sup_of rng f,L & ex_sup_of rng netmap (FinSups f,L),L and
A2: for x being Element of Fin J holds ex_sup_of f.:x,L;
set h = netmap (FinSups f,L);
rng f c= rng h by Th25;
then A3: "\/"(rng f,L) <= sup rng h by A1,YELLOW_0:34;
rng h is_<=_than "\/"(rng f,L)
proof
let a be Element of L;
assume a in rng h;
then consider x being set such that
A4: x in dom h & a = h.x by FUNCT_1:def 5;
consider g being Function of Fin J, the carrier of L such that
A5: for x being Element of Fin J holds g.x = sup (f.:x) &
FinSups f = NetStr (# Fin J, RelIncl Fin J, g #) by Def2;
reconsider x as Element of Fin J by A4,A5;
A6: g = h by A5,WAYBEL_0:def 7;
A7: ex_sup_of f.:x,L by A2;
f.:x c= rng f by RELAT_1:144;
then sup(f.:x) <= "\/"(rng f,L) by A1,A7,YELLOW_0:34;
hence a <= "\/"(rng f,L) by A4,A5,A6;
end;
then A8: sup rng h <= "\/"(rng f,L) by A1,YELLOW_0:def 9;
thus Sup f = "\/"(rng f,L) by YELLOW_2:def 5
.= sup rng netmap (FinSups f,L) by A3,A8,ORDERS_1:25
.= Sup netmap (FinSups f,L) by YELLOW_2:def 5
.= Sup the mapping of FinSups f by WAYBEL_0:def 7
.= sup FinSups f by Def1;
end;
theorem Th27:
for L being with_infima antisymmetric transitive RelStr, N being prenet of L
for x being Element of L st N is eventually-directed
holds x "/\" N is eventually-directed
proof
let L be with_infima antisymmetric transitive RelStr,
N be prenet of L,
x be Element of L such that
A1: N is eventually-directed;
A2: the RelStr of x "/\" N = the RelStr of N by Def3;
for i being Element of x "/\" N ex j being Element of x "/\" N st
for k being Element of x "/\" N st j <= k holds (x "/\" N).i <= (x "/\"
N).k
proof
let i1 be Element of x "/\" N;
reconsider i = i1 as Element of N by Th22;
consider j being Element of N such that
A3: for k being Element of N st j <= k holds N.i <= N.k by A1,WAYBEL_0:11;
reconsider j1 = j as Element of x "/\" N by Th22;
take j1;
let k1 be Element of x "/\" N;
reconsider k = k1 as Element of N by Th22;
assume j1 <= k1;
then j <= k by A2,YELLOW_0:1;
then A4: N.i <= N.k by A3;
consider yi being Element of L such that
A5: yi = (the mapping of N).i1 & (the mapping of x "/\" N).i1 = x "/\"
yi by Def3;
consider yk being Element of L such that
A6: yk = (the mapping of N).k1 & (the mapping of x "/\" N).k1 = x "/\"
yk by Def3;
A7: (x "/\" N).i1 = x "/\" yi by A5,WAYBEL_0:def 8
.= x "/\" (N.i) by A5,WAYBEL_0:def 8;
(x "/\" N).k1 = x "/\" yk by A6,WAYBEL_0:def 8
.= x "/\" (N.k) by A6,WAYBEL_0:def 8;
hence (x "/\" N).i1 <= (x "/\" N).k1 by A4,A7,WAYBEL_1:2;
end;
hence x "/\" N is eventually-directed by WAYBEL_0:11;
end;
theorem Th28:
for L being up-complete Semilattice st
for x being Element of L, E being non empty directed Subset of L
st x <= sup E holds x <= sup ({x} "/\" E) holds
for D being non empty directed Subset of L, x being Element of L
holds x "/\" sup D = sup ({x} "/\" D)
proof
let L be up-complete Semilattice such that
A1: for x being Element of L, E being non empty directed Subset of L
st x <= sup E holds x <= sup ({x} "/\" E);
let D be non empty directed Subset of L,
x be Element of L;
ex w being Element of L st x >= w & sup D >= w &
for c being Element of L st x >= c & sup D >= c holds w >= c
by LATTICE3:def 11;
then x "/\" sup D <= sup D by LATTICE3:def 14;
then A2: x "/\" sup D <= sup ({x "/\" sup D} "/\" D) by A1;
ex_sup_of D,L by WAYBEL_0:75;
then A3: sup D is_>=_than D by YELLOW_0:30;
reconsider T = {x "/\" sup D} as non empty directed Subset of L
by WAYBEL_0:5;
A4: ex_sup_of T "/\" D,L by WAYBEL_0:75;
{x "/\" sup D} "/\" D is_<=_than x "/\" sup D by YELLOW_4:52;
then sup ({x "/\" sup D} "/\" D) <= x "/\" sup D by A4,YELLOW_0:30;
hence x "/\" sup D = sup ({x "/\" sup D} "/\" D) by A2,ORDERS_1:25
.= sup ({x} "/\" {sup D} "/\" D) by YELLOW_4:46
.= sup ({x} "/\" ({sup D} "/\" D)) by YELLOW_4:41
.= sup ({x} "/\" D) by A3,YELLOW_4:51;
end;
theorem
for L being with_suprema Poset st
for X being directed Subset of L, x being Element of L
holds x "/\" sup X = sup ({x} "/\" X) holds
for X being Subset of L, x being Element of L st ex_sup_of X,L holds
x "/\" sup X = sup ({x} "/\" finsups X)
proof
let L be with_suprema Poset such that
A1: for X being directed Subset of L, x being Element of L
holds x "/\" sup X = sup ({x} "/\" X);
let X be Subset of L,
x be Element of L;
assume ex_sup_of X,L;
hence x "/\" sup X = x "/\" sup finsups X by WAYBEL_0:55
.= sup ({x} "/\" finsups X) by A1;
end;
theorem
for L being up-complete LATTICE st
for X being Subset of L, x being Element of L holds
x "/\" sup X = sup ({x} "/\" finsups X) holds
for X being non empty directed Subset of L, x being Element of L
holds x "/\" sup X = sup ({x} "/\" X)
proof
let L be up-complete LATTICE such that
A1: for X being Subset of L, x being Element of L holds
x "/\" sup X = sup ({x} "/\" finsups X);
let X be non empty directed Subset of L,
x be Element of L;
A2: {x} "/\" finsups X = {x "/\" y where y is Element of L : y in finsups X}
by YELLOW_4:42;
reconsider T = {x} as non empty directed Subset of L by WAYBEL_0:5;
A3: ex_sup_of T "/\" X,L by WAYBEL_0:75;
A4: ex_sup_of T "/\" finsups X,L by WAYBEL_0:75;
{x} "/\" finsups X is_<=_than sup ({x} "/\" X)
proof
let q be Element of L;
assume q in {x} "/\" finsups X;
then consider y being Element of L such that
A5: q = x "/\" y & y in finsups X by A2;
finsups X = {"\/"(Y,L) where Y is finite Subset of X: ex_sup_of Y,L}
by WAYBEL_0:def 27;
then consider Y being finite Subset of X such that
A6: y = "\/"(Y,L) & ex_sup_of Y,L by A5;
consider z being Element of L such that
A7: z in X & z is_>=_than Y by WAYBEL_0:1;
A8: "\/"(Y,L) <= z by A6,A7,YELLOW_0:30;
x in {x} by TARSKI:def 1;
then x "/\" z in {x} "/\" X by A7,YELLOW_4:37;
then A9: x "/\" z <= sup ({x} "/\" X) by A3,YELLOW_4:1;
x <= x;
then x "/\" y <= x "/\" z by A6,A8,YELLOW_3:2;
hence q <= sup ({x} "/\" X) by A5,A9,YELLOW_0:def 2;
end;
then sup ({x} "/\" finsups X) <= sup ({x} "/\" X) by A4,YELLOW_0:30;
then A10: x "/\" sup X <= sup ({x} "/\" X) by A1;
ex_sup_of X,L by WAYBEL_0:75;
then sup ({x} "/\" X) <= x "/\" sup X by A3,YELLOW_4:53;
hence x "/\" sup X = sup ({x} "/\" X) by A10,ORDERS_1:25;
end;
begin :: On the inf and sup operation
definition let L be non empty RelStr;
func inf_op L -> map of [:L,L:], L means :Def4:
for x, y being Element of L holds it.[x,y] = x "/\" y;
existence
proof
deffunc F(Element of L, Element of L) = $1 "/\" $2;
A1: for x, y being Element of L holds F(x,y) is Element of L;
consider f being map of [:L,L:], L such that
A2: for x, y being Element of L holds f.[x,y] = F(x,y) from Kappa2DS(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f, g be map of [:L,L:], L such that
A3: for x, y being Element of L holds f.[x,y] = x "/\" y and
A4: for x, y being Element of L holds g.[x,y] = x "/\" y;
now
let x, y be Element of L;
thus f.[x,y] = x "/\" y by A3
.= g.[x,y] by A4;
end;
hence f = g by YELLOW_3:13;
end;
end;
theorem Th31:
for L being non empty RelStr, x being Element of [:L,L:] holds
(inf_op L).x = x`1 "/\" x`2
proof
let L be non empty RelStr,
x be Element of [:L,L:];
the carrier of [:L,L:] = [:the carrier of L, the carrier of L:]
by YELLOW_3:def 2;
then consider a, b being set such that
A1: a in the carrier of L & b in the carrier of L & x = [a,b]
by ZFMISC_1:def 2;
thus (inf_op L).x = (inf_op L).[x`1,x`2] by A1,MCART_1:8
.= x`1 "/\" x`2 by Def4;
end;
definition let L be with_infima transitive antisymmetric RelStr;
cluster inf_op L -> monotone;
coherence
proof
set f = inf_op L;
let x, y be Element of [:L,L:];
assume x <= y;
then A1: x`1 <= y`1 & x`2 <= y`2 by YELLOW_3:12;
let a, b be Element of L such that
A2: a = f.x & b = f.y;
f.x = x`1 "/\" x`2 & f.y = y`1 "/\" y`2 by Th31;
hence a <= b by A1,A2,YELLOW_3:2;
end;
end;
theorem Th32:
for S being non empty RelStr, D1, D2 being Subset of S holds
(inf_op S).:[:D1,D2:] = D1 "/\" D2
proof
let S be non empty RelStr,
D1, D2 be Subset of S;
set f = inf_op S;
thus f.:[:D1,D2:] c= D1 "/\" D2
proof
let q be set; assume
A1: q in f.:[:D1,D2:];
then reconsider q1 = q as Element of S;
consider c being Element of [:S,S:] such that
A2: c in [:D1,D2:] & q1 = f.c by A1,FUNCT_2:116;
consider x, y being set such that
A3: x in D1 & y in D2 & c = [x,y] by A2,ZFMISC_1:def 2;
reconsider x, y as Element of S by A3;
q = x "/\" y by A2,A3,Def4;
then q in { a "/\" b where a, b is Element of S : a in D1 & b in D2 }
by A3;
hence q in D1 "/\" D2 by YELLOW_4:def 4;
end;
reconsider X = [:D1,D2:] as set;
let q be set;
assume q in D1 "/\" D2;
then q in { x "/\" y where x, y is Element of S : x in D1 & y in D2 }
by YELLOW_4:def 4;
then consider x, y being Element of S such that
A4: q = x "/\" y & x in D1 & y in D2;
A5: q = f.[x,y] by A4,Def4;
[x,y] in X by A4,ZFMISC_1:106;
hence thesis by A5,FUNCT_2:43;
end;
theorem Th33:
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds
sup ((inf_op L).:D) = sup (proj1 D "/\" proj2 D)
proof
let L be up-complete Semilattice,
D be non empty directed Subset of [:L,L:];
reconsider C = the carrier of L as non empty set;
D c= the carrier of [:L,L:]; then
D c= [:the carrier of L,the carrier of L:] by YELLOW_3:def 2; then
reconsider D' = D as non empty Subset of [:C,C:];
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L
by YELLOW_3:21,22;
set f = inf_op L;
A1: D' c= [:D1,D2:] by YELLOW_3:1;
A2: f.:D is directed by YELLOW_2:17;
then A3: ex_sup_of f.:D,L by WAYBEL_0:75;
A4: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75;
downarrow (f.:D) is directed by A2,WAYBEL_0:30;
then A5: ex_sup_of downarrow (f.:D),L by WAYBEL_0:75;
[:D1,D2:] c= downarrow D by YELLOW_3:48;
then A6: f.:[:D1,D2:] c= f.:(downarrow D) by RELAT_1:156;
A7: f.:(downarrow D) c= downarrow (f.:D) by Th13;
f.:D' c= f.:[:D1,D2:] by A1,RELAT_1:156;
then f.:D' c= D1 "/\" D2 by Th32;
then A8: sup (f.:D) <= sup (D1 "/\" D2) by A3,A4,YELLOW_0:34;
A9: f.:[:D1,D2:] c= downarrow (f.:D) by A6,A7,XBOOLE_1:1;
f.:[:D1,D2:] = D1 "/\" D2 by Th32;
then sup (D1 "/\" D2) <= sup (downarrow (f.:
D)) by A4,A5,A9,YELLOW_0:34;
then sup (D1 "/\" D2) <= sup(f.:D) by A3,WAYBEL_0:33;
hence thesis by A8,ORDERS_1:25;
end;
definition let L be non empty RelStr;
func sup_op L -> map of [:L,L:], L means :Def5:
for x, y being Element of L holds it.[x,y] = x "\/" y;
existence
proof
deffunc F(Element of L, Element of L) = $1 "\/" $2;
A1: for x, y being Element of L holds F(x,y) is Element of L;
consider f being map of [:L,L:], L such that
A2: for x, y being Element of L holds f.[x,y] = F(x,y) from Kappa2DS(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f, g be map of [:L,L:], L such that
A3: for x, y being Element of L holds f.[x,y] = x "\/" y and
A4: for x, y being Element of L holds g.[x,y] = x "\/" y;
now
let x, y be Element of L;
thus f.[x,y] = x "\/" y by A3
.= g.[x,y] by A4;
end;
hence f = g by YELLOW_3:13;
end;
end;
theorem Th34:
for L being non empty RelStr, x being Element of [:L,L:] holds
(sup_op L).x = x`1 "\/" x`2
proof
let L be non empty RelStr,
x be Element of [:L,L:];
the carrier of [:L,L:] = [:the carrier of L, the carrier of L:]
by YELLOW_3:def 2;
then consider a, b being set such that
A1: a in the carrier of L & b in the carrier of L & x = [a,b]
by ZFMISC_1:def 2;
thus (sup_op L).x = (sup_op L).[x`1,x`2] by A1,MCART_1:8
.= x`1 "\/" x`2 by Def5;
end;
definition let L be with_suprema transitive antisymmetric RelStr;
cluster sup_op L -> monotone;
coherence
proof
set f = sup_op L;
let x, y be Element of [:L,L:];
assume x <= y;
then A1: x`1 <= y`1 & x`2 <= y`2 by YELLOW_3:12;
let a, b be Element of L such that
A2: a = f.x & b = f.y;
f.x = x`1 "\/" x`2 & f.y = y`1 "\/" y`2 by Th34;
hence a <= b by A1,A2,YELLOW_3:3;
end;
end;
theorem Th35:
for S being non empty RelStr, D1, D2 being Subset of S holds
(sup_op S).:[:D1,D2:] = D1 "\/" D2
proof
let S be non empty RelStr,
D1, D2 be Subset of S;
set f = sup_op S;
thus f.:[:D1,D2:] c= D1 "\/" D2
proof
let q be set; assume
A1: q in f.:[:D1,D2:];
then reconsider q1 = q as Element of S;
consider c being Element of [:S,S:] such that
A2: c in [:D1,D2:] & q1 = f.c by A1,FUNCT_2:116;
consider x, y being set such that
A3: x in D1 & y in D2 & c = [x,y] by A2,ZFMISC_1:def 2;
reconsider x, y as Element of S by A3;
q = x "\/" y by A2,A3,Def5;
then q in { a "\/" b where a, b is Element of S : a in D1 & b in D2 }
by A3;
hence q in D1 "\/" D2 by YELLOW_4:def 3;
end;
reconsider X = [:D1,D2:] as set;
let q be set;
assume q in D1 "\/" D2;
then q in { x "\/" y where x, y is Element of S : x in D1 & y in D2 }
by YELLOW_4:def 3;
then consider x, y being Element of S such that
A4: q = x "\/" y & x in D1 & y in D2;
A5: q = f.[x,y] by A4,Def5;
[x,y] in X by A4,ZFMISC_1:106;
hence thesis by A5,FUNCT_2:43;
end;
theorem
for L being complete (non empty Poset)
for D being non empty filtered Subset of [:L,L:] holds
inf ((sup_op L).:D) = inf (proj1 D "\/" proj2 D)
proof
let L be complete (non empty Poset),
D be non empty filtered Subset of [:L,L:];
reconsider C = the carrier of L as non empty set;
D c= the carrier of [:L,L:]; then
D c= [:the carrier of L,the carrier of L:] by YELLOW_3:def 2; then
reconsider D' = D as non empty Subset of [:C,C:];
set D1 = proj1 D,
D2 = proj2 D,
f = sup_op L;
A1: D' c= [:D1,D2:] by YELLOW_3:1;
A2: ex_inf_of f.:D',L by YELLOW_0:17;
A3: ex_inf_of D1 "\/" D2,L by YELLOW_0:17;
A4: ex_inf_of uparrow (f.:D),L by YELLOW_0:17;
[:D1,D2:] c= uparrow D by YELLOW_3:49;
then A5: f.:[:D1,D2:] c= f.:(uparrow D) by RELAT_1:156;
A6: f.:(uparrow D) c= uparrow (f.:D) by Th14;
f.:D' c= f.:[:D1,D2:] by A1,RELAT_1:156;
then f.:D' c= D1 "\/" D2 by Th35;
then A7: inf (f.:D) >= inf (D1 "\/" D2) by A2,A3,YELLOW_0:35;
A8: f.:[:D1,D2:] c= uparrow (f.:D) by A5,A6,XBOOLE_1:1;
f.:[:D1,D2:] = D1 "\/" D2 by Th35;
then inf (D1 "\/" D2) >= inf (uparrow (f.:D)) by A3,A4,A8,YELLOW_0:35;
then inf (D1 "\/" D2) >= inf(f.:D) by A2,WAYBEL_0:38;
hence thesis by A7,ORDERS_1:25;
end;
begin :: Meet-continuous lattices
:: Def 4.1, s.30
definition let R be non empty reflexive RelStr;
attr R is satisfying_MC means :Def6:
for x being Element of R, D being non empty directed Subset of R holds
x "/\" sup D = sup ({x} "/\" D);
end;
definition let R be non empty reflexive RelStr;
attr R is meet-continuous means :Def7:
R is up-complete satisfying_MC;
end;
definition
cluster trivial -> satisfying_MC (non empty reflexive RelStr);
coherence
proof
let IT be non empty reflexive RelStr;
assume IT is trivial;
then reconsider I = IT as trivial (non empty reflexive RelStr);
let x be Element of IT,
D be non empty directed Subset of IT;
consider a being Element of I such that
A1: the carrier of I = {a} by TEX_1:def 1;
thus x "/\" sup D = sup ({x} "/\" D) by A1,REALSET1:def 20;
end;
end;
definition
cluster meet-continuous ->
up-complete satisfying_MC (non empty reflexive RelStr);
coherence by Def7;
cluster up-complete satisfying_MC ->
meet-continuous (non empty reflexive RelStr);
coherence by Def7;
end;
definition
cluster strict non empty trivial LATTICE;
existence
proof
consider B being strict trivial non empty reflexive RelStr;
take B;
thus thesis;
end;
end;
theorem Th37:
for S being non empty reflexive RelStr st
for X being Subset of S, x being Element of S holds
x "/\" sup X = "\/"({x"/\"y where y is Element of S: y in X},S) holds
S is satisfying_MC
proof
let S be non empty reflexive RelStr such that
A1: for X being Subset of S, x being Element of S holds
x "/\" sup X = "\/"({x"/\"y where y is Element of S: y in X},S);
let y be Element of S,
D be non empty directed Subset of S;
thus sup ({y} "/\" D) = "\/"({y"/\"z where z is Element of S: z in D},S)
by YELLOW_4:42
.= y "/\" sup D by A1;
end;
:: Th 4.2, s.30, 1 => 2
theorem Th38:
for L being up-complete Semilattice st SupMap L is meet-preserving holds
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
proof
let L be up-complete Semilattice such that
A1: SupMap L is meet-preserving;
let I1, I2 be Ideal of L;
reconsider x = I1, y = I2 as Element of InclPoset(Ids L) by YELLOW_2:43;
set f = SupMap L;
A2: f preserves_inf_of {x,y} by A1,WAYBEL_0:def 34;
reconsider fx = f.x as Element of L;
thus (sup I1) "/\" (sup I2)
= fx "/\" (sup I2) by YELLOW_2:def 3
.= f.x "/\" f.y by YELLOW_2:def 3
.= f.(x "/\" y) by A2,YELLOW_3:8
.= f.(I1 "/\" I2) by YELLOW_4:58
.= sup (I1 "/\" I2) by YELLOW_2:def 3;
end;
definition let L be up-complete sup-Semilattice;
cluster SupMap L -> join-preserving;
coherence
proof
set f = SupMap L;
A1: dom f = the carrier of InclPoset(Ids L) by FUNCT_2:def 1;
let x, y be Element of InclPoset(Ids L);
assume ex_sup_of {x,y},InclPoset(Ids L);
f.:{x,y} = {f.x,f.y} by A1,FUNCT_1:118;
hence ex_sup_of f.:{x,y},L by YELLOW_0:20;
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:43;
A2: ex_sup_of x1 "\/" y1,L by WAYBEL_0:75;
thus sup (f.:{x,y}) = sup {f.x,f.y} by A1,FUNCT_1:118
.= f.x "\/" f.y by YELLOW_0:41
.= f.x "\/" sup y1 by YELLOW_2:def 3
.= sup x1 "\/" sup y1 by YELLOW_2:def 3
.= sup (x1 "\/" y1) by Th4
.= sup downarrow (x1 "\/" y1) by A2,WAYBEL_0:33
.= f.(downarrow (x1 "\/" y1)) by YELLOW_2:def 3
.= f.(x "\/" y) by YELLOW_4:30
.= f.sup {x,y} by YELLOW_0:41;
end;
end;
:: Th 4.2, s.30, 2 => 1
theorem Th39:
for L being up-complete Semilattice st
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\"
I2) holds
SupMap L is meet-preserving
proof
let L be up-complete Semilattice such that
A1: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\"
I2);
set f = SupMap L;
A2: dom f = the carrier of InclPoset(Ids L) by FUNCT_2:def 1;
let x, y be Element of InclPoset(Ids L);
assume ex_inf_of {x,y},InclPoset(Ids L);
f.:{x,y} = {f.x,f.y} by A2,FUNCT_1:118;
hence ex_inf_of f.:{x,y},L by YELLOW_0:21;
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:43;
thus inf (f.:{x,y}) = inf {f.x,f.y} by A2,FUNCT_1:118
.= f.x "/\" f.y by YELLOW_0:40
.= f.x "/\" (sup y1) by YELLOW_2:def 3
.= (sup x1) "/\" (sup y1) by YELLOW_2:def 3
.= sup (x1 "/\" y1) by A1
.= f.(x1 "/\" y1) by YELLOW_2:def 3
.= f.(x "/\" y) by YELLOW_4:58
.= f.inf {x,y} by YELLOW_0:40;
end;
:: Th 4.2, s.30, 2 => 3
theorem Th40:
for L being up-complete Semilattice st
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\"
I2) holds
for D1, D2 be directed non empty Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proof
let L be up-complete Semilattice such that
A1: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\"
I2);
let D1, D2 be directed non empty Subset of L;
A2: ex_sup_of D1,L & ex_sup_of downarrow D1,L by WAYBEL_0:75;
A3: ex_sup_of D2,L & ex_sup_of downarrow D2,L by WAYBEL_0:75;
A4: ex_sup_of D1 "/\" D2,L & ex_sup_of downarrow (D1 "/\" D2),L by WAYBEL_0:75;
A5: ex_sup_of (downarrow D1 "/\" downarrow D2),L &
ex_sup_of downarrow (downarrow D1 "/\" downarrow D2),L by WAYBEL_0:75;
thus (sup D1) "/\" (sup D2)
= (sup downarrow D1) "/\" (sup D2) by A2,WAYBEL_0:33
.= (sup downarrow D1) "/\" (sup downarrow D2) by A3,WAYBEL_0:33
.= sup (downarrow D1 "/\" downarrow D2) by A1
.= sup downarrow ((downarrow D1) "/\" (downarrow D2)) by A5,WAYBEL_0:33
.= sup downarrow (D1 "/\" D2) by YELLOW_4:62
.= sup (D1 "/\" D2) by A4,WAYBEL_0:33;
end;
:: Th 4.2, s.30, 4 => 7
theorem Th41:
for L being non empty reflexive RelStr st L is satisfying_MC holds
for x being Element of L, N being non empty prenet of L st
N is eventually-directed holds
x "/\" sup N = sup ({x} "/\" rng netmap (N,L))
proof
let L be non empty reflexive RelStr such that
A1: L is satisfying_MC;
let x be Element of L,
N be non empty prenet of L;
assume N is eventually-directed;
then A2: rng netmap (N,L) is directed by Th18;
thus x "/\" sup N
= x "/\" Sup the mapping of N by Def1
.= x "/\" Sup netmap (N,L) by WAYBEL_0:def 7
.= x "/\" sup rng netmap (N,L) by YELLOW_2:def 5
.= sup ({x} "/\" rng netmap (N,L)) by A1,A2,Def6;
end;
:: Th 4.2, s.30, 7 => 4
theorem Th42:
for L being non empty reflexive RelStr st
for x being Element of L, N being prenet of L st N is eventually-directed
holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) holds
L is satisfying_MC
proof
let L be non empty reflexive RelStr such that
A1: for x being Element of L, N being prenet of L st N is eventually-directed
holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L));
let x be Element of L,
D be non empty directed Subset of L;
reconsider n = id D as Function of D, the carrier of L by FUNCT_2:9;
reconsider N = NetStr (#D,(the InternalRel of L)|_2 D,n#) as prenet of L
by Th19;
D c= D;
then A2: D = n.:D by BORSUK_1:3
.= rng n by FUNCT_2:45
.= rng netmap (N,L) by WAYBEL_0:def 7;
A3: N is eventually-directed by Th20;
A4: Sup netmap (N,L) = Sup the mapping of N by WAYBEL_0:def 7
.= sup N by Def1;
thus x "/\" sup D = x "/\" Sup netmap (N,L) by A2,YELLOW_2:def 5
.= sup ({x} "/\" D) by A1,A2,A3,A4;
end;
:: Th 4.2, s.30, 6 => 3
theorem Th43:
for L being up-complete antisymmetric (non empty reflexive RelStr) st
inf_op L is directed-sups-preserving holds
for D1, D2 being non empty directed Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proof
let L be up-complete antisymmetric (non empty reflexive RelStr) such that
A1: inf_op L is directed-sups-preserving;
let D1, D2 be non empty directed Subset of L;
set X = [:D1,D2:],
f = inf_op L;
A2: f preserves_sup_of X by A1,WAYBEL_0:def 37;
A3: ex_sup_of X,[:L,L:] by WAYBEL_0:75;
A4: ex_sup_of D1,L & ex_sup_of D2,L by WAYBEL_0:75;
thus (sup D1) "/\" (sup D2)
= f.[sup D1,sup D2] by Def4
.= f.(sup X) by A4,YELLOW_3:43
.= sup (f.:X) by A2,A3,WAYBEL_0:def 31
.= sup (D1 "/\" D2) by Th32;
end;
:: Th 4.2, s.30, 3 => 4
theorem Th44:
for L being non empty reflexive antisymmetric RelStr st
for D1, D2 being non empty directed Subset of L
holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
holds L is satisfying_MC
proof
let L be non empty reflexive antisymmetric RelStr such that
A1: for D1, D2 being non empty directed Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2);
let x be Element of L,
D be non empty directed Subset of L;
A2: {x} is directed by WAYBEL_0:5;
thus x "/\" sup D = sup {x} "/\" sup D by YELLOW_0:39
.= sup ({x} "/\" D) by A1,A2;
end;
:: Th 4.2, s.30, MC => 5
theorem Th45:
for L being satisfying_MC with_infima antisymmetric
(non empty reflexive RelStr) holds
for x being Element of L, D being non empty directed Subset of L
st x <= sup D holds x = sup ({x} "/\" D)
proof
let L be satisfying_MC with_infima antisymmetric
(non empty reflexive RelStr);
let x be Element of L,
D be non empty directed Subset of L;
assume x <= sup D;
hence x = x "/\" sup D by YELLOW_0:25
.= sup ({x} "/\" D) by Def6;
end;
:: Th 4.2, s.30, 5 => 6
theorem Th46:
for L being up-complete Semilattice st
for x being Element of L, E being non empty directed Subset of L
st x <= sup E holds x <= sup ({x} "/\" E) holds
inf_op L is directed-sups-preserving
proof
let L be up-complete Semilattice such that
A1: for x being Element of L, E being non empty directed Subset of L
st x <= sup E holds x <= sup ({x} "/\" E);
let D be Subset of [:L,L:];
assume D is non empty directed;
then reconsider DD = D as non empty directed Subset of [:L,L:];
thus inf_op L preserves_sup_of D
proof
set f = inf_op L;
assume ex_sup_of D,[:L,L:];
f.:DD is directed by YELLOW_2:17;
hence ex_sup_of f.:D,L by WAYBEL_0:75;
reconsider C = the carrier of L as non empty set;
reconsider D1 = proj1 DD, D2 = proj2 DD as
non empty directed Subset of L by YELLOW_3:21,22;
set d2 = sup D2;
{x "/\" y where x, y is Element of L : x in D1 & y in {d2}} c= C
proof
let q be set;
assume q in {x "/\"
y where x, y is Element of L : x in D1 & y in {d2}};
then consider x, y being Element of L such that
A2: q = x "/\" y & x in D1 & y in {d2};
thus q in C by A2;
end;
then reconsider F = {x "/\"
y where x, y is Element of L : x in D1 & y in {d2}}
as Subset of L;
A3: F = { sup ({z} "/\" D2) where z is Element of L : z in D1 }
proof
thus F c= { sup ({z} "/\" D2) where z is Element of L : z in D1 }
proof
let q be set;
assume q in F;
then consider x, y being Element of L such that
A4: q = x "/\" y & x in D1 & y in {d2};
q = x "/\" d2 by A4,TARSKI:def 1
.= sup ({x} "/\" D2) by A1,Th28;
hence q in { sup ({z} "/\" D2) where z is Element of L : z in
D1 } by A4;
end;
let q be set;
assume q in { sup ({z} "/\" D2) where z is Element of L : z in
D1 };
then consider z being Element of L such that
A5: q = sup ({z} "/\" D2) & z in D1;
A6: q = z "/\" d2 by A1,A5,Th28;
d2 in {d2} by TARSKI:def 1;
hence q in F by A5,A6;
end;
defpred P[set] means ex x being Element of L st $1 = {x} "/\" D2 & x in D1;
A7: "\/" ({ sup X where X is non empty directed Subset of L: P[X] },L)
= "\/" (union {X where X is non empty directed Subset of L: P[X]},L)
by Th10;
thus sup (f.:D)
= sup (D1 "/\" D2) by Th33
.= "\/" ({ "\/"
(X,L) where X is non empty directed Subset of L: P[X] },L)
by A7,Th6
.= "\/" ({ sup ({x} "/\" D2) where x is Element of L : x in D1 },L)
by Th5
.= sup ({d2} "/\" D1) by A3,YELLOW_4:def 4
.= sup D1 "/\" d2 by A1,Th28
.= f.[sup D1,sup D2] by Def4
.= f.sup D by Th12;
end;
end;
:: Th 4.2, s.30, 7 => 8
theorem Th47:
for L being complete antisymmetric (non empty reflexive RelStr) st
for x being Element of L, N being prenet of L st N is eventually-directed
holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) holds
for x being Element of L, J being set, f being Function of J,the carrier of L
holds x "/\" Sup f = sup(x "/\" FinSups f)
proof
let L be complete antisymmetric (non empty reflexive RelStr) such that
A1: for x being Element of L, N being prenet of L st N is eventually-directed
holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L));
let x be Element of L,
J be set,
f be Function of J,the carrier of L;
set F = FinSups f;
A2: ex_sup_of rng f,L by YELLOW_0:17;
A3: ex_sup_of rng netmap (FinSups f,L),L by YELLOW_0:17;
A4: for x being Element of Fin J holds ex_sup_of f.:x,L by YELLOW_0:17;
consider g being Function of Fin J, the carrier of L such that
A5: for x being Element of Fin J holds g.x = sup (f.:x) &
F = NetStr (# Fin J, RelIncl Fin J, g #) by Def2;
A6: g = netmap (F,L) by A5,WAYBEL_0:def 7;
A7: Sup netmap (F,L) = Sup the mapping of F by WAYBEL_0:def 7
.= sup F by Def1;
thus x "/\" Sup f
= x "/\" sup F by A2,A3,A4,Th26
.= x "/\" Sup the mapping of F by Def1
.= x "/\" Sup netmap (F,L) by WAYBEL_0:def 7
.= sup ({x} "/\" rng netmap (F,L)) by A1,A7
.= "\/" (rng the mapping of x "/\" F,L) by A5,A6,Th23
.= Sup (the mapping of x "/\" F) by YELLOW_2:def 5
.= sup (x "/\" F) by Def1;
end;
:: Th 4.2, s.30, 8 => 7
theorem Th48:
for L being complete Semilattice st
for x being Element of L, J being set, f being Function of J,the carrier of L
holds x "/\" Sup f = sup (x "/\" FinSups f) holds
for x being Element of L, N being prenet of L st N is eventually-directed
holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L))
proof
let L be complete Semilattice such that
A1: for x being Element of L, J being set
for f being Function of J,the carrier of L
holds x "/\" Sup f = sup (x "/\" FinSups f);
let x be Element of L,
N be prenet of L such that
A2: N is eventually-directed;
A3: Sup netmap (N,L) = Sup the mapping of N by WAYBEL_0:def 7
.= sup N by Def1;
set f = the mapping of N;
reconsider R = rng netmap (N,L) as non empty directed Subset of L
by A2,Th18;
A4: ex_sup_of R,L by WAYBEL_0:75;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
A5: ex_sup_of xx "/\" R ,L by WAYBEL_0:75;
Sup netmap (N,L) = "\/"(rng netmap(N,L),L) by YELLOW_2:def 5;
then A6: sup ({x} "/\" rng netmap (N,L)) <= x "/\" Sup netmap (N,L)
by A4,A5,YELLOW_4:53;
Sup (the mapping of x "/\" FinSups f) =
"\/"(rng the mapping of x "/\" FinSups f,L) by YELLOW_2:def 5;
then A7: sup (x "/\" FinSups f) = "\/"(rng the mapping of x "/\"
FinSups f,L) by Def1;
set h = the mapping of FinSups f;
x "/\" FinSups f is eventually-directed by Th27;
then rng netmap(x "/\" FinSups f,L) is directed by Th18;
then rng the mapping of x "/\" FinSups f is directed by WAYBEL_0:def 7;
then A8: ex_sup_of rng the mapping of x "/\" FinSups f,L by WAYBEL_0:75;
rng the mapping of x "/\" FinSups f is_<=_than sup ({x} "/\"
rng netmap (N,L))
proof
let a be Element of L;
assume a in rng the mapping of x "/\" FinSups f;
then A9: a in {x} "/\" rng h by Th23;
{x} "/\" rng h = {x "/\" y where y is Element of L: y in rng h}
by YELLOW_4:42;
then consider y being Element of L such that
A10: a = x "/\" y & y in rng h by A9;
A11: finsups rng f = {"\/"(Y,L) where Y is finite Subset of rng f:
ex_sup_of Y,L} by WAYBEL_0:def 27;
A12: for x being set holds ex_sup_of f.:x,L by YELLOW_0:17;
A13: y in rng netmap(FinSups f,L) by A10,WAYBEL_0:def 7;
rng netmap(FinSups f,L) c= finsups rng f by A12,Th24;
then y in finsups rng f by A13;
then consider Y being finite Subset of rng f such that
A14: y = "\/"(Y,L) & ex_sup_of Y,L by A11;
rng netmap (N,L) is directed by A2,Th18;
then rng f is directed by WAYBEL_0:def 7;
then consider z being Element of L such that
A15: z in rng f & z is_>=_than Y by WAYBEL_0:1;
A16: "\/"(Y,L) <= z by A14,A15,YELLOW_0:30;
A17: netmap(N,L) = f by WAYBEL_0:def 7;
x in {x} by TARSKI:def 1;
then x "/\" z in {x} "/\" rng f by A15,YELLOW_4:37;
then A18: x "/\" z <= sup (xx "/\" rng f) by A5,A17,YELLOW_4:1;
x <= x;
then x "/\" y <= x "/\" z by A14,A16,YELLOW_3:2;
then a <= sup ({x} "/\" rng f) by A10,A18,YELLOW_0:def 2;
hence a <= sup ({x} "/\" rng netmap (N,L)) by WAYBEL_0:def 7;
end;
then A19: "\/"(rng the mapping of x "/\" FinSups f,L) <= sup ({x} "/\"
rng netmap (N,L))
by A8,YELLOW_0:def 9;
x "/\" Sup f = sup(x "/\" FinSups f) by A1;
then x "/\" Sup netmap (N,L) <= sup ({x} "/\" rng netmap (N,L)) by A7,A19,
WAYBEL_0:def 7;
hence x "/\" sup N = sup ({x} "/\" rng netmap (N,L))
by A3,A6,ORDERS_1:25;
end;
:: Th 4.2, s.30, 4 <=> 1
theorem Th49:
for L being up-complete LATTICE
holds L is meet-continuous iff
SupMap L is meet-preserving join-preserving
proof
let L be up-complete LATTICE;
hereby
assume L is meet-continuous;
then A1: L is satisfying_MC by Def7;
for D1, D2 being non empty directed Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proof
let D1, D2 be non empty directed Subset of L;
for x being Element of L, E being non empty directed Subset of L
st x <= sup E holds x <= sup ({x} "/\" E) by A1,Th45;
then inf_op L is directed-sups-preserving by Th46;
hence (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43;
end;
then for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1
"/\"
I2);
hence SupMap L is meet-preserving join-preserving by Th39;
end;
assume
A2: SupMap L is meet-preserving join-preserving;
thus L is up-complete;
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\"
I2
)
by A2,Th38;
then for D1, D2 be non empty directed Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40;
hence L is satisfying_MC by Th44;
end;
definition let L be meet-continuous LATTICE;
cluster SupMap L -> meet-preserving join-preserving;
coherence by Th49;
end;
:: Th 4.2, s.30, 4 <=> 2
theorem Th50:
for L being up-complete LATTICE
holds L is meet-continuous iff
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
proof
let L be up-complete LATTICE;
hereby assume L is meet-continuous;
then SupMap L is meet-preserving join-preserving by Th49;
hence for I1, I2 being Ideal of L
holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by Th38;
end;
assume for I1, I2 being Ideal of L
holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2);
then for D1, D2 be directed non empty Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40;
hence L is up-complete & L is satisfying_MC by Th44;
end;
:: Th 4.2, s.30, 4 <=> 3
theorem Th51:
for L being up-complete LATTICE holds
L is meet-continuous iff
for D1, D2 being non empty directed Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proof
let L be up-complete LATTICE;
hereby
assume L is meet-continuous;
then for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1
"/\"
I2)
by Th50;
hence for D1, D2 be directed non empty Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40;
end;
assume for D1, D2 being non empty directed Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2);
hence L is up-complete & L is satisfying_MC by Th44;
end;
:: Th 4.2, s.30, 4 <=> 5
theorem
for L being up-complete LATTICE holds
L is meet-continuous iff
for x being Element of L, D being non empty directed Subset of L
st x <= sup D holds x = sup ({x} "/\" D)
proof
let L be up-complete LATTICE;
hereby
assume L is meet-continuous;
then L is satisfying_MC by Def7;
hence for x being Element of L, D being non empty directed Subset of L
st x <= sup D holds x = sup ({x} "/\" D) by Th45;
end;
assume for x being Element of L, D being non empty directed Subset of L
st x <= sup D holds x = sup ({x} "/\" D);
then for x being Element of L, D being non empty directed Subset of L
st x <= sup D holds x <= sup ({x} "/\" D);
then inf_op L is directed-sups-preserving by Th46;
then for D1, D2 being non empty directed Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43;
hence thesis by Th51;
end;
:: Th 4.2, s.30, 4 <=> 6
theorem Th53:
for L being up-complete Semilattice holds
L is meet-continuous iff inf_op L is directed-sups-preserving
proof
let L be up-complete Semilattice;
hereby
assume L is meet-continuous;
then L is satisfying_MC by Def7;
then for x being Element of L, D being non empty directed Subset of L
st x <= sup D holds x <= sup ({x} "/\" D) by Th45;
hence inf_op L is directed-sups-preserving by Th46;
end;
assume inf_op L is directed-sups-preserving;
then for D1, D2 being non empty directed Subset of L holds
(sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43;
hence L is up-complete & L is satisfying_MC by Th44;
end;
definition let L be meet-continuous Semilattice;
cluster inf_op L -> directed-sups-preserving;
coherence by Th53;
end;
:: Th 4.2, s.30, 4 <=> 7
theorem Th54:
for L being up-complete Semilattice holds
L is meet-continuous iff
for x being Element of L, N being non empty prenet of L st
N is eventually-directed holds
x "/\" sup N = sup ({x} "/\" rng netmap (N,L))
proof
let L be up-complete Semilattice;
hereby
assume L is meet-continuous;
then L is satisfying_MC by Def7;
hence for x being Element of L, N being non empty prenet of L st
N is eventually-directed holds
x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) by Th41;
end;
assume for x being Element of L, N being non empty prenet of L st
N is eventually-directed holds
x "/\" sup N = sup ({x} "/\" rng netmap (N,L));
hence L is up-complete & L is satisfying_MC by Th42;
end;
:: Th 4.2, s.30, 4 <=> 8
theorem
for L being complete Semilattice holds
L is meet-continuous iff
for x being Element of L, J being set
for f being Function of J,the carrier of L
holds x "/\" Sup f = sup(x "/\" FinSups f)
proof
let L be complete Semilattice;
hereby
assume L is meet-continuous;
then for x being Element of L, N being non empty prenet of L st
N is eventually-directed holds
x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) by Th54;
hence for x being Element of L, J being set
for f being Function of J,the carrier of L
holds x "/\" Sup f = sup(x "/\" FinSups f) by Th47;
end;
assume for x being Element of L, J being set
for f being Function of J,the carrier of L
holds x "/\" Sup f = sup(x "/\" FinSups f);
then for x being Element of L, N being prenet of L st N is
eventually-directed
holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) by Th48;
hence L is up-complete & L is satisfying_MC by Th42;
end;
Lm1:
for L being meet-continuous Semilattice, x being Element of L
holds x "/\" is directed-sups-preserving
proof
let L be meet-continuous Semilattice,
x be Element of L;
let X be Subset of L such that
A1: X is non empty directed;
assume ex_sup_of X,L;
A2: x"/\".:X is directed by A1,YELLOW_2:17;
reconsider X1 = X as non empty Subset of L by A1;
x"/\".:X1 is non empty;
hence ex_sup_of x"/\".:X,L by A2,WAYBEL_0:75;
A3: for x being Element of L, E being non empty directed Subset of L
st x <= sup E holds x <= sup ({x} "/\" E) by Th45;
thus sup (x"/\".:X) = "\/"({x"/\"y where y is Element of L: y in X},L)
by WAYBEL_1:64
.= sup({x} "/\" X) by YELLOW_4:42
.= x "/\" sup X by A1,A3,Th28
.= x"/\".sup X by WAYBEL_1:def 18;
end;
definition let L be meet-continuous Semilattice,
x be Element of L;
cluster x "/\" -> directed-sups-preserving;
coherence by Lm1;
end;
:: Remark 4.3 s.31
theorem Th56:
for H being complete (non empty Poset) holds
H is Heyting iff H is meet-continuous distributive
proof
let H be complete (non empty Poset);
hereby assume
A1: H is Heyting;
then for x being Element of H holds x "/\" has_an_upper_adjoint
by WAYBEL_1:def 19;
then A2: for X being Subset of H, x being Element of H holds
x "/\" sup X = "\/"({x"/\"y where y is Element of H: y in
X},H) by WAYBEL_1:67;
thus H is meet-continuous
proof
thus H is up-complete satisfying_MC by A2,Th37;
end;
thus H is distributive by A1,WAYBEL_1:69;
end;
assume that
A3: H is meet-continuous distributive;
thus H is LATTICE;
let a be Element of H;
A4: for X being finite Subset of H holds a "/\" preserves_sup_of X by A3,Th17;
for X being non empty directed Subset of H holds a "/\" preserves_sup_of
X
proof
let X be non empty directed Subset of H;
a "/\" is directed-sups-preserving by A3,Lm1;
hence a "/\" preserves_sup_of X by WAYBEL_0:def 37;
end;
then a "/\" is sups-preserving by A4,WAYBEL_0:74;
hence a "/\" has_an_upper_adjoint by WAYBEL_1:18;
end;
definition
cluster complete Heyting -> meet-continuous distributive (non empty Poset);
coherence by Th56;
cluster complete meet-continuous distributive -> Heyting (non empty Poset);
coherence by Th56;
end;