:: Meet-continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received October 10, 1996
:: Copyright (c) 1996-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, RELAT_1, RELAT_2, LATTICE3,
ORDERS_2, XXREAL_0, TREES_2, WAYBEL_0, YELLOW_0, LATTICES, EQREL_1,
ORDINAL2, ZFMISC_1, TARSKI, STRUCT_0, MCART_1, SEQM_3, REWRITE1,
FINSET_1, WELLORD1, CAT_1, YELLOW_2, FINSUB_1, WELLORD2, YELLOW_1,
CARD_FIL, LATTICE2, WAYBEL_1, WAYBEL_2, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSUB_1, RELAT_1, FUNCT_1,
RELSET_1, TOLER_1, FINSET_1, PARTFUN1, BINOP_1, FUNCT_2, DOMAIN_1,
ORDERS_1, STRUCT_0, ORDERS_2, ORDERS_3, LATTICE3, YELLOW_0, WAYBEL_0,
YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4;
constructors DOMAIN_1, FINSUB_1, TOLER_1, ORDERS_3, WAYBEL_1, YELLOW_3,
YELLOW_4, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
FINSUB_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2,
WAYBEL_1, YELLOW_3, YELLOW_4, RELSET_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions WAYBEL_1, LATTICE3, ORDERS_3, TARSKI, WAYBEL_0, XBOOLE_0;
equalities YELLOW_0, WAYBEL_0, WELLORD1, BINOP_1, RELAT_1, STRUCT_0;
expansions WAYBEL_1, YELLOW_0, LATTICE3, ORDERS_3, TARSKI, WAYBEL_0;
theorems FINSUB_1, FUNCT_1, FUNCT_2, LATTICE3, MCART_1, ORDERS_2, RELAT_1,
STRUCT_0, TARSKI, WAYBEL_0, YELLOW_0, ZFMISC_1, YELLOW_1, YELLOW_2,
WAYBEL_1, YELLOW_3, YELLOW_4, XBOOLE_1, RELSET_1, XTUPLE_0;
schemes FINSET_1, YELLOW_3, FUNCT_2;
begin :: Preliminaries
registration
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
set x = the Element of Z;
A1: dom f = X by FUNCT_2:def 1;
thus thesis by A1;
end;
end;
registration
cluster reflexive connected -> with_infima with_suprema for
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;
suppose
A2: x <= y;
take z = x;
thus z <= x & z <= y by A1,A2;
thus thesis;
end;
suppose
A3: y <= x;
take z = y;
thus z <= x & z <= y by A1,A3;
thus thesis;
end;
end;
let x, y be Element of L;
per cases by A1;
suppose
A4: x <= y;
take z = y;
thus z >= x & z >= y by A1,A4;
thus thesis;
end;
suppose
A5: y <= x;
take z = x;
thus z >= x & z >= y by A1,A5;
thus thesis;
end;
end;
end;
registration
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 thesis;
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 thesis;
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;
set b = the Element of B;
let x be Element of L;
assume x in A;
then
A2: x "\/" b in A "\/" B by A1;
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
A3: x <= x "\/" b by LATTICE3:def 13;
ex_sup_of A "\/" B,L by WAYBEL_0:75;
then A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def 9;
then x "\/" b <= sup (A "\/" B) by A2;
hence x <= sup (A "\/" B) by A3,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 B,L by WAYBEL_0:75;
then
A2: B is_<=_than sup B by YELLOW_0:30;
A3: ex_sup_of A,L by WAYBEL_0:75;
then A is_<=_than sup A by YELLOW_0:30;
then ex_sup_of A "\/" B,L & A "\/" B is_<=_than sup A "\/" sup B by A2,
WAYBEL_0:75,YELLOW_4:27;
then
A4: sup (A "\/" B) <= sup A "\/" sup B by YELLOW_0:def 9;
B is_<=_than sup (A "\/" B) by Th3;
then
A5: sup B <= sup (A "\/" B) by A1,YELLOW_0:30;
A is_<=_than sup (A "\/" B) by Th3;
then sup A <= sup (A "\/" B) by A3,YELLOW_0:30;
then
A6: sup A "\/" sup B <= sup (A "\/" B) "\/" sup (A "\/" B) by A5,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 A4,A6,ORDERS_2:2;
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 object;
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 thesis by A1;
end;
let q be object;
assume q in { sup X where X is non empty directed Subset of L: P[X] };
then ex X being non empty directed Subset of L st q = sup X & P[X];
hence thesis;
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;
reconsider T = D2 as non empty directed Subset of L by YELLOW_3:21,22;
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 object;
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 and
A3: 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
A4: w = e and
A5: P[e] by A3;
consider p being Element of L such that
A6: e = {p} "/\" D2 and
A7: p in D1 by A5;
{p} "/\" D2 = { p "/\" y where y is Element of L : y in D2 } by YELLOW_4:42
;
then ex y being Element of L st q = p "/\" y & y in D2 by A2,A4,A6;
hence thesis by A1,A7;
end;
let q be object;
assume q in D1 "/\" D2;
then consider x, y being Element of L such that
A8: q = x "/\" y and
A9: x in D1 and
A10: y in D2 by A1;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
xx "/\" T is non empty directed;
then
A11: {x} "/\" D2 in {X where X is non empty directed Subset of L: P[X]} by A9;
{x} "/\" D2 = { x "/\" d where d is Element of L : d in D2 } by YELLOW_4:42;
then q in {x} "/\" D2 by A8,A10;
hence thesis by A11,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 object;
assume q in union A;
then consider r being set such that
A1: q in r and
A2: r in A by TARSKI:def 4;
ex s being non empty directed Subset of L st r = s & ex x being Element
of L st s = {x} "/\" D2 & x in D1 by A2;
hence thesis by A1;
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 object;
assume q in A;
then ex X being non empty directed Subset of L st q = sup X & P[X];
hence thesis;
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 object;
assume q in union R;
then consider r being set such that
A1: q in r and
A2: r in R by TARSKI:def 4;
ex s being non empty directed Subset of L st r = s & ex x being Element
of L st s = {x} "/\" D2 & x in D1 by A2;
hence thesis by A1;
end;
then reconsider UR = union R as Subset of L;
set a = sup UR;
A3: ex_sup_of UR,L by Th7;
A4: for b being Element of L st A is_<=_than b holds a <= b
proof
let b be Element of L such that
A5: 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
A6: k in k1 and
A7: k1 in R by TARSKI:def 4;
consider s being non empty directed Subset of L such that
A8: k1 = s and
A9: P[s] by A7;
consider x being Element of L such that
A10: s = {x} "/\" D2 and
x in D1 by A9;
A11: {x} "/\" D2 = {x "/\" d2 where d2 is Element of L: d2 in D2} by
YELLOW_4:42;
sup s in A by A9;
then
A12: sup s <= b by A5;
consider d2 being Element of L such that
A13: k = x "/\" d2 and
d2 in D2 by A6,A8,A10,A11;
x "/\" d2 <= sup s by A6,A8,A10,A13,Th1,YELLOW_4:1;
hence k <= b by A13,A12,YELLOW_0:def 2;
end;
hence thesis by A3,YELLOW_0:def 9;
end;
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
A14: b = sup X and
A15: P[X];
ex_sup_of X,L & X in R by A15,WAYBEL_0:75;
hence b <= a by A3,A14,YELLOW_0:34,ZFMISC_1:74;
end;
hence thesis by A4,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: "\/"(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 and
A3: P[q];
A4: q in {X where X is non empty directed Subset of L: P[X]} by A3;
ex_sup_of q,L & ex_sup_of union {X where X is non empty directed
Subset of L : P[X]},L by Th7,WAYBEL_0:75;
hence
a <= "\/"(union {X where X is non empty directed Subset of L: P[X]},L
) by A2,A4,YELLOW_0:34,ZFMISC_1:74;
end;
ex_sup_of { sup X where X is non empty directed Subset of L: P[X] },L by Th8;
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: 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 and
A4: 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
A5: b = c and
A6: P[c] by A4;
"\/"(c,L) in { "\/" (X,L) where X is non empty directed Subset of L:
P[X] } by A6;
then
A7: "\/"(c,L) <= "\/" ({ "\/"(X,L) where X is non empty directed Subset
of L: P[X] },L) by Th8,YELLOW_4:1;
ex_sup_of c,L by WAYBEL_0:75;
then a <= "\/"(c,L) by A3,A5,YELLOW_4:1;
hence
a <= "\/" ({ "\/"(X,L) where X is non empty directed Subset of L: P[X
] },L) by A7,YELLOW_0:def 2;
end;
ex_sup_of union {X where X is non empty directed Subset of L: P[X]},L by Th7;
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_2:2;
end;
registration
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:21;
then z`2 is_>=_than X2 by A5,YELLOW_3:31;
then
A7: y <= z`2 by A4;
z`1 is_>=_than X1 by A5,A6,YELLOW_3:31;
then x <= z`1 by A2;
hence thesis by A6,A7,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
set D = the non empty directed Subset of T;
let X be non empty directed Subset of S;
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;
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:21;
hence x`1 is_>=_than X by A2,YELLOW_3:29;
ex_sup_of [:X,D:],[:S,T:] by A1,WAYBEL_0:75;
then ex_sup_of D,T by YELLOW_3:39;
then
A5: sup D is_>=_than D by YELLOW_0:def 9;
let y be Element of S;
assume y is_>=_than X;
then x <= [y,sup D] by A3,A5,YELLOW_3:30;
hence thesis by A4,YELLOW_3:11;
end;
set D = the non empty directed Subset of S;
let X be non empty directed Subset of T;
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;
ex_sup_of [:D,X:],[:S,T:] by A1,WAYBEL_0:75;
then ex_sup_of D,S by YELLOW_3:39;
then
A8: sup D is_>=_than D by YELLOW_0:def 9;
take x`2;
the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by
YELLOW_3:def 2;
then
A9: x = [x`1,x`2] by MCART_1:21;
hence x`2 is_>=_than X by A6,YELLOW_3:29;
let y be Element of T;
assume y is_>=_than X;
then x <= [sup D,y] by A7,A8,YELLOW_3:30;
hence thesis by A9,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;
reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def 2;
A1: ex_sup_of D1,L by WAYBEL_0:75;
the carrier of [:L,L:] = [:C,C:] by YELLOW_3:def 2;
then consider d1, d2 being object such that
A2: d1 in C & d2 in C and
A3: sup D = [d1,d2] by ZFMISC_1:def 2;
A4: ex_sup_of D2,L by WAYBEL_0:75;
reconsider d1, d2 as Element of L by A2;
A5: ex_sup_of D,[:L,L:] by WAYBEL_0:75;
D2 is_<=_than d2
proof
let b be Element of L;
assume b in D2;
then consider x being object such that
A6: [x,b] in D by XTUPLE_0:def 13;
reconsider x as Element of D1 by A6,XTUPLE_0:def 12;
D is_<=_than [d1,d2] by A5,A3,YELLOW_0:def 9;
then [x,b] <= [d1,d2] by A6;
hence b <= d2 by YELLOW_3:11;
end;
then
A7: sup D2 <= d2 by A4,YELLOW_0:def 9;
D1 is_<=_than d1
proof
let b be Element of L;
assume b in D1;
then consider x being object such that
A8: [b,x] in D by XTUPLE_0:def 12;
reconsider x as Element of D2 by A8,XTUPLE_0:def 13;
D is_<=_than [d1,d2] by A5,A3,YELLOW_0:def 9;
then [b,x] <= [d1,d2] by A8;
hence b <= d1 by YELLOW_3:11;
end;
then sup D1 <= d1 by A1,YELLOW_0:def 9;
then
A9: [sup D1,sup D2] <= sup D by A3,A7,YELLOW_3:11;
A10: ex_sup_of [:D1,D2:],[:L,L:] by WAYBEL_0:75;
reconsider D1, D2 as non empty Subset of L;
D9 c= [:D1,D2:] by YELLOW_3:1;
then sup D <= sup [:D1,D2:] by A5,A10,YELLOW_0:34;
then sup D <= [sup proj1 D,sup proj2 D] by A1,A4,YELLOW_3:43;
hence thesis by A9,ORDERS_2:2;
end;
theorem Th13:
for S1, S2 being RelStr, D being Subset of S1 for f being
Function 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 Function of S1,S2 such that
A1: f is monotone;
let q be object;
assume
A2: q in f.:(downarrow D);
then consider x being object such that
A3: x in dom f and
A4: x in downarrow D and
A5: q = f.x by FUNCT_1:def 6;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A2;
reconsider x as Element of s1 by A3;
consider y being Element of s1 such that
A6: x <= y and
A7: y in D by A4,WAYBEL_0:def 15;
reconsider f1 = f as Function of s1,s2;
f1.x is Element of s2;
then reconsider q1 = q, fy = f1.y as Element of s2 by A5;
the carrier of s2 <> {};
then dom f = the carrier of s1 by FUNCT_2:def 1;
then
A8: f.y in f.:D by A7,FUNCT_1:def 6;
q1 <= fy by A1,A5,A6;
hence thesis by A8,WAYBEL_0:def 15;
end;
theorem Th14:
for S1, S2 being RelStr, D being Subset of S1 for f being
Function 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 Function of S1,S2 such that
A1: f is monotone;
let q be object;
assume
A2: q in f.:(uparrow D);
then consider x being object such that
A3: x in dom f and
A4: x in uparrow D and
A5: q = f.x by FUNCT_1:def 6;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A2;
reconsider x as Element of s1 by A3;
consider y being Element of s1 such that
A6: y <= x and
A7: y in D by A4,WAYBEL_0:def 16;
reconsider f1 = f as Function of s1,s2;
f1.x is Element of s2;
then reconsider q1 = q, fy = f1.y as Element of s2 by A5;
the carrier of s2 <> {};
then dom f = the carrier of s1 by FUNCT_2:def 1;
then
A8: f.y in f.:D by A7,FUNCT_1:def 6;
fy <= q1 by A1,A5,A6;
hence thesis by A8,WAYBEL_0:def 16;
end;
registration
cluster -> distributive complemented for 1-element reflexive RelStr;
coherence
proof
let L be 1-element reflexive RelStr;
thus L is distributive
by STRUCT_0:def 10;
let x be Element of L;
take y = x;
thus x "\/" y = Top L by STRUCT_0:def 10;
thus thesis by STRUCT_0:def 10;
end;
end;
registration
cluster strict 1-element for LATTICE;
existence
proof
set B = the strict 1-element 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: P[{}]
proof
reconsider A = {} as Subset of H by XBOOLE_1:2;
take A;
thus A = {};
Bottom H <= a & {a} "/\" {}H = {} by YELLOW_0:44,YELLOW_4:36;
hence thesis by YELLOW_0:25;
end;
A2: 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
A3: x in X and
A4: B c= X and
A5: P[B];
reconsider x1 = x as Element of H by A3;
A6: {x1} c= the carrier of H;
B c= the carrier of H by A4,XBOOLE_1:1;
then reconsider C = B \/ {x} as Subset of H by A6,XBOOLE_1:8;
take C;
thus C = B \/ {x};
consider A being Subset of H such that
A7: A = B and
A8: a "/\" sup A = sup({a} "/\" A) by A5;
A9: {a} "/\" C = ({a} "/\" A) \/ ({a} "/\" {x1}) by A7,YELLOW_4:43
.= ({a} "/\" A) \/ {a "/\" x1} by YELLOW_4:46;
A10: ex_sup_of {a} "/\" A,H & ex_sup_of {a "/\" x1},H by YELLOW_0:17;
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 A7,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 A10,A9,YELLOW_2:3;
end;
A11: X is finite;
P[X] from FINSET_1:sch 2(A11,A1,A2);
hence thesis;
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: P[{}]
proof
reconsider A = {} as Subset of H by XBOOLE_1:2;
take A;
thus A = {};
a <= Top H & {a} "\/" {}H = {} by YELLOW_0:45,YELLOW_4:9;
hence thesis by YELLOW_0:24;
end;
A2: 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
A3: x in X and
A4: B c= X and
A5: P[B];
reconsider x1 = x as Element of H by A3;
A6: {x1} c= the carrier of H;
B c= the carrier of H by A4,XBOOLE_1:1;
then reconsider C = B \/ {x} as Subset of H by A6,XBOOLE_1:8;
take C;
thus C = B \/ {x};
consider A being Subset of H such that
A7: A = B and
A8: a "\/" inf A = inf({a} "\/" A) by A5;
A9: {a} "\/" C = ({a} "\/" A) \/ ({a} "\/" {x1}) by A7,YELLOW_4:16
.= ({a} "\/" A) \/ {a "\/" x1} by YELLOW_4:19;
A10: ex_inf_of {a} "\/" A,H & ex_inf_of {a "\/" x1},H by YELLOW_0:17;
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 A7,A8,WAYBEL_1:5
.= inf({a} "\/" A) "/\" (a "\/" x1) by YELLOW_0:39
.= inf({a} "\/" A) "/\" inf{a "\/" x1} by YELLOW_0:39
.= inf({a} "\/" C) by A10,A9,YELLOW_2:4;
end;
A11: X is finite;
P[X] from FINSET_1:sch 2(A11,A1,A2);
hence thesis;
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:61
.= 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 FUNCT_2:sch 8(A1);
set M = NetStr (# the carrier of N(), the InternalRel of N(), f #);
the RelStr of M = the RelStr of N() & [#]N() is directed by WAYBEL_0:def 6;
then [#]M is directed by WAYBEL_0:3;
then reconsider M as prenet of L() by WAYBEL_0:def 6;
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 object such that
A4: a in dom f and
A5: f.a = x by A2,FUNCT_1:def 3;
consider b being object such that
A6: b in dom f and
A7: f.b = y by A3,FUNCT_1:def 3;
reconsider a, b as Element of N by A4,A6;
consider ja being Element of N such that
A8: 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
A9: for k being Element of N st jb <= k holds N.b <= N.k by A1,WAYBEL_0:11;
[#]N is directed by WAYBEL_0:def 6;
then consider c being Element of N such that
c in [#]N and
A10: ja <= c & jb <= c;
take z = f.c;
dom f = the carrier of N by FUNCT_2:def 1;
hence z in rng f by FUNCT_1:def 3;
N.c = f.c;
hence thesis by A5,A7,A8,A9,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 that
x in [#]N and
y in [#]N;
reconsider x1 = x, y1 = y as Element of D;
consider z1 being Element of L such that
A1: z1 in D and
A2: x1 <= z1 & y1 <= z1 by WAYBEL_0:def 1;
reconsider z = z1 as Element of N by A1;
take z;
thus z in [#]N;
the InternalRel of N c= the InternalRel of L by XBOOLE_1:17;
then reconsider N as SubRelStr of L by YELLOW_0:def 13;
N is full;
hence thesis by A2,YELLOW_0:60;
end;
hence thesis;
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;
the InternalRel of N c= the InternalRel of L by A2,XBOOLE_1:17;
then
A4: N is SubRelStr of L by A2,YELLOW_0:def 13;
reconsider nj = n.j, nk = n.k as Element of L by A2,FUNCT_2:5;
nj = j & nk = k by A1,A2;
hence thesis by A2,A3,A4,YELLOW_0:59;
end;
hence thesis by WAYBEL_0:11;
end;
definition
let L be non empty RelStr, N be NetStr over L;
func sup N -> Element of L equals
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 FUNCT_2:sch 8(
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 and
y in [#]M;
reconsider x1 = x, y1 = y as Element of Fin J;
reconsider z = x1 \/ y1 as Element of M;
take z;
thus z in [#]M;
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;
y c= z by XBOOLE_1:7;
then
A4: y2 <= z1 by YELLOW_1:3;
x c= z by XBOOLE_1:7;
then x2 <= z1 by YELLOW_1:3;
hence thesis by A3,A4,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
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) & A = NetStr (#Fin J, RelIncl Fin J, g
#) and
A6: 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
A7: for x being Element of Fin J holds g1.x = sup (f.:x) & A = NetStr
(#Fin J, RelIncl Fin J, g1#) by A5;
consider g2 being Function of Fin J, the carrier of L such that
A8: for x being Element of Fin J holds g2.x = sup (f.:x) & B = NetStr
(#Fin J, RelIncl Fin J, g2#) by A6;
for x being object st x in Fin J holds g1.x = g2.x
proof
let x be object;
assume
A9: x in Fin J;
reconsider xx=x as set by TARSKI:1;
thus g1.x = sup (f.:xx) by A7,A9
.= g2.x by A8,A9;
end;
hence thesis by A7,A8,FUNCT_2:12;
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;
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) & FinSups f = NetStr (# Fin J, RelIncl Fin J, g #)
by Def2;
hence thesis;
end;
registration
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;
g.x = sup (f.:x) by A2;
then reconsider fx = g.x as Element of L;
A3: 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;
A4: ex_sup_of f.:x,L & ex_sup_of f.:y,L by YELLOW_0:17;
x1 <= y1 by A1,A2,A3,YELLOW_0:1;
then x c= y by YELLOW_1:3;
then sup (f.:x) <= sup (f.:y) by A4,RELAT_1:123,YELLOW_0:34;
then
A5: fx <= sup (f.:y) by A2;
let a, b be Element of L;
assume a = netmap(FinSups f,L).x & b = netmap(FinSups f,L).y;
hence a <= b by A2,A5;
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 FUNCT_2:sch 3(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 and
A4: 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
A5: the RelStr of B = the RelStr of N and
A6: 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,A5;
for c being Element of C holds f1.c = f2.c
proof
let c be Element of C;
(ex ya being Element of L st ya = (the mapping of N).c & f1.c = x
"/\" ya )& ex yb being Element of L st yb = (the mapping of N).c & f2.c = x
"/\" yb by A3,A4,A5,A6;
hence thesis;
end;
hence thesis by A3,A5,FUNCT_2:63;
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 thesis;
end;
registration
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;
end;
end;
registration
let L be non empty RelStr, x be Element of L, N be prenet of L;
cluster x "/\" N -> directed;
coherence
proof
the RelStr of x "/\" N = the RelStr of N & [#]N is directed by Def3,
WAYBEL_0:def 6;
hence [#](x "/\" N) is directed by 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: {x} "/\" A = {x "/\" y where y is Element of L: y in A} by YELLOW_4:42;
A2: the RelStr of x "/\" F = the RelStr of F by Def3;
then
A3: dom h = the carrier of F by FUNCT_2:def 1;
A4: dom f = the carrier of F by FUNCT_2:def 1;
thus rng the mapping of x "/\" F c= {x} "/\" A
proof
let q be object;
assume q in rng h;
then consider a being object such that
A5: a in dom h and
A6: q = h.a by FUNCT_1:def 3;
reconsider a as Element of x "/\" F by A5;
consider y being Element of L such that
A7: y = f.a and
A8: h.a = x "/\" y by Def3;
y in A by A2,A4,A7,FUNCT_1:def 3;
hence thesis by A1,A6,A8;
end;
let q be object;
assume q in {x} "/\" A;
then consider y being Element of L such that
A9: q = x "/\" y and
A10: y in A by A1;
consider z being object such that
A11: z in dom f and
A12: y = f.z by A10,FUNCT_1:def 3;
reconsider z as Element of x "/\" F by A2,A11;
ex w being Element of L st w = f.z & h.z = x "/\" w by Def3;
hence thesis by A3,A9,A11,A12,FUNCT_1:def 3;
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;
let q be object;
set h = netmap(FinSups f,L);
assume q in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = q by FUNCT_1:def 3;
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) & FinSups f = NetStr (# Fin J, RelIncl Fin J, g #)
by Def2;
then reconsider x as Element of Fin J by A2;
A5: f.:x is finite Subset of rng f & ex_sup_of f.:x,L by A1,RELAT_1:111;
h.x = sup (f.:x) by A4;
hence thesis by A3,A5;
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 object;
assume a in rng f;
then consider b being object such that
A2: b in dom f and
A3: a = f.b by FUNCT_1:def 3;
reconsider b as Element of J by A2;
f.b in rng f by A2,FUNCT_1:def 3;
then reconsider fb = f.b as Element of L;
A4: Im(f,b) = {fb} by A2,FUNCT_1:59;
{b} c= J by A1,ZFMISC_1:31;
then reconsider x = {b} as Element of Fin J by FINSUB_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;
dom g = Fin J by FUNCT_2:def 1;
then
A6: x in dom g;
g.{b} = sup (f.:x) by A5
.= a by A3,A4,YELLOW_0:39;
hence thesis by A5,A6,FUNCT_1:def 3;
end;
suppose
A7: J is empty;
rng f = {} by A7;
hence thesis;
end;
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 and
A2: ex_sup_of rng netmap (FinSups f,L),L and
A3: for x being Element of Fin J holds ex_sup_of f.:x,L;
set h = netmap (FinSups f,L);
A4: "\/"(rng f,L) <= sup rng h by A1,A2,Th25,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 object such that
A5: x in dom h and
A6: a = h.x by FUNCT_1:def 3;
A7: 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) & FinSups f = NetStr (# Fin J, RelIncl Fin J, g
#) by Def2;
then reconsider x as Element of Fin J by A5;
ex_sup_of f.:x,L by A3;
then sup(f.:x) <= "\/"(rng f,L) by A1,RELAT_1:111,YELLOW_0:34;
hence a <= "\/"(rng f,L) by A6,A7;
end;
then
A8: sup rng h <= "\/"(rng f,L) by A2,YELLOW_0:def 9;
thus Sup f = "\/"(rng f,L) by YELLOW_2:def 5
.= sup rng netmap (FinSups f,L) by A4,A8,ORDERS_2:2
.= sup FinSups f by YELLOW_2:def 5;
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;
( ex yi being Element of L st yi = (the mapping of N).i1 & (the
mapping of x "/\" N).i1 = x "/\" yi)& ex yk being Element of L st yk = (the
mapping of N). k1 & (the mapping of x "/\" N).k1 = x "/\" yk by Def3;
hence thesis by A4,WAYBEL_1:1;
end;
hence thesis 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;
reconsider T = {x "/\" sup D} as non empty directed Subset of L by WAYBEL_0:5
;
ex_sup_of D,L by WAYBEL_0:75;
then
A3: sup D is_>=_than D by YELLOW_0:30;
ex_sup_of T "/\" D,L & {x "/\" sup D} "/\" D is_<=_than x "/\" sup D by
WAYBEL_0:75,YELLOW_4:52;
then sup ({x "/\" sup D} "/\" D) <= x "/\" sup D by YELLOW_0:30;
hence x "/\" sup D = sup ({x "/\" sup D} "/\" D) by A2,ORDERS_2:2
.= 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;
reconsider T = {x} as non empty directed Subset of L by WAYBEL_0:5;
A2: ex_sup_of T "/\" X,L by WAYBEL_0:75;
A3: {x} "/\" finsups X = {x "/\" y where y is Element of L : y in finsups X}
by YELLOW_4:42;
A4: {x} "/\" finsups X is_<=_than sup ({x} "/\" X)
proof
let q be Element of L;
A5: x <= x;
assume q in {x} "/\" finsups X;
then consider y being Element of L such that
A6: q = x "/\" y and
A7: y in finsups X by A3;
consider Y being finite Subset of X such that
A8: y = "\/"(Y,L) and
A9: ex_sup_of Y,L by A7;
consider z being Element of L such that
A10: z in X and
A11: z is_>=_than Y by WAYBEL_0:1;
"\/"(Y,L) <= z by A9,A11,YELLOW_0:30;
then
A12: x "/\" y <= x "/\" z by A8,A5,YELLOW_3:2;
x in {x} by TARSKI:def 1;
then x "/\" z <= sup ({x} "/\" X) by A2,A10,YELLOW_4:1,37;
hence q <= sup ({x} "/\" X) by A6,A12,YELLOW_0:def 2;
end;
ex_sup_of T "/\" finsups X,L by WAYBEL_0:75;
then sup ({x} "/\" finsups X) <= sup ({x} "/\" X) by A4,YELLOW_0:30;
then
A13: 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 A2,YELLOW_4:53;
hence thesis by A13,ORDERS_2:2;
end;
begin :: On the inf and sup operation
definition
let L be non empty RelStr;
func inf_op L -> Function 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 Function of [:L,L:], L such that
A2: for x, y being Element of L holds f.(x,y) = F(x,y) from YELLOW_3:
sch 6 (A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f, g be Function 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
ex a, b being object st a in the carrier of L & b in the carrier of L & x =
[a,b] by ZFMISC_1:def 2;
hence (inf_op L).x = (inf_op L).(x`1,x`2)
.= x`1 "/\" x`2 by Def4;
end;
registration
let L be with_infima transitive antisymmetric RelStr;
cluster inf_op L -> monotone;
coherence
proof
let x, y be Element of [:L,L:];
set f = inf_op L;
assume x <= y;
then
A1: x`1 <= y`1 & x`2 <= y`2 by YELLOW_3:12;
A2: f.x = x`1 "/\" x`2 & f.y = y`1 "/\" y`2 by Th31;
let a, b be Element of L;
assume a = f.x & b = f.y;
hence thesis 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;
reconsider X = [:D1,D2:] as set;
thus f.:[:D1,D2:] c= D1 "/\" D2
proof
let q be object;
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:] and
A3: q1 = f.c by A1,FUNCT_2:65;
consider x, y being object such that
A4: x in D1 & y in D2 and
A5: c = [x,y] by A2,ZFMISC_1:def 2;
reconsider x, y as Element of S by A4;
q = f.(x,y) by A3,A5
.= x "/\" y by Def4;
then
q in { a "/\" b where a, b is Element of S : a in D1 & b in D2 } by A4;
hence thesis by YELLOW_4:def 4;
end;
let q be object;
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
A6: q = x "/\" y & x in D1 & y in D2;
q = f.(x,y) & [x,y] in X by A6,Def4,ZFMISC_1:87;
hence thesis by FUNCT_2:35;
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;
reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def 2;
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: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75;
A2: f.:[:D1,D2:] = D1 "/\" D2 by Th32;
A3: f.:[:D1,D2:] c= f.:(downarrow D) & f.:(downarrow D) c= downarrow (f.:D)
by Th13,RELAT_1:123,YELLOW_3:48;
A4: f.:D is directed by YELLOW_2:15;
then
A5: ex_sup_of f.:D,L by WAYBEL_0:75;
ex_sup_of downarrow (f.:D),L by A4,WAYBEL_0:75;
then sup (D1 "/\" D2) <= sup (downarrow (f.: D)) by A1,A3,A2,XBOOLE_1:1
,YELLOW_0:34;
then
A6: sup (D1 "/\" D2) <= sup(f.:D) by A5,WAYBEL_0:33;
f.:D9 c= f.:[:D1,D2:] by RELAT_1:123,YELLOW_3:1;
then f.:D9 c= D1 "/\" D2 by Th32;
then sup (f.:D) <= sup (D1 "/\" D2) by A5,A1,YELLOW_0:34;
hence thesis by A6,ORDERS_2:2;
end;
definition
let L be non empty RelStr;
func sup_op L -> Function 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 Function of [:L,L:], L such that
A2: for x, y being Element of L holds f.(x,y) = F(x,y) from YELLOW_3:
sch 6 (A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f, g be Function 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
ex a, b being object st a in the carrier of L & b in the carrier of L & x =
[a,b] by ZFMISC_1:def 2;
hence (sup_op L).x = (sup_op L).(x`1,x`2)
.= x`1 "\/" x`2 by Def5;
end;
registration
let L be with_suprema transitive antisymmetric RelStr;
cluster sup_op L -> monotone;
coherence
proof
let x, y be Element of [:L,L:];
set f = sup_op L;
assume x <= y;
then
A1: x`1 <= y`1 & x`2 <= y`2 by YELLOW_3:12;
A2: f.x = x`1 "\/" x`2 & f.y = y`1 "\/" y`2 by Th34;
let a, b be Element of L;
assume a = f.x & b = f.y;
hence thesis 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;
reconsider X = [:D1,D2:] as set;
thus f.:[:D1,D2:] c= D1 "\/" D2
proof
let q be object;
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:] and
A3: q1 = f.c by A1,FUNCT_2:65;
consider x, y being object such that
A4: x in D1 & y in D2 and
A5: c = [x,y] by A2,ZFMISC_1:def 2;
reconsider x, y as Element of S by A4;
q = f.(x,y) by A3,A5
.= x "\/" y by Def5;
then
q in { a "\/" b where a, b is Element of S : a in D1 & b in D2 } by A4;
hence thesis by YELLOW_4:def 3;
end;
let q be object;
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
A6: q = x "\/" y & x in D1 & y in D2;
q = f.(x,y) & [x,y] in X by A6,Def5,ZFMISC_1:87;
hence thesis by FUNCT_2:35;
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;
reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def 2;
set D1 = proj1 D, D2 = proj2 D, f = sup_op L;
A1: ex_inf_of D1 "\/" D2,L by YELLOW_0:17;
A2: ex_inf_of uparrow (f.:D),L & f.:[:D1,D2:] c= f.:(uparrow D) by RELAT_1:123
,YELLOW_0:17,YELLOW_3:49;
f.:(uparrow D) c= uparrow (f.:D) & f.:[:D1,D2:] = D1 "\/" D2 by Th14,Th35;
then inf (D1 "\/" D2) >= inf (uparrow (f.:D)) by A1,A2,XBOOLE_1:1,YELLOW_0:35
;
then
A3: inf (D1 "\/" D2) >= inf(f.:D) by WAYBEL_0:38,YELLOW_0:17;
f.:D9 c= f.:[:D1,D2:] by RELAT_1:123,YELLOW_3:1;
then ex_inf_of f.:D9,L & f.:D9 c= D1 "\/" D2 by Th35,YELLOW_0:17;
then inf (f.:D) >= inf (D1 "\/" D2) by A1,YELLOW_0:35;
hence thesis by A3,ORDERS_2:2;
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
R is up-complete satisfying_MC;
end;
registration
cluster -> satisfying_MC for 1-element reflexive RelStr;
coherence
by STRUCT_0:def 10;
end;
registration
cluster meet-continuous -> up-complete satisfying_MC for non empty reflexive
RelStr;
coherence;
cluster up-complete satisfying_MC -> meet-continuous for non empty reflexive
RelStr;
coherence;
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;
set f = SupMap L;
let I1, I2 be Ideal of L;
reconsider x = I1, y = I2 as Element of InclPoset(Ids L) by YELLOW_2:41;
A2: f preserves_inf_of {x,y} by A1;
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;
registration
let L be up-complete sup-Semilattice;
cluster SupMap L -> join-preserving;
coherence
proof
let x, y be Element of InclPoset(Ids L);
set f = SupMap L;
assume ex_sup_of {x,y},InclPoset(Ids L);
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:41;
A1: ex_sup_of x1 "\/" y1,L by WAYBEL_0:75;
A2: dom f = the carrier of InclPoset(Ids L) by FUNCT_2:def 1;
then f.:{x,y} = {f.x,f.y} by FUNCT_1:60;
hence ex_sup_of f.:{x,y},L by YELLOW_0:20;
thus sup (f.:{x,y}) = sup {f.x,f.y} by A2,FUNCT_1:60
.= 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 A1,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);
let x, y be Element of InclPoset(Ids L);
set f = SupMap L;
assume ex_inf_of {x,y},InclPoset(Ids L);
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:41;
A2: dom f = the carrier of InclPoset(Ids L) by FUNCT_2:def 1;
then f.:{x,y} = {f.x,f.y} by FUNCT_1:60;
hence ex_inf_of f.:{x,y},L by YELLOW_0:21;
thus inf (f.:{x,y}) = inf {f.x,f.y} by A2,FUNCT_1:60
.= 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 D2,L by WAYBEL_0:75;
A3: ex_sup_of (downarrow D1 "/\" downarrow D2),L by WAYBEL_0:75;
A4: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75;
ex_sup_of D1,L by WAYBEL_0:75;
hence (sup D1) "/\" (sup D2) = (sup downarrow D1) "/\" (sup D2) by
WAYBEL_0:33
.= (sup downarrow D1) "/\" (sup downarrow D2) by A2,WAYBEL_0:33
.= sup (downarrow D1 "/\" downarrow D2) by A1
.= sup downarrow ((downarrow D1) "/\" (downarrow D2)) by A3,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 rng netmap (N,L) by YELLOW_2:def 5
.= sup ({x} "/\" rng netmap (N,L)) by A1,A2;
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:7;
reconsider N = NetStr (#D,(the InternalRel of L)|_2 D,n#) as prenet of L by
Th19;
A2: Sup netmap (N,L) = sup N;
D c= D;
then
A3: D = n.:D by FUNCT_1:92
.= rng netmap (N,L) by RELSET_1:22;
hence x "/\" sup D = x "/\" Sup netmap (N,L) by YELLOW_2:def 5
.= sup ({x} "/\" D) by A1,A3,A2,Th20;
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;
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
.= 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
reconsider D1 = proj1 DD, D2 = proj2 DD as non empty directed Subset of L
by YELLOW_3:21,22;
reconsider C = the carrier of L as non empty set;
set f = inf_op L;
assume ex_sup_of D,[:L,L:];
set d2 = sup D2;
defpred P[set] means ex x being Element of L st $1 = {x} "/\" D2 & x in D1;
f.:DD is directed by YELLOW_2:15;
hence ex_sup_of f.:D,L by WAYBEL_0:75;
{x "/\" y where x, y is Element of L : x in D1 & y in {d2}} c= C
proof
let q be object;
assume q in {x "/\" y where x, y is Element of L : x in D1 & y in {d2}};
then ex x, y being Element of L st q = x "/\" y & x in D1 & y in {d2};
hence thesis;
end;
then reconsider
F = {x "/\" y where x, y is Element of L : x in D1 & y in {d2}}
as Subset of L;
A2: "\/" ({ 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;
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 object;
assume q in F;
then consider x, y being Element of L such that
A4: q = x "/\" y and
A5: x in D1 and
A6: y in {d2};
q = x "/\" d2 by A4,A6,TARSKI:def 1
.= sup ({x} "/\" D2) by A1,Th28;
hence thesis by A5;
end;
let q be object;
A7: d2 in {d2} by TARSKI:def 1;
assume q in { sup ({z} "/\" D2) where z is Element of L : z in D1 };
then consider z being Element of L such that
A8: q = sup ({z} "/\" D2) and
A9: z in D1;
q = z "/\" d2 by A1,A8,Th28;
hence thesis by A9,A7;
end;
thus sup (f.:D) = sup (D1 "/\" D2) by Th33
.= "\/" ({ "\/" (X,L) where X is non empty directed Subset of L: P[X]
},L) by A2,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: for x being Element of Fin J holds ex_sup_of f.:x,L by YELLOW_0:17;
ex_sup_of rng f,L & ex_sup_of rng netmap (FinSups f,L),L by YELLOW_0:17;
hence x "/\" Sup f = x "/\" sup F by A2,Th26
.= sup ({x} "/\" rng netmap (F,L)) by A1
.= "\/" (rng the mapping of x "/\" F,L) by Th23
.= sup (x "/\" F) by YELLOW_2:def 5;
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;
reconsider R = rng netmap (N,L) as non empty directed Subset of L by A2,Th18;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
set f = the mapping of N;
set h = the mapping of FinSups f;
A3: ex_sup_of xx "/\" R,L by WAYBEL_0:75;
A4: rng the mapping of x "/\" FinSups f is_<=_than sup ({x} "/\" rng netmap
(N,L))
proof
let a be Element of L;
A5: {x} "/\" rng h = {x "/\" y where y is Element of L: y in rng h} by
YELLOW_4:42;
assume a in rng the mapping of x "/\" FinSups f;
then a in {x} "/\" rng h by Th23;
then consider y being Element of L such that
A6: a = x "/\" y and
A7: y in rng h by A5;
for x being set holds ex_sup_of f.:x,L by YELLOW_0:17;
then rng netmap(FinSups f,L) c= finsups rng f by Th24;
then y in finsups rng f by A7;
then consider Y being finite Subset of rng f such that
A8: y = "\/"(Y,L) and
A9: ex_sup_of Y,L;
rng netmap (N,L) is directed by A2,Th18;
then consider z being Element of L such that
A10: z in rng f and
A11: z is_>=_than Y by WAYBEL_0:1;
A12: x <= x;
"\/"(Y,L) <= z by A9,A11,YELLOW_0:30;
then
A13: x "/\" y <= x "/\" z by A8,A12,YELLOW_3:2;
x in {x} by TARSKI:def 1;
then x "/\" z <= sup (xx "/\" rng f) by A3,A10,YELLOW_4:1,37;
hence a <= sup ({x} "/\" rng netmap (N,L)) by A6,A13,YELLOW_0:def 2;
end;
x "/\" FinSups f is eventually-directed by Th27;
then rng netmap(x "/\" FinSups f,L) is directed by Th18;
then ex_sup_of rng the mapping of x "/\" FinSups f,L by WAYBEL_0:75;
then sup (x "/\" FinSups f) = "\/"(rng the mapping of x "/\" FinSups f,L) &
"\/"( rng the mapping of x "/\" FinSups f,L) <= sup ({x} "/\" rng netmap (N,L))
by A4,YELLOW_0:def 9,YELLOW_2:def 5;
then
A14: x "/\" Sup netmap (N,L) <= sup ({x} "/\" rng netmap (N,L)) by A1;
ex_sup_of R,L & Sup netmap (N,L) = "\/"(rng netmap(N,L),L) by WAYBEL_0:75
,YELLOW_2:def 5;
then sup ({x} "/\" rng netmap (N,L)) <= x "/\" Sup netmap (N,L) by A3,
YELLOW_4:53;
hence thesis by A14,ORDERS_2:2;
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
A1: L is meet-continuous;
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 thesis 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 thesis by Th44;
end;
registration
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;
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;
thus L is meet-continuous implies 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;
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
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;
registration
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))
by Th41,Th42;
:: 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;
reconsider X1 = X as non empty Subset of L by A1;
assume ex_sup_of X,L;
A2: x"/\".:X1 is non empty;
x"/\".:X is directed by A1,YELLOW_2:15;
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:61
.= sup({x} "/\" X) by YELLOW_4:42
.= x "/\" sup X by A1,A3,Th28
.= x"/\".sup X by WAYBEL_1:def 18;
end;
registration
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 "/\" is lower_adjoint;
then 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:64;
then H is up-complete satisfying_MC by Th37;
hence H is meet-continuous;
thus H is distributive by A1;
end;
assume
A2: H is meet-continuous distributive;
thus H is LATTICE;
let a be Element of H;
( for X being finite Subset of H holds a "/\" preserves_sup_of X)& for X
being non empty directed Subset of H holds a "/\" preserves_sup_of X by A2,Th17
,WAYBEL_0:def 37;
then a "/\" is sups-preserving by WAYBEL_0:74;
hence thesis by WAYBEL_1:17;
end;
registration
cluster complete Heyting -> meet-continuous distributive for
non empty Poset;
coherence by Th56;
cluster complete meet-continuous distributive -> Heyting for
non empty Poset;
coherence by Th56;
end;