Copyright (c) 1996 Association of Mizar Users
environ
vocabulary WAYBEL_0, ORDERS_1, FUNCT_1, RELAT_1, FUNCT_4, QUANTAL1, RELAT_2,
ORDINAL2, LATTICES, REALSET1, PRE_TOPC, YELLOW_0, BHSP_3, FUNCOP_1,
BOOLE, LATTICE3, SEQM_3, WAYBEL_2, WAYBEL_3, TARSKI, FILTER_0, SUBSET_1,
ORDERS_2, ZFMISC_1, FINSET_1, YELLOW_1, FUNCT_3, FRAENKEL, LATTICE2,
OPPCAT_1, WAYBEL_5, ZF_REFLE, PBOOLE, YELLOW_2, FUNCT_6, CARD_3, PRALG_1,
FINSEQ_4, WAYBEL_6, HAHNBAN;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
FINSET_1, RELAT_1, ORDINAL1, RELAT_2, REALSET1, STRUCT_0, ORDERS_1,
PRE_TOPC, CARD_3, FRAENKEL, LATTICE3, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_6,
PBOOLE, PRALG_1, PRALG_2, YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1,
YELLOW_2, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, BORSUK_1,
YELLOW_7, FUNCT_7;
constructors WAYBEL_5, WAYBEL_4, NAT_1, RELAT_2, BORSUK_1, YELLOW_4, ORDERS_3,
WAYBEL_1, WAYBEL_2, WAYBEL_3, PRALG_2, FUNCT_7, MEMBERED;
clusters SUBSET_1, WAYBEL_0, WAYBEL_2, WAYBEL_3, YELLOW_0, STRUCT_0, ORDERS_1,
LATTICE3, PBOOLE, FINSET_1, WAYBEL_1, WAYBEL_5, PRALG_1, YELLOW_7,
YELLOW_4, RELSET_1, ARYTM_3, XBOOLE_0, FRAENKEL, MEMBERED, ZFMISC_1,
FUNCT_2, PARTFUN1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RELAT_2, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_5,
FUNCT_1, ORDERS_3, XBOOLE_0;
theorems WAYBEL_3, TARSKI, YELLOW_0, ZFMISC_1, WAYBEL_0, ORDERS_1, WAYBEL_4,
FUNCT_2, FUNCT_1, LATTICE3, NAT_1, PRE_TOPC, WAYBEL_1, YELLOW_1,
YELLOW_5, WAYBEL_2, YELLOW_2, FINSET_1, WAYBEL_5, CARD_3, PBOOLE,
PRALG_2, FUNCT_6, YELLOW_7, ORDERS_2, RELAT_2, FRAENKEL, CARD_5, FUNCT_3,
YELLOW_6, YELLOW_4, YELLOW_3, BORSUK_1, FUNCOP_1, RELAT_1, RELSET_1,
PRALG_1, ORDINAL1, XBOOLE_0, XBOOLE_1, FUNCT_7, XCMPLX_1;
schemes FUNCT_1, FINSET_1, WAYBEL_3, ZFREFLE1, NAT_1, YELLOW_2, YELLOW_3,
COMPTS_1;
begin
reserve x,y,Y,Z for set,
L for LATTICE,
l for Element of L,
n,k for Nat;
:: Preliminaries
scheme NonUniqExD1 { Z() ->non empty RelStr, X() -> Subset of Z(),
Y() -> non empty Subset of Z(), P[set,set] }:
ex f being Function of X(),Y() st
for e be Element of Z() st e in X()
ex u be Element of Z() st u in Y() & u = f.e & P[e,u]
provided
A1: for e be Element of Z() st e in X() ex u be Element of Z()
st u in Y() & P[e,u]
proof
defpred p[set,set] means P[$1,$2];
A2: for e be set st e in X() ex u be set st u in Y() & p[e,u]
proof
let e be set; assume A3: e in X();
then reconsider e1 = e as Element of X();
reconsider e1 as Element of Z() by A3;
consider u be Element of Z() such that A4: u in Y() & P[e1,u] by A1,A3;
reconsider u1 = u as set;
take u1;
thus thesis by A4;
end;
consider f being Function such that
A5: dom f = X() & rng f c= Y() and
A6: for e be set st e in X() holds p[e,f.e] from NonUniqBoundFuncEx(A2);
reconsider f as Function of X(),Y() by A5,FUNCT_2:def 1,RELSET_1:11;
A7: for e be Element of Z() st e in X()
ex u be Element of Z() st u in Y() & u = f.e & P[e,u]
proof
let e be Element of Z(); assume A8: e in X();
then reconsider e1 = f.e as Element of Y() by FUNCT_2:7;
reconsider fe = e1 as Element of Z();
take fe;
thus thesis by A6,A8;
end;
take f;
thus thesis by A7;
end;
definition
let L be LATTICE;
let A be non empty Subset of L;
let f be Function of A,A;
let n be Element of NAT;
redefine func iter (f,n) -> Function of A,A;
coherence by FUNCT_7:85;
end;
definition
let L be LATTICE;
let C,D be non empty Subset of L;
let f be Function of C,D;
let c be Element of C;
redefine func f.c -> Element of L;
coherence
proof
f.c in D;
hence thesis;
end;
end;
definition
let L be non empty Poset;
cluster -> filtered directed Chain of L;
coherence
proof
let C be Chain of L;
A1:the InternalRel of L is_strongly_connected_in C by ORDERS_1:def 11;
thus C is filtered
proof
let x,y be Element of L; assume A2: x in C & y in C;
then [x,y] in the InternalRel of L or [y,x] in the InternalRel of L
by A1,RELAT_2:def 7;
then A3: x <= y or y <= x by ORDERS_1:def 9;
x <= x & y <= y;
hence thesis by A2,A3;
end;
let x,y be Element of L; assume A4: x in C & y in C;
then [x,y] in the InternalRel of L or [y,x] in the InternalRel of L
by A1,RELAT_2:def 7;
then A5:x <= y or y <= x by ORDERS_1:def 9;
x <= x & y <= y;
hence thesis by A4,A5;
end;
end;
definition
cluster strict continuous distributive lower-bounded LATTICE;
existence
proof
consider x1 being set, R be Order of {x1};
reconsider RS = RelStr(#{x1},R#) as trivial reflexive non empty RelStr;
take RS;
thus thesis;
end;
end;
theorem Th1:
for S,T being Semilattice, f being map of S,T
holds f is meet-preserving iff for x,y being Element of S holds
f.(x "/\" y) = f. x "/\" f.y
proof
let S,T be Semilattice, f be map of S,T;
A1: dom f = the carrier of S by FUNCT_2:def 1;
thus f is meet-preserving implies
for x,y being Element of S holds f.(x "/\" y) = f. x "/\" f.y
proof
assume A2: f is meet-preserving;
let z,y be Element of S;
A3: f.:{z,y} = {f.z,f.y} by A1,FUNCT_1:118;
A4: ex_inf_of {z,y},S by YELLOW_0:21;
A5: f preserves_inf_of {z,y} by A2,WAYBEL_0:def 34;
thus f.(z "/\" y) = f.inf {z,y} by YELLOW_0:40
.= inf({f.z,f.y}) by A3,A4,A5,WAYBEL_0:def 30
.= f.z "/\" f.y by YELLOW_0:40;
end;
assume A6: for x,y being Element of S holds f.(x "/\" y) = f. x "/\" f.y;
for z,y being Element of S holds f preserves_inf_of {z,y}
proof
let z,y be Element of S;
A7: f.:{z,y} = {f.z,f.y} by A1,FUNCT_1:118;
then A8: ex_inf_of {z,y},S implies ex_inf_of f.:{z,y},T
by YELLOW_0:21;
inf (f.:{z,y}) = f.z "/\" f.y by A7,YELLOW_0:40
.= f.(z "/\" y) by A6
.= f.inf {z,y} by YELLOW_0:40;
hence thesis by A8,WAYBEL_0:def 30;
end;
hence f is meet-preserving by WAYBEL_0:def 34;
end;
theorem Th2:
for S,T being sup-Semilattice, f being map of S,T holds
f is join-preserving iff for x,y being Element of S holds
f.(x "\/" y) = f. x "\/" f.y
proof
let S,T be sup-Semilattice, f be map of S,T;
A1: dom f = the carrier of S by FUNCT_2:def 1;
thus f is join-preserving implies
for x,y being Element of S holds f.(x "\/" y) = f. x "\/" f.y
proof
assume A2: f is join-preserving;
let z,y be Element of S;
A3: f.:{z,y} = {f.z,f.y} by A1,FUNCT_1:118;
A4: ex_sup_of {z,y},S by YELLOW_0:20;
A5: f preserves_sup_of {z,y} by A2,WAYBEL_0:def 35;
thus f.(z "\/" y) = f.sup {z,y} by YELLOW_0:41
.= sup ({f.z,f.y}) by A3,A4,A5,WAYBEL_0:def 31
.= f.z "\/" f.y by YELLOW_0:41;
end;
assume A6: for x,y being Element of S holds f.(x "\/" y) = f. x "\/" f.y;
for z,y being Element of S holds f preserves_sup_of {z,y}
proof
let z,y be Element of S;
A7: f.:{z,y} = {f.z,f.y} by A1,FUNCT_1:118;
then A8: ex_sup_of {z,y},S implies ex_sup_of f.:{z,y},T
by YELLOW_0:20;
sup (f.:{z,y}) = f.z "\/" f.y by A7,YELLOW_0:41
.= f.(z "\/" y) by A6
.= f.sup {z,y} by YELLOW_0:41;
hence thesis by A8,WAYBEL_0:def 31;
end;
hence f is join-preserving by WAYBEL_0:def 35;
end;
theorem Th3:
for S,T being LATTICE, f being map of S,T st T is distributive &
f is meet-preserving join-preserving one-to-one holds
S is distributive
proof
let S,T be LATTICE, f be map of S,T; assume that
A1: T is distributive and
A2: f is meet-preserving join-preserving one-to-one;
let x,y,z be Element of S;
f.( x "/\" (y "\/" z)) = f. x "/\" f.(y "\/" z) by A2,Th1
.= f. x "/\" (f.y "\/" f.z) by A2,Th2
.= (f.x "/\" f.y) "\/" (f.x "/\" f.z) by A1,WAYBEL_1:def 3
.= (f.x "/\" f.y) "\/" f.(x "/\" z) by A2,Th1
.= f.(x "/\" y) "\/" f.(x "/\" z) by A2,Th1
.= f.((x "/\" y) "\/" (x "/\" z))by A2,Th2;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A2,FUNCT_2:25;
end;
definition
let S,T be complete LATTICE;
cluster sups-preserving map of S,T;
existence
proof
set t = Bottom T;
set f = S --> t;
take f;
let X be Subset of S;
assume ex_sup_of X,S;
thus ex_sup_of f.:X,T by YELLOW_0:17;
A1: (f.:X) c= rng f by RELAT_1:144;
A2: f = (the carrier of S) --> t by BORSUK_1:def 3;
then rng f c= {t} by FUNCOP_1:19;
then (f.:X) c= {t} by A1,XBOOLE_1:1;
then A3:(f.:X) = {t} or (f.:X) = {} by ZFMISC_1:39;
per cases;
suppose X = {};
then (f.:X) = {} by RELAT_1:149;
then sup (f.:X) = t by YELLOW_0:def 11;
hence sup (f.:X) = f.sup X by A2,FUNCOP_1:13;
suppose X <> {};
then reconsider X1 = X as non empty Subset of S;
consider x be Element of X1;
f.x in (f.:X) by FUNCT_2:43;
hence sup (f.:X) = t by A3,YELLOW_0:39
.= f.sup X by A2,FUNCOP_1:13;
end;
end;
Lm1:
for S,T being with_suprema non empty Poset
for f being map of S, T holds
f is directed-sups-preserving implies f is monotone
proof
let S,T be with_suprema non empty Poset;
let f be map of S, T;
assume
A1: f is directed-sups-preserving;
let x, y be Element of S such that
A2: x <= y;
let afx, bfy be Element of T such that
A3: afx = f.x & bfy = f.y;
A4: y = y"\/"x by A2,YELLOW_0:24;
x <= y & y <= y by A2;
then A5: {x, y} is_<=_than y by YELLOW_0:8;
for b being Element of S st {x, y} is_<=_than b holds y <= b by YELLOW_0:8;
then A6: ex_sup_of {x, y},S by A5,YELLOW_0:30;
for a, b being Element of S st a in {x, y} & b in {x, y}
ex z being Element of S st z in {x, y} & a <= z & b <= z
proof
let a, b be Element of S such that
A7: a in {x, y} & b in {x, y};
take y;
thus y in {x, y} by TARSKI:def 2;
thus a <= y & b <= y by A2,A7,TARSKI:def 2;
end;
then {x, y} is directed non empty by WAYBEL_0:def 1;
then f preserves_sup_of {x, y} by A1,WAYBEL_0:def 37;
then A8: sup(f.:{x, y}) = f.sup{x, y} by A6,WAYBEL_0:def 31
.= f.y by A4,YELLOW_0:41;
dom f = the carrier of S by FUNCT_2:def 1;
then f.y = sup{f.x, f.y} by A8,FUNCT_1:118
.= f.y"\/"f.x by YELLOW_0:41;
hence afx <= bfy by A3,YELLOW_0:22;
end;
theorem Th4:
for S,T being complete LATTICE, f being sups-preserving map of S,T st
T is meet-continuous & f is meet-preserving one-to-one holds
S is meet-continuous
proof
let S,T be complete LATTICE, f be sups-preserving map of S,T;
assume that
A1: T is meet-continuous and
A2: f is meet-preserving one-to-one;
A3: f is monotone by Lm1;
A4: T is meet-continuous LATTICE by A1;
S is satisfying_MC
proof
let x be Element of S, D be non empty directed Subset of S;
A5: dom f = the carrier of S & rng f c= the carrier of T by FUNCT_2:def 1;
A6: ex_sup_of D,S & f preserves_sup_of D by WAYBEL_0:75,def 33;
reconsider Y = {x} as directed non empty Subset of S by WAYBEL_0:5;
A7: ex_sup_of Y"/\"D,S & f preserves_sup_of {x}"/\"D by WAYBEL_0:75,def 33;
A8: {f.x} "/\" (f.:D) =
{(f.x) "/\" y where y is Element of T: y in (f.:D)} by YELLOW_4:42;
A9: {x} "/\" D =
{x "/\" y where y is Element of S: y in D} by YELLOW_4:42;
A10: {f.x} "/\" (f.:D) c= f.:({x}"/\"D)
proof
let p be set; assume p in {f.x} "/\" (f.:D);
then consider y be Element of T such that A11:p = (f.x) "/\" y & y in (f
.:D) by A8;
consider k be set such that A12: k in dom f & k in D & y = f.k
by A11,FUNCT_1:def 12;
reconsider k as Element of S by A12;
f preserves_inf_of {x,k} by A2,WAYBEL_0:def 34;
then A13: p = f.(x "/\" k) by A11,A12,YELLOW_3:8;
(x "/\" k) in {x "/\" a where a is Element of S: a in D} by A12;
then (x "/\" k) in dom f & (x "/\" k) in ({x} "/\" D) by A5,YELLOW_4:42
;
hence p in f.:({x}"/\"D) by A13,FUNCT_1:def 12;
end;
A14: f.:({x}"/\"D) c= {f.x} "/\" (f.:D)
proof
let p be set; assume p in f.:({x}"/\"D);
then consider m be set such that
A15: m in dom f & m in ({x} "/\" D) & p = f.m by FUNCT_1:def 12;
reconsider m as Element of S by A15;
consider a be Element of S such that
A16: m = x "/\" a & a in D by A9,A15;
reconsider fa = f.a as Element of T;
A17: fa in f.:D by A5,A16,FUNCT_1:def 12;
f preserves_inf_of {x,a} by A2,WAYBEL_0:def 34;
then p = (f.x) "/\" fa by A15,A16,YELLOW_3:8;
hence thesis by A8,A17;
end;
reconsider X = f.:D as directed Subset of T by A3,YELLOW_2:17;
f.(x "/\" sup D) = (f.x) "/\" (f.sup D) by A2,Th1
.= (f.x) "/\" sup X by A6,WAYBEL_0:def 31
.= sup ({f.x} "/\" X) by A4,WAYBEL_2:def 6
.= sup (f.:({x} "/\" D)) by A10,A14,XBOOLE_0:def 10
.= f.(sup ({x} "/\" D)) by A7,WAYBEL_0:def 31;
hence x "/\" sup D = sup ({x} "/\" D) by A2,A5,FUNCT_1:def 8;
end;
hence thesis by WAYBEL_2:def 7;
end;
begin :: Open sets
definition ::def 3.1, p.68
let L be non empty reflexive RelStr,
X be Subset of L;
attr X is Open means :Def1:
for x be Element of L st x in X ex y be Element of L st y in X & y << x;
end;
theorem
for L be up-complete LATTICE, X be upper Subset of L holds
X is Open iff for x be Element of L st x in X holds waybelow x meets X
proof
let L be up-complete LATTICE, X be upper Subset of L;
hereby assume A1: X is Open;
thus for x be Element of L st x in X holds waybelow x meets X
proof
let x be Element of L; assume x in X;
then consider y be Element of L such that A2: y in X & y << x by A1,Def1;
y in {y1 where y1 is Element of L: y1 << x} by A2;
then y in waybelow x by WAYBEL_3:def 3;
hence waybelow x meets X by A2,XBOOLE_0:3;
end;
end;
assume A3: for x be Element of L st x in X holds waybelow x meets X;
now let x1 be Element of L; assume
x1 in X;
then (waybelow x1) meets X by A3;
then consider y such that A4: y in (waybelow x1) and A5: y in X by XBOOLE_0:
3;
waybelow x1 = {y1 where y1 is Element of L: y1 << x1} by WAYBEL_3:def 3;
then consider z be Element of L such that
A6: z = y & z << x1 by A4;
thus ex z be Element of L st z in X & z << x1 by A5,A6;
end;
hence X is Open by Def1;
end;
theorem ::3.2, p.68
for L be up-complete LATTICE, X be upper Subset of L holds
X is Open iff X = union {wayabove x where x is Element of L : x in X}
proof
let L be up-complete LATTICE, X be upper Subset of L;
hereby assume A1: X is Open;
A2: X c= union {wayabove x where x is Element of L : x in X}
proof
let z be set; assume A3: z in X;
then reconsider x1 = z as Element of X;
reconsider x1 as Element of L by A3;
consider y be Element of L such that
A4: y in X & y << x1 by A1,A3,Def1;
x1 in {y1 where y1 is Element of L: y1 >> y} by A4;
then A5: x1 in wayabove y by WAYBEL_3:def 4;
wayabove y in {wayabove x where x is Element of L : x in X} by A4;
hence thesis by A5,TARSKI:def 4;
end;
union {wayabove x where x is Element of L : x in X} c= X
proof
let z be set; assume
z in union {wayabove x where x is Element of L : x in X};
then consider Y be set such that
A6: z in Y and
A7: Y in {wayabove x where x is Element of L : x in X} by TARSKI:def 4;
consider x be Element of L such that
A8: Y = wayabove x & x in X by A7;
z in {y where y is Element of L: y >> x} by A6,A8,WAYBEL_3:def 4;
then consider z1 be Element of L such that A9: z1 = z & z1 >> x;
x <= z1 by A9,WAYBEL_3:1;
hence thesis by A8,A9,WAYBEL_0:def 20;
end;
hence X = union {wayabove x where x is Element of L : x in X}
by A2,XBOOLE_0:def 10;
end;
assume A10: X = union {wayabove x where x is Element of L : x in X};
now let x1 be Element of L; assume
x1 in X;
then consider Y be set such that
A11: x1 in Y and
A12: Y in {wayabove x where x is Element of L : x in X} by A10,TARSKI:def 4;
consider x be Element of L such that
A13: Y = wayabove x & x in X by A12;
x1 in {y where y is Element of L: y >> x} by A11,A13,WAYBEL_3:def 4;
then consider z1 be Element of L such that
A14: z1 = x1 & z1 >> x;
thus ex x be Element of L st x in X & x << x1 by A13,A14;
end;
hence X is Open by Def1;
end;
definition
let L be up-complete lower-bounded LATTICE;
cluster Open Filter of L;
existence
proof
take [#]L;
now let x be Element of L; assume x in [#]L;
A1: [#]L = the carrier of L by PRE_TOPC:12;
Bottom L << x by WAYBEL_3:4;
hence ex y be Element of L st y in [#]L & y << x by A1;
end;
hence thesis by Def1;
end;
end;
theorem
for L be lower-bounded continuous LATTICE, x be Element of L holds
(wayabove x) is Open
proof
let L be lower-bounded continuous LATTICE,
x be Element of L;
for l be Element of L st l in (wayabove x)
ex y be Element of L st y in (wayabove x) & y << l
proof
let l be Element of L; assume l in (wayabove x);
then x << l by WAYBEL_3:8;
then consider y be Element of L such that
A1: x << y & y << l by WAYBEL_4:53;
take y;
thus thesis by A1,WAYBEL_3:8;
end;
hence thesis by Def1;
end;
theorem Th8: ::3.3, p.68
for L be lower-bounded continuous LATTICE, x,y be Element of L st x << y holds
ex F be Open Filter of L st y in F & F c= wayabove x
proof
let L be lower-bounded continuous LATTICE,
x,y be Element of L; assume
A1: x << y;
then A2: y in (wayabove x) by WAYBEL_3:8;
reconsider W = (wayabove x) as non empty Subset of L by A1,WAYBEL_3:8;
defpred P[Element of L, Element of L] means $2 << $1;
A3: for z be Element of L st z in W
ex z1 be Element of L st z1 in W & P[z,z1]
proof
let z be Element of L; assume z in W;
then x << z by WAYBEL_3:8;
then consider x' be Element of L such that
A4: x << x' & x' << z by WAYBEL_4:53;
x' in W by A4,WAYBEL_3:8;
hence thesis by A4;
end;
consider f be Function of W,W such that
A5: for z be Element of L st z in W
ex z1 be Element of L st z1 in W & z1 = f.z & P[z,z1] from NonUniqExD1(A3);
dom f = W by FUNCT_2:def 1;
then A6: y in (dom f \/ rng f) by A2,XBOOLE_0:def 2;
set F = union {uparrow z where z is Element of L : ex n st z = iter(f,n).y};
now let u1 be set; assume u1 in F;
then consider Y be set such that
A7: u1 in Y and
A8: Y in {uparrow z where z is Element of L : ex n st z = iter(f,n).y}
by TARSKI:def 4;
consider z be Element of L such that
A9: Y = uparrow z and
ex n st z = iter(f,n).y by A8;
reconsider z1 = {z} as Subset of L;
u1 in uparrow z1 by A7,A9,WAYBEL_0:def 18;
then u1 in {a where a is Element of L:
ex b being Element of L st a >= b & b in z1} by WAYBEL_0:15;
then consider a be Element of L such that
A10: a = u1 and
ex b being Element of L st a >= b & b in z1;
thus u1 in the carrier of L by A10;
end;
then F c= the carrier of L by TARSKI:def 3;
then reconsider F as Subset of L;
y <= y;
then A11: y in uparrow y by WAYBEL_0:18;
iter(f,0).y = (id(dom f \/ rng f)).y by FUNCT_7:70
.= y by A6,FUNCT_1:35;
then A12: uparrow y in {uparrow z where z is Element of L : ex n st z = iter(
f,n).y};
set V = {uparrow z where z is Element of L : ex n st z = iter(f,n).y};
now let u1 be set; assume u1 in V;
then consider z be Element of L such that
A13: u1 = uparrow z and
ex n st z = iter(f,n).y;
thus u1 in bool the carrier of L by A13;
end;
then reconsider V as Subset of bool the carrier of L by TARSKI:def 3;
A14: for X being Subset of L st X in V holds X is upper
proof
let X be Subset of L; assume X in V;
then consider z be Element of L such that
A15: X = uparrow z and
ex n st z = iter(f,n).y;
thus X is upper by A15;
end;
A16: for X being Subset of L st X in V holds X is filtered
proof
let X be Subset of L; assume X in V;
then consider z be Element of L such that
A17: X = uparrow z and
ex n st z = iter(f,n).y;
thus X is filtered by A17;
end;
A18: for X,Y being Subset of L st X in V & Y in V
ex Z being Subset of L st Z in V & X \/ Y c= Z
proof
let X,Y be Subset of L; assume A19: X in V & Y in V;
then consider z1 be Element of L such that
A20: X = uparrow z1 and
A21: ex n st z1 = iter(f,n).y;
consider n1 be Nat such that
A22: z1 = iter(f,n1).y by A21;
consider z2 be Element of L such that
A23: Y = uparrow z2 and
A24: ex n st z2 = iter(f,n).y by A19;
consider n2 be Nat such that
A25: z2 = iter(f,n2).y by A24;
reconsider y1 = y as Element of W by A1,WAYBEL_3:8;
A26: for n holds
for k holds iter(f,n+k).y1 <= iter(f,n).y1
proof
let n;
defpred P[Nat] means iter(f,n+$1).y1 <= iter(f,n).y1;
A27: P[0];
A28: for k st P[k] holds P[k+1]
proof
let k; assume A29: iter(f,n+k).y1 <= iter(f,n).y1;
set nk = iter(f,n+k).y1;
nk in W by FUNCT_2:7;
then consider znk be Element of L such that
A30: znk in W & znk = f.nk & znk << nk by A5;
dom iter(f,n+k) = W by FUNCT_2:def 1;
then A31: znk = (f*(iter(f,n+k))).y1 by A30,FUNCT_1:23
.= iter(f,n+k+1).y1 by FUNCT_7:73
.= iter(f,n+(k+1)).y1 by XCMPLX_1:1;
znk <= nk by A30,WAYBEL_3:1;
hence thesis by A29,A31,ORDERS_1:26;
end;
for k holds P[k] from Ind(A27,A28);
hence thesis;
end;
set z = z1 "/\" z2;
A32: now per cases;
suppose n1 <= n2;
then consider k such that A33: n1 + k = n2 by NAT_1:28;
z2 <= z1 by A22,A25,A26,A33;
hence uparrow z in V by A19,A23,YELLOW_0:25;
suppose n2 <= n1;
then consider k such that A34: n2 + k = n1 by NAT_1:28;
z1 <= z2 by A22,A25,A26,A34;
hence uparrow z in V by A19,A20,YELLOW_0:25;
end;
z <= z1 & z <= z2 by YELLOW_0:23;
then uparrow z1 c= uparrow z & uparrow z2 c= uparrow z by WAYBEL_0:22;
then (uparrow z1) \/ (uparrow z2) c= uparrow z by XBOOLE_1:8;
hence thesis by A20,A23,A32;
end;
now let u1 be Element of L; assume u1 in F;
then consider Y be set such that
A35: u1 in Y and
A36: Y in {uparrow z where z is Element of L : ex n st z = iter(f,n).y}
by TARSKI:def 4;
consider z be Element of L such that
A37: Y = uparrow z and
A38: ex n st z = iter(f,n).y by A36;
consider n such that
A39: z = iter(f,n).y by A38;
reconsider z1 = {z} as Subset of L;
u1 in uparrow z1 by A35,A37,WAYBEL_0:def 18;
then u1 in {a where a is Element of L:
ex b being Element of L st a >= b & b in z1} by WAYBEL_0:15;
then consider a be Element of L such that
A40: a = u1 and
A41:ex b being Element of L st a >= b & b in z1;
consider b being Element of L such that
A42:a >= b & b in z1 by A41;
A43: b = z by A42,TARSKI:def 1;
z in W by A2,A39,FUNCT_2:7;
then consider z' be Element of L such that
A44: z' in W & z' = f.z & z' << z by A5;
A45: z' << u1 by A40,A42,A43,A44,WAYBEL_3:2;
z' <= z';
then A46: z' in uparrow z' by WAYBEL_0:18;
dom iter(f,n) = W by FUNCT_2:def 1;
then z' = (f*(iter(f,n))).y by A2,A39,A44,FUNCT_1:23
.= iter(f,n+1).y by FUNCT_7:73;
then uparrow z' in {uparrow p where p is Element of L : ex n st p = iter(f,
n).y};
then z' in F by A46,TARSKI:def 4;
hence ex g be Element of L st g in F & g << u1 by A45;
end;
then reconsider F as Open Filter of L by A11,A12,A14,A16,A18,Def1,TARSKI:def
4,WAYBEL_0:28,47;
take F;
now let u1 be set; assume A47: u1 in F;
then consider Y be set such that
A48: u1 in Y and
A49: Y in {uparrow z where z is Element of L : ex n st z = iter(f,n).y}
by TARSKI:def 4;
consider z be Element of L such that
A50: Y = uparrow z and
A51: ex n st z = iter(f,n).y by A49;
consider n such that
A52: z = iter(f,n).y by A51;
reconsider u = u1 as Element of L by A47;
A53: z <= u by A48,A50,WAYBEL_0:18;
z in wayabove x by A2,A52,FUNCT_2:7;
then x << z by WAYBEL_3:8;
then x << u by A53,WAYBEL_3:2;
hence u1 in wayabove x by WAYBEL_3:8;
end;
hence thesis by A11,A12,TARSKI:def 3,def 4;
end;
theorem Th9: ::3.4, p.69
for L being complete LATTICE, X being Open upper Subset of L holds
for x being Element of L st x in (X`)
ex m being Element of L st x <= m & m is_maximal_in (X`)
proof
let L be complete LATTICE, X be Open upper Subset of L;
let x be Element of L; assume A1: x in (X`);
set A = {C where C is Chain of L : C c= (X`) & x in C};
reconsider x1 = {x} as Chain of L by ORDERS_1:35;
x1 c= (X`) & x in x1 by A1,ZFMISC_1:37;
then A2: x1 in A;
for Z be set st Z <> {} & Z c= A & Z is c=-linear
holds union Z in A
proof
let Z be set; assume that
A3: Z <> {} & Z c= A and
A4: Z is c=-linear;
now let Y; assume Y in Z;
then Y in A by A3;
then ex C be Chain of L st Y = C & C c= (X`) & x in C;
hence Y c= the carrier of L;
end;
then union Z c= the carrier of L by ZFMISC_1:94;
then reconsider UZ = union Z as Subset of L;
the InternalRel of L is_strongly_connected_in UZ
proof
let a,b be set; assume A5: a in UZ & b in UZ;
then consider az be set such that
A6: a in az & az in Z by TARSKI:def 4;
consider bz be set such that
A7: b in bz & bz in Z by A5,TARSKI:def 4;
az, bz are_c=-comparable by A4,A6,A7,ORDINAL1:def 9;
then A8: az c= bz or bz c= az by XBOOLE_0:def 9;
az in A by A3,A6;
then ex C be Chain of L st az = C & C c= (X`) & x in C;
then reconsider az as Chain of L;
bz in A by A3,A7;
then ex C be Chain of L st bz = C & C c= (X`) & x in C;
then reconsider bz as Chain of L;
the InternalRel of L is_strongly_connected_in az &
the InternalRel of L is_strongly_connected_in bz by ORDERS_1:def 11;
hence thesis by A6,A7,A8,RELAT_2:def 7;
end;
then reconsider UZ as Chain of L by ORDERS_1:def 11;
now let Y; assume Y in Z;
then Y in A by A3;
then ex C be Chain of L st Y = C & C c= (X`) & x in C;
hence Y c= (X`);
end;
then A9: UZ c= (X`) by ZFMISC_1:94;
consider Y be Element of Z;
Y in Z by A3;
then Y in A by A3;
then ex C be Chain of L st Y = C & C c= (X`) & x in C;
then x in UZ by A3,TARSKI:def 4;
hence thesis by A9;
end;
then consider Y1 be set such that
A10: Y1 in A & for Z st Z in A & Z <> Y1 holds not Y1 c= Z by A2,ORDERS_2:79;
consider Y be Chain of L such that A11: Y = Y1 & Y c= (X`) & x in Y by A10;
set m = sup Y;
A12: m is_>=_than Y by YELLOW_0:32;
A13: X` = [#](L) \ X by PRE_TOPC:17
.= (the carrier of L) \ X by PRE_TOPC:12;
now assume m in X;
then consider y be Element of L such that A14: y in X & y << m by Def1;
consider d being Element of L such that
A15:d in Y & y <= d by A11,A14,WAYBEL_3:def 1;
d in X by A14,A15,WAYBEL_0:def 20;
hence contradiction by A11,A13,A15,XBOOLE_0:def 4;
end;
then A16:m in (X`) by A13,XBOOLE_0:def 4;
m is_>=_than Y by YELLOW_0:32;
then A17:x <= m by A11,LATTICE3:def 9;
now given y being Element of L such that A18: y in (X`) & y > m;
A19: m <= y & m <> y by A18,ORDERS_1:def 10;
set Y2 = Y \/ {y};
the InternalRel of L is_strongly_connected_in Y2
proof
let a,b be set; assume A20: a in Y2 & b in Y2;
per cases by A20,XBOOLE_0:def 2;
suppose A21: a in Y & b in Y;
the InternalRel of L is_strongly_connected_in Y by ORDERS_1:def 11;
hence [a,b] in the InternalRel of L or
[b,a] in the InternalRel of L by A21,RELAT_2:def 7;
suppose A22: a in Y & b in {y};
then reconsider b1 = b as Element of L;
reconsider a1 = a as Element of L by A22;
A23: b1 = y by A22,TARSKI:def 1;
a1 <= m by A12,A22,LATTICE3:def 9;
then a1 <= b1 by A19,A23,ORDERS_1:26;
hence [a,b] in the InternalRel of L or
[b,a] in the InternalRel of L by ORDERS_1:def 9;
suppose A24: a in {y} & b in Y;
then reconsider b1 = a as Element of L;
reconsider a1 = b as Element of L by A24;
A25: b1 = y by A24,TARSKI:def 1;
a1 <= m by A12,A24,LATTICE3:def 9;
then a1 <= b1 by A19,A25,ORDERS_1:26;
hence [a,b] in the InternalRel of L or
[b,a] in the InternalRel of L by ORDERS_1:def 9;
suppose A26: a in {y} & b in {y};
then reconsider a1 = a as Element of L;
a = y & b = y & a1 <= a1 by A26,TARSKI:def 1;
hence [a,b] in the InternalRel of L or
[b,a] in the InternalRel of L by ORDERS_1:def 9;
end;
then reconsider Y2 as Chain of L by ORDERS_1:def 11;
{y} c= (X`) by A18,ZFMISC_1:37;
then Y2 c= (X`) & x in Y2 by A11,XBOOLE_0:def 2,XBOOLE_1:8;
then A27:Y2 in A;
A28: now assume y in Y;
then y <= m by A12,LATTICE3:def 9;
hence contradiction by A18,ORDERS_1:30;
end;
y in {y} by TARSKI:def 1;
then A29: y in Y2 by XBOOLE_0:def 2;
Y c= Y2 by XBOOLE_1:7;
hence contradiction by A10,A11,A27,A28,A29;
end;
then m is_maximal_in (X`) by A16,WAYBEL_4:56;
hence thesis by A17;
end;
begin :: Irreducible elements
definition ::def 3.5, p.69
let G be non empty RelStr,
g be Element of G;
attr g is meet-irreducible means :Def2:
for x,y being Element of G st g = x "/\" y holds x = g or y = g;
synonym g is irreducible;
end;
definition
let G be non empty RelStr,
g be Element of G;
attr g is join-irreducible means
for x,y being Element of G st g = x "\/" y holds x = g or y = g;
end;
definition
let L be non empty RelStr;
func IRR L -> Subset of L means :Def4:
for x be Element of L holds x in it iff x is irreducible;
existence
proof
defpred P[Element of L] means $1 is irreducible;
consider X being Subset of L such that
A1: for x being Element of L holds x in X iff P[x] from SSubsetEx;
take X;
thus thesis by A1;
end;
uniqueness
proof
let X,Y be Subset of L such that
A2: for x be Element of L holds x in X iff x is irreducible and
A3: for x be Element of L holds x in Y iff x is irreducible;
now let x; assume A4: x in X;
then reconsider x1 = x as Element of L;
x1 is irreducible by A2,A4;
hence x in Y by A3;
end;
then A5: X c= Y by TARSKI:def 3;
now let x; assume A6: x in Y;
then reconsider x1 = x as Element of L;
x1 is irreducible by A3,A6;
hence x in X by A2;
end;
then Y c= X by TARSKI:def 3;
hence X = Y by A5,XBOOLE_0:def 10;
end;
end;
theorem Th10:
for L being upper-bounded antisymmetric with_infima non empty RelStr holds
Top L is irreducible
proof
let L be upper-bounded with_infima antisymmetric non empty RelStr;
let x,y be Element of L; assume x "/\" y = Top L;
then A1: x >= Top L & y >= Top L by YELLOW_0:23;
x <= Top L or y <= Top L by YELLOW_0:45;
hence x = Top L or y = Top L by A1,ORDERS_1:25;
end;
definition
let L be upper-bounded antisymmetric with_infima non empty RelStr;
cluster irreducible Element of L;
existence
proof
take Top L;
thus thesis by Th10;
end;
end;
theorem
for L being Semilattice, x being Element of L holds
x is irreducible iff
for A being finite non empty Subset of L st x = inf A holds x in A
proof let L be Semilattice, I be Element of L;
thus I is irreducible implies
for A being finite non empty Subset of L st I = inf A holds I in A
proof assume
A1: for x,y being Element of L st I = x"/\"y holds I = x or I = y;
let A be finite non empty Subset of L;
A2: A is finite;
defpred P[set] means $1 is non empty & I = "/\"($1,L) implies I in $1;
A3: P[{}];
A4: now let x,B be set such that
A5: x in A & B c= A and
A6: P[B];
thus P[B \/ {x}] proof assume
A7: B \/ {x} is non empty & I = "/\"(B \/ {x},L);
B c= the carrier of L by A5,XBOOLE_1:1;
then reconsider C = B as finite Subset of L
by A5,FINSET_1:13;
reconsider a = x as Element of L by A5;
per cases;
suppose B = {};
then "/\"(B \/ {a},L) = a & a in B \/ {a} by TARSKI:def 1,YELLOW_0:39
;
hence I in B \/ {x} by A7;
suppose
A8: B <> {}; then ex_inf_of C, L & ex_inf_of {a}, L by YELLOW_0:55;
then A9: "/\"(B \/ {x},L) = (inf C)"/\"inf {a} & inf {a} = a
by YELLOW_0:39,YELLOW_2:4;
hereby per cases by A1,A7,A9;
suppose inf C = I;
then consider b being Element of L such that
A10: b in B & b = I by A6,A8;
thus I in B \/ {x} by A10,XBOOLE_0:def 2;
suppose
A11: a = I;
a in {a} by TARSKI:def 1;
hence I in B \/ {x} by A11,XBOOLE_0:def 2;
end;
end;
end;
P[A] from Finite(A2,A3,A4);
hence thesis;
end;
assume
A12: for A being finite non empty Subset of L st I = inf A holds I in A;
let a,b be Element of L; assume I = a"/\"b;
then I = inf {a,b} by YELLOW_0:40;
then I in {a,b} by A12;
hence thesis by TARSKI:def 2;
end;
theorem
for L be LATTICE,l be Element of L
st (uparrow l \ {l}) is Filter of L holds l is irreducible
proof
let L be LATTICE,
l be Element of L; assume
A1: (uparrow l \ {l}) is Filter of L;
set F = (uparrow l \ {l});
now let x,y be Element of L; assume
A2: l = x "/\" y & x <> l & y <> l;
then l <= x & l <= y by YELLOW_0:23;
then x in uparrow l & y in uparrow l by WAYBEL_0:18;
then x in F & y in F by A2,ZFMISC_1:64;
then consider z being Element of L such that
A3: z in F & z <= x & z <= y by A1,WAYBEL_0:def 2;
l >= z by A2,A3,YELLOW_0:23;
then l in F by A1,A3,WAYBEL_0:def 20;
hence contradiction by ZFMISC_1:64;
end;
hence thesis by Def2;
end;
theorem Th13: ::3.6, p.69
for L be LATTICE, p be Element of L, F be Filter of L st
p is_maximal_in (F`) holds p is irreducible
proof
let L be LATTICE,
p be Element of L,
F be Filter of L such that
A1: p is_maximal_in (F`);
A2: F` = [#](L) \ F by PRE_TOPC:17
.= (the carrier of L) \ F by PRE_TOPC:12;
set X = (the carrier of L)\F;
A3: p in X by A1,A2,WAYBEL_4:56;
now let x,y be Element of L; assume
A4: p = x "/\" y & x <> p & y <> p;
now assume x in F & y in F;
then consider z being Element of L such that
A5: z in F & z <= x & z <= y by WAYBEL_0:def 2;
p >= z by A4,A5,YELLOW_0:23;
then p in F by A5,WAYBEL_0:def 20;
hence contradiction by A3,XBOOLE_0:def 4;
end;
then A6: x in X or y in X by XBOOLE_0:def 4;
p <= x & p <= y by A4,YELLOW_0:23;
then p < x & p < y by A4,ORDERS_1:def 10;
hence contradiction by A1,A2,A6,WAYBEL_4:56;
end;
hence thesis by Def2;
end;
theorem Th14: ::3.7, p.69
for L be lower-bounded continuous LATTICE, x,y be Element of L st not y <= x
holds ex p be Element of L st p is irreducible & x <= p & not y <= p
proof
let L be lower-bounded continuous LATTICE,
x,y be Element of L such that
A1: not y <= x;
(for x being Element of L holds waybelow x is non empty directed) &
L is up-complete satisfying_axiom_of_approximation;
then consider u being Element of L such that
A2: u << y & not u <= x by A1,WAYBEL_3:24;
consider F be Open Filter of L such that
A3: y in F & F c= wayabove u by A2,Th8;
A4: wayabove u c= uparrow u by WAYBEL_3:11;
A5: F` = [#](L) \ F by PRE_TOPC:17
.= (the carrier of L) \ F by PRE_TOPC:12;
now assume x in F;
then x in uparrow u by A3,A4,TARSKI:def 3;
hence contradiction by A2,WAYBEL_0:18;
end;
then x in (the carrier of L)\F by XBOOLE_0:def 4;
then consider m being Element of L such that
A6: x <= m & m is_maximal_in (F`) by A5,Th9;
A7: F` = [#](L) \ F by PRE_TOPC:17
.= (the carrier of L) \ F by PRE_TOPC:12;
A8: m in (F`) by A6,WAYBEL_4:56;
A9: now assume y <= m;
then m in F by A3,WAYBEL_0:def 20;
hence contradiction by A7,A8,XBOOLE_0:def 4;
end;
take m;
thus thesis by A6,A9,Th13;
end;
begin :: Order generating sets
definition ::def 3.8, p.70
let L be non empty RelStr,
X be Subset of L;
attr X is order-generating means :Def5:
for x be Element of L holds
ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X);
end;
theorem Th15: ::3.9 (1-2), p.70
for L be up-complete lower-bounded LATTICE, X be Subset of L holds
X is order-generating iff
for l being Element of L ex Y be Subset of X st l = "/\" (Y,L)
proof
let L be up-complete lower-bounded LATTICE, X be Subset of L;
thus X is order-generating implies
for l being Element of L ex Y be Subset of X st l = "/\" (Y,L)
proof
assume A1: X is order-generating;
let l be Element of L;
for x st x in ((uparrow l) /\ X) holds
x in X by XBOOLE_0:def 3;
then reconsider Y = ((uparrow l) /\ X) as Subset of X by TARSKI:def 3;
l = "/\" (Y,L) by A1,Def5;
hence thesis;
end;
thus (for l being Element of L ex Y be Subset of X st l = "/\" (Y,L))
implies
X is order-generating
proof
assume A2: (for l being Element of L ex Y be Subset of X st l = "/\"
(Y,L));
let l be Element of L;
consider Y be Subset of X such that A3: l = "/\" (Y,L) by A2;
set S = ((uparrow l) /\ X);
thus ex_inf_of S,L by YELLOW_0:17;
now let x be Element of L; assume x in S;
then x in (uparrow l) & x in X by XBOOLE_0:def 3;
hence l <= x by WAYBEL_0:18;
end;
then A4: l is_<=_than S by LATTICE3:def 8;
for b be Element of L st b is_<=_than S holds b <= l
proof
let b be Element of L; assume A5: b is_<=_than S;
now let x be Element of L; assume A6: x in Y;
l is_<=_than Y by A3,YELLOW_0:33;
then l <= x by A6,LATTICE3:def 8;
then x in uparrow l by WAYBEL_0:18;
then x in S by A6,XBOOLE_0:def 3;
hence b <= x by A5,LATTICE3:def 8;
end;
then b is_<=_than Y by LATTICE3:def 8;
hence b <= l by A3,YELLOW_0:33;
end;
hence l = inf S by A4,YELLOW_0:33;
end;
end;
theorem ::3.9 (1-3), p.70
for L be up-complete lower-bounded LATTICE, X be Subset of L holds
X is order-generating iff
for Y be Subset of L st X c= Y & for Z be Subset of Y holds "/\"
(Z,L) in Y holds
the carrier of L = Y
proof
let L be up-complete lower-bounded LATTICE, X be Subset of L;
thus X is order-generating implies
(for Y be Subset of L st X c= Y &
for Z be Subset of Y holds "/\"(Z,L) in Y holds
the carrier of L = Y)
proof
assume A1: X is order-generating;
let Y be Subset of L; assume that
A2: X c= Y and
A3: for Z be Subset of Y holds "/\"(Z,L) in Y;
now let l1 be set; assume l1 in the carrier of L;
then reconsider l = l1 as Element of L;
A4: l = inf ((uparrow l) /\ X) by A1,Def5;
A5: (uparrow l) /\ Y c= Y by XBOOLE_1:17;
(uparrow l) /\ X c= (uparrow l) /\ Y by A2,XBOOLE_1:26;
then (uparrow l) /\ X c= Y by A5,XBOOLE_1:1;
hence l1 in Y by A3,A4;
end;
hence the carrier of L c= Y by TARSKI:def 3;
thus Y c= the carrier of L;
end;
thus (for Y be Subset of L st X c= Y &
for Z be Subset of Y holds "/\"(Z,L) in Y holds the carrier of L = Y)
implies X is order-generating
proof
assume
A6: for Y be Subset of L st
X c= Y & for Z be Subset of Y holds "/\"(Z,L) in Y holds
the carrier of L = Y;
set Y = {"/\"(Z,L) where Z is Subset of L : Z c= X};
now let x; assume x in Y;
then consider Z be Subset of L such that A7: x = "/\"(Z,L) & Z c= X;
thus x in the carrier of L by A7;
end;
then Y c= the carrier of L by TARSKI:def 3;
then reconsider Y as Subset of L;
now let x; assume A8: x in X;
then reconsider x1 = x as Element of L;
A9: {x1} c= X by A8,ZFMISC_1:37;
reconsider x2 = {x1} as Subset of L;
x1 = "/\"(x2,L) by YELLOW_0:39;
hence x in Y by A9;
end;
then
A10: X c= Y by TARSKI:def 3;
for l being Element of L ex Z be Subset of X st l = "/\" (Z,L)
proof
let l be Element of L;
for Z be Subset of Y holds "/\"(Z,L) in Y
proof
let Z be Subset of Y;
defpred P[Subset of L] means $1 c= X & "/\"($1,L) in Z;
set N = {"/\"(A,L) where A is Subset of L : P[A]};
now let x; assume A11: x in Z;
then x in Y;
then consider Z be Subset of L such that
A12: x = "/\"(Z,L) & Z c= X;
thus x in N by A11,A12;
end;
then A13: Z c= N by TARSKI:def 3;
now let x; assume x in N;
then consider S be Subset of L such that
A14: x = "/\"(S,L) & S c= X & "/\"(S,L) in Z;
thus x in Z by A14;
end;
then N c= Z by TARSKI:def 3;
then
A15: "/\"(Z,L) = "/\"(N,L) by A13,XBOOLE_0:def 10
.= "/\" (union {A where A is Subset of L : P[A]}, L)
from Inf_of_Infs;
set S = union {A where A is Subset of L : A c= X & "/\"(A,L) in Z};
now let x; assume x in S;
then consider Y be set such that
A16: x in Y and
A17: Y in {A where A is Subset of L : A c= X & "/\"
(A,L) in Z} by TARSKI:def 4;
consider A be Subset of L such that
A18: Y = A & A c= X & "/\"(A,L) in Z by A17;
thus x in the carrier of L by A16,A18;
end;
then S c= the carrier of L by TARSKI:def 3;
then reconsider S as Subset of L;
now let B be set; assume
B in {A where A is Subset of L : A c= X & "/\"(A,L) in Z};
then consider A be Subset of L such that A19: B = A & A c= X & "/\"(A,
L) in
Z;
thus B c= X by A19;
end;
then S c= X by ZFMISC_1:94;
hence "/\"(Z,L) in Y by A15;
end;
then the carrier of L = Y by A6,A10;
then l in Y;
then consider Z be Subset of L such that
A20: l = "/\" (Z,L) & Z c= X;
thus thesis by A20;
end;
hence thesis by Th15;
end;
end;
theorem Th17: ::3.9 (1-4), p.70
for L be up-complete lower-bounded LATTICE, X be Subset of L holds
X is order-generating iff
(for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st
p in X & l1 <= p & not l2 <= p)
proof
let L be up-complete lower-bounded LATTICE, X be Subset of L;
thus X is order-generating implies
(for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st
p in X & l1 <= p & not l2 <= p)
proof
assume A1: X is order-generating;
let l1,l2 be Element of L; assume A2: not l2 <= l1;
consider P be Subset of X such that A3: l1 = "/\" (P,L) by A1,Th15;
now assume for p be Element of L st p in P holds l2 <= p;
then l2 is_<=_than P by LATTICE3:def 8;
hence contradiction by A2,A3,YELLOW_0:33;
end;
then consider p be Element of L such that A4: p in P & not l2 <= p;
take p;
l1 is_<=_than P by A3,YELLOW_0:33;
hence thesis by A4,LATTICE3:def 8;
end;
thus (for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st
p in X & l1 <= p & not l2 <= p) implies X is order-generating
proof
assume
A5: (for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st
p in X & l1 <= p & not l2 <= p);
let l be Element of L;
set y = inf ((uparrow l) /\ X);
thus ex_inf_of (uparrow l) /\ X,L by YELLOW_0:17;
A6: y is_<=_than ((uparrow l) /\ X ) by YELLOW_0:33;
now assume A7: y <> l;
l is_<=_than ((uparrow l) /\ X )
proof
let b be Element of L; assume b in ((uparrow l) /\ X );
then b in (uparrow l) by XBOOLE_0:def 3;
hence thesis by WAYBEL_0:18;
end;
then l <= y by YELLOW_0:33;
then A8: not y < l by ORDERS_1:30;
now per cases by A8,ORDERS_1:def 10;
suppose not y <= l;
then consider p be Element of L such that
A9: p in X & l <= p & not y <= p by A5;
p in (uparrow l) by A9,WAYBEL_0:18;
then p in (uparrow l) /\ X by A9,XBOOLE_0:def 3;
hence contradiction by A6,A9,LATTICE3:def 8;
suppose y = l;
hence contradiction by A7;
end;
hence contradiction;
end;
hence l = y;
end;
end;
theorem Th18: ::3.10, p.70
for L be lower-bounded continuous LATTICE, X be Subset of L st X = IRR L \ {
Top L}
holds X is order-generating
proof
let L be lower-bounded continuous LATTICE, X be Subset of L; assume
A1: X = IRR L \ {Top L};
for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st
p in X & l1 <= p & not l2 <= p
proof
let x,y be Element of L; assume not y <= x;
then consider p be Element of L such that
A2: p is irreducible & x <= p & not y <= p by Th14;
A3: p <> Top L by A2,YELLOW_0:45;
p in IRR L by A2,Def4;
then p in X by A1,A3,ZFMISC_1:64;
hence thesis by A2;
end;
hence thesis by Th17;
end;
theorem Th19:
for L being lower-bounded continuous LATTICE, X,Y being Subset of L st
X is order-generating & X c= Y holds Y is order-generating
proof
let L be lower-bounded continuous LATTICE, X,Y be Subset of L; assume
A1: X is order-generating & X c= Y;
let x be Element of L;
thus ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17;
A2:ex_inf_of ((uparrow x) /\ Y),L by YELLOW_0:17;
A3:ex_inf_of ((uparrow x) /\ X),L by YELLOW_0:17;
A4:ex_inf_of (uparrow x),L by WAYBEL_0:39;
(uparrow x) /\ Y c= (uparrow x) by XBOOLE_1:17;
then inf ((uparrow x) /\ Y) >= inf (uparrow x) by A2,A4,YELLOW_0:35;
then A5: inf ((uparrow x) /\ Y) >= x by WAYBEL_0:39;
(uparrow x) /\ X c= (uparrow x) /\ Y by A1,XBOOLE_1:26;
then inf ((uparrow x) /\ X) >= inf ((uparrow x) /\ Y) by A2,A3,YELLOW_0:35;
then x >= inf ((uparrow x) /\ Y) by A1,Def5;
hence x = inf((uparrow x) /\ Y) by A5,ORDERS_1:25;
end;
begin :: Prime elements
definition ::def 3.11, p.70
let L be non empty RelStr;
let l be Element of L;
attr l is prime means :Def6:
for x,y be Element of L st x "/\" y <= l holds x <= l or y <= l;
end;
definition
let L be non empty RelStr;
func PRIME L -> Subset of L means :Def7:
for x be Element of L holds x in it iff x is prime;
existence
proof defpred P[Element of L] means $1 is prime;
consider X being Subset of L such that
A1: for x being Element of L holds x in X iff P[x] from SSubsetEx;
take X;
thus thesis by A1;
end;
uniqueness
proof
let X,Y be Subset of L; assume that
A2: for x be Element of L holds x in X iff x is prime and
A3: for x be Element of L holds x in Y iff x is prime;
thus X c= Y
proof
let x; assume A4: x in X;
then reconsider x1 = x as Element of L;
x1 is prime by A2,A4;
hence thesis by A3;
end;
thus Y c= X
proof
let x; assume A5: x in Y;
then reconsider x1 = x as Element of L;
x1 is prime by A3,A5;
hence thesis by A2;
end;
end;
end;
definition
let L be non empty RelStr;
let l be Element of L;
attr l is co-prime means :Def8:
l~ is prime;
end;
theorem Th20:
for L being upper-bounded antisymmetric non empty RelStr holds Top L is prime
proof
let L be upper-bounded antisymmetric non empty RelStr;
let x,y be Element of L; assume x "/\" y <= Top L;
thus x <= Top L or y <= Top L by YELLOW_0:45;
end;
theorem
for L being lower-bounded antisymmetric non empty RelStr holds Bottom
L is co-prime
proof
let L be lower-bounded antisymmetric non empty RelStr;
Top (L~) is prime by Th20;
hence (Bottom L)~ is prime by YELLOW_7:33;
end;
definition
let L be upper-bounded antisymmetric non empty RelStr;
cluster prime Element of L;
existence
proof
take Top L;
thus thesis by Th20;
end;
end;
theorem Th22:
for L being Semilattice, l being Element of L holds
l is prime iff
for A being finite non empty Subset of L st l >= inf A
ex a being Element of L st a in A & l >= a
proof
let L be Semilattice, l be Element of L;
thus l is prime implies
for A being finite non empty Subset of L st l >= inf A
ex a being Element of L st a in A & l >= a
proof assume
A1: for x,y being Element of L st l >= x"/\"y holds l >= x or l >= y;
let A be finite non empty Subset of L;
A2: A is finite;
defpred P[set] means $1 is non empty & l >= "/\"($1,L)
implies (ex k being Element of L st k in $1 & l >= k);
A3: P[{}];
A4: now let x,B be set such that
A5: x in A & B c= A and
A6: P[B];
thus P[B \/ {x}] proof assume
A7: B \/ {x} is non empty & l >= "/\"(B \/ {x},L);
B c= the carrier of L by A5,XBOOLE_1:1;
then reconsider C = B as finite Subset of L
by A5,FINSET_1:13;
reconsider a = x as Element of L by A5;
per cases;
suppose B = {};
then "/\"(B \/ {a},L) = a & a in B \/ {a} by TARSKI:def 1,YELLOW_0:39
;
hence ex k being Element of L st k in B \/ {x} & l >= k by A7;
suppose
A8: B <> {}; then ex_inf_of C, L & ex_inf_of {a}, L by YELLOW_0:55;
then A9: "/\"(B \/ {x},L) = (inf C)"/\"inf {a} & inf {a} = a
by YELLOW_0:39,YELLOW_2:4;
hereby per cases by A1,A7,A9;
suppose inf C <= l;
then consider b being Element of L such that
A10: b in B & b <= l by A6,A8;
b in B \/ {x} by A10,XBOOLE_0:def 2;
hence ex k being Element of L st k in B \/ {x} & l >= k by A10;
suppose
A11: a <= l;
a in {a} by TARSKI:def 1;
then a in B \/ {x} by XBOOLE_0:def 2;
hence ex k being Element of L st k in B \/ {x} & l >= k by A11;
end;
end;
end;
P[A] from Finite(A2,A3,A4);
hence thesis;
end;
assume A12: for A being finite non empty Subset of L st l >= inf A
ex a being Element of L st a in A & l >= a;
let a,b be Element of L; assume A13: a "/\" b <= l;
set A = {a,b};
inf A = a"/\"b by YELLOW_0:40;
then consider k being Element of L such that A14: k in A & l >= k by A12,A13
;
thus thesis by A14,TARSKI:def 2;
end;
theorem Th23:
for L being sup-Semilattice, x being Element of L holds
x is co-prime iff
for A being finite non empty Subset of L st x <= sup A
ex a being Element of L st a in A & x <= a
proof
let L be sup-Semilattice, x be Element of L;
thus x is co-prime implies
for A being finite non empty Subset of L st x <= sup A
ex a being Element of L st a in A & x <= a
proof
assume x is co-prime;
then A1: x~ is prime by Def8;
let A be finite non empty Subset of L; assume x <= sup A;
then A2: x~ >= (sup A)~ by LATTICE3:9;
L~ = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
then reconsider A1 = A as finite non empty Subset of L~;
A3: ex_sup_of A,L by YELLOW_0:54;
then A4: ex_inf_of A,L~ by YELLOW_7:10;
"\/"(A,L) is_>=_than A by A3,YELLOW_0:def 9;
then A5: "\/"(A,L)~ is_<=_than A by YELLOW_7:8;
now let y be Element of L~; assume y is_<=_than A;
then ~y is_>=_than A by YELLOW_7:9;
then ~y >= "\/"(A,L) by A3,YELLOW_0:def 9;
hence y <= "\/"(A,L)~ by YELLOW_7:2;
end;
then (sup A)~ = (inf A1) by A4,A5,YELLOW_0:def 10;
then consider a being Element of L~ such that A6: a in A1 & x~ >= a by A1,A2
,Th22;
take ~a;
thus thesis by A6,LATTICE3:def 7,YELLOW_7:2;
end;
thus (for A being finite non empty Subset of L st x <= sup A
ex a being Element of L st a in A & x <= a) implies x is co-prime
proof
assume A7: for A being finite non empty Subset of L st x <= sup A
ex a being Element of L st a in A & x <= a;
now let a,b be Element of L~; assume A8: a "/\" b <= x~;
set A = {~a,~b};
A9: sup A = (~a)"\/"(~b) by YELLOW_0:41;
A10: ~(a "/\" b) = (a "/\" b) by LATTICE3:def 7;
x <= ~(a "/\" b) by A8,YELLOW_7:2;
then x <= (~a)"\/"(~b) by A10,YELLOW_7:24;
then consider l being Element of L such that A11: l in A & x <= l by A7,A9;
l = ~a or l = ~b by A11,TARSKI:def 2;
hence a <= x~ or b <= x~ by A11,YELLOW_7:2;
end;
then x~ is prime by Def6;
hence thesis by Def8;
end;
end;
theorem Th24:
for L being LATTICE, l being Element of L st l is prime
holds l is irreducible
proof
let L be LATTICE, l be Element of L; assume A1: l is prime;
let x,y be Element of L; assume
A2: l = x "/\" y;
then A3: l <= x & l <= y by YELLOW_0:23;
x "/\" y <= l by A2;
then x <= l or y <= l by A1,Def6;
hence x = l or y = l by A3,ORDERS_1:25;
end;
theorem Th25: ::3.12 (1-2), p.70
for l holds
l is prime iff for x being set, f being map of L,BoolePoset {x} st
(for p be Element of L holds f.p = {} iff p <= l) holds
f is meet-preserving join-preserving
proof
let l;
thus l is prime implies
for x being set, f being map of L,BoolePoset {x} st
(for p be Element of L holds f.p = {} iff p <= l) holds
f is meet-preserving join-preserving
proof
assume A1: l is prime;
let x be set, f be map of L,BoolePoset {x}; assume
A2: for p be Element of L holds f.p = {} iff p <= l;
A3: dom f = the carrier of L & rng f c= the carrier of BoolePoset {x}
by FUNCT_2:def 1;
A4: the carrier of BoolePoset {x} = the carrier of InclPoset bool {x}
by YELLOW_1:4
.= bool {x} by YELLOW_1:1
.= { {} , {x}} by ZFMISC_1:30;
for z,y being Element of L holds f preserves_inf_of {z,y}
proof
let z,y be Element of L;
A5: f.:{z,y} = {f.z,f.y} by A3,FUNCT_1:118;
then A6: ex_inf_of {z,y},L implies ex_inf_of f.:{z,y},BoolePoset {x}
by YELLOW_0:21;
A7: now per cases by A4,TARSKI:def 2;
suppose A8: f.z = {} & f.y = {};
then z "/\" y <= z & z <= l by A2,YELLOW_0:23;
then A9: z "/\" y <= l by ORDERS_1:26;
thus f.z "/\" f.y = {} /\ {} by A8,YELLOW_1:17
.= f.(z "/\" y) by A2,A9;
suppose A10: f.z = {x} & f.y = {x};
then z "/\" y <= y & not y <= l & not z <= l by A2,YELLOW_0:23;
then not z "/\" y <= l by A1,Def6;
then A11: not f.(z "/\" y) = {} by A2;
thus f.z "/\" f.y = {x} /\ {x} by A10,YELLOW_1:17
.= f.(z "/\" y) by A4,A11,TARSKI:def 2;
suppose A12: f.z = {} & f.y = {x};
then z "/\" y <= z & z <= l by A2,YELLOW_0:23;
then A13: z "/\" y <= l by ORDERS_1:26;
thus f.z "/\" f.y = {} /\ {x} by A12,YELLOW_1:17
.= f.(z "/\" y) by A2,A13;
suppose A14: f.z = {x} & f.y = {};
then z "/\" y <= y & y <= l by A2,YELLOW_0:23;
then A15: z "/\" y <= l by ORDERS_1:26;
thus f.z "/\" f.y = {x} /\ {} by A14,YELLOW_1:17
.= f.(z "/\" y) by A2,A15;
end;
inf (f.:{z,y}) = f.z "/\" f.y by A5,YELLOW_0:40
.= f.inf {z,y} by A7,YELLOW_0:40;
hence thesis by A6,WAYBEL_0:def 30;
end;
hence f is meet-preserving by WAYBEL_0:def 34;
for z,y being Element of L holds f preserves_sup_of {z,y}
proof
let z,y be Element of L;
A16: f.:{z,y} = {f.z,f.y} by A3,FUNCT_1:118;
then A17: ex_sup_of {z,y},L implies ex_sup_of f.:{z,y},BoolePoset {x}
by YELLOW_0:20;
A18: now per cases by A4,TARSKI:def 2;
suppose A19: f.z = {} & f.y = {};
then z <= l & y <= l by A2;
then A20: z "\/" y <= l by YELLOW_0:22;
thus f.z "\/" f.y = {} \/ {} by A19,YELLOW_1:17
.= f.(z "\/" y) by A2,A20;
suppose A21: f.z = {x} & f.y = {x};
then z "\/" y >= z & not z <= l by A2,YELLOW_0:22;
then not z "\/" y <= l by ORDERS_1:26;
then A22: not f.(z "\/" y) = {} by A2;
thus f.z "\/" f.y = {x} \/ {x} by A21,YELLOW_1:17
.= f.(z "\/" y) by A4,A22,TARSKI:def 2;
suppose A23: f.z = {} & f.y = {x};
then z "\/" y >= y & not y <= l by A2,YELLOW_0:22;
then not z "\/" y <= l by ORDERS_1:26;
then A24: not f.(z "\/" y) = {} by A2;
thus f.z "\/" f.y = {} \/ {x} by A23,YELLOW_1:17
.= f.(z "\/" y) by A4,A24,TARSKI:def 2;
suppose A25: f.z = {x} & f.y = {};
then z "\/" y >= z & not z <= l by A2,YELLOW_0:22;
then not z "\/" y <= l by ORDERS_1:26;
then A26: not f.(z "\/" y) = {} by A2;
thus f.z "\/" f.y = {x} \/ {} by A25,YELLOW_1:17
.= f.(z "\/" y) by A4,A26,TARSKI:def 2;
end;
sup (f.:{z,y}) = f.z "\/" f.y by A16,YELLOW_0:41
.= f.sup {z,y} by A18,YELLOW_0:41;
hence thesis by A17,WAYBEL_0:def 31;
end;
hence f is join-preserving by WAYBEL_0:def 35;
end;
thus (for x being set, f being map of L,BoolePoset {x} st
(for p be Element of L holds f.p = {} iff p <= l) holds
f is meet-preserving join-preserving) implies l is prime
proof
assume A27: (for x being set, f being map of L,BoolePoset {x} st
(for p be Element of L holds f.p = {} iff p <= l) holds
f is meet-preserving join-preserving);
let z,y be Element of L; assume
A28: z "/\" y <= l;
consider x being set;
A29: the carrier of BoolePoset {x} = the carrier of InclPoset bool {x}
by YELLOW_1:4
.= bool {x} by YELLOW_1:1
.= { {} , {x}} by ZFMISC_1:30;
defpred P[Element of L, set] means $1 <= l iff $2 = {};
A30: for a being Element of L ex b being Element of BoolePoset {x} st P[a,b]
proof
let a be Element of L;
now per cases;
suppose A31: a <= l;
set b = {};
b in the carrier of BoolePoset {x} by A29,TARSKI:def 2;
then reconsider b as Element of BoolePoset {x};
a <= l iff b = {} by A31;
hence thesis;
suppose A32: not a <= l;
set b = {x};
b in the carrier of BoolePoset {x} by A29,TARSKI:def 2;
then reconsider b as Element of BoolePoset {x};
a <= l iff b = {} by A32;
hence thesis;
end;
hence thesis;
end;
consider f being map of L,BoolePoset {x} such that
A33: for p be Element of L holds P[p, f.p] from NonUniqExMD(A30);
dom f = the carrier of L & rng f c= the carrier of BoolePoset {x}
by FUNCT_2:def 1;
then A34: f.:{z,y} = {f.z,f.y} by FUNCT_1:118;
A35: ex_inf_of {z,y},L by YELLOW_0:21;
f is meet-preserving by A27,A33;
then A36: f preserves_inf_of {z,y} by WAYBEL_0:def 34;
A37: {} = f.(z "/\" y) by A28,A33
.= f.inf {z,y} by YELLOW_0:40
.= inf({f.z,f.y}) by A34,A35,A36,WAYBEL_0:def 30
.= f.z "/\" f.y by YELLOW_0:40
.= f.z /\ f.y by YELLOW_1:17;
now assume not f.z = {} & not f.y = {};
then f.z = {x} & f.y = {x} by A29,TARSKI:def 2;
hence contradiction by A37;
end;
hence z <= l or y <= l by A33;
end;
end;
theorem Th26: ::3.12 (1-3), p.70
for L being upper-bounded LATTICE, l being Element of L st l <> Top L holds
l is prime iff (downarrow l)` is Filter of L
proof
let L be upper-bounded LATTICE, l be Element of L;
assume A1: l <> Top L;
A2: (downarrow l)` = [#](L) \ (downarrow l) by PRE_TOPC:17
.= (the carrier of L) \ (downarrow l) by PRE_TOPC:12;
set X1 = (the carrier of L)\(downarrow l);
for x be set st x in X1 holds x in the carrier of L by XBOOLE_0:def 4;
then X1 c= the carrier of L by TARSKI:def 3;
then reconsider X = X1 as Subset of L;
thus l is prime implies (downarrow l)` is Filter of L
proof
assume A3: l is prime;
A4: now let x,y be Element of L; assume x in X & y in X;
then x in the carrier of L & not x in (downarrow l) &
y in the carrier of L & not y in (downarrow l) by XBOOLE_0:def 4;
then A5: not x <= l & not y <= l by WAYBEL_0:17;
A6: x "/\" y <= x & x "/\" y <= y by YELLOW_0:23;
now assume x "/\" y in (downarrow l);
then x "/\" y <= l by WAYBEL_0:17;
hence contradiction by A3,A5,Def6;
end;
then x "/\" y in X by XBOOLE_0:def 4;
hence ex z being Element of L st z in X & z <= x & z <= y by A6;
end;
A7: now let x,y be Element of L; assume
A8: x in X & x <= y;
then x in the carrier of L & not x in (downarrow l) by XBOOLE_0:def 4;
then not x <= l by WAYBEL_0:17;
then not y <= l by A8,ORDERS_1:26;
then not y in (downarrow l) by WAYBEL_0:17;
hence y in X by XBOOLE_0:def 4;
end;
now assume Top L in (downarrow l);
then Top L <= l by WAYBEL_0:17;
then Top L < l by A1,ORDERS_1:def 10;
then not l <= Top L by ORDERS_1:30;
hence contradiction by YELLOW_0:45;
end;
hence thesis by A2,A4,A7,WAYBEL_0:def 2,def 20,XBOOLE_0:def 4;
end;
thus (downarrow l)` is Filter of L implies l is prime
proof
assume A9: (downarrow l)` is Filter of L;
let x,y be Element of L; assume A10: x "/\" y <= l;
l <= l;
then A11: l in (downarrow l) by WAYBEL_0:17;
now assume not x <= l & not y <= l;
then not x in (downarrow l) & not y in (downarrow l) by WAYBEL_0:17;
then x in X & y in X by XBOOLE_0:def 4;
then consider z being Element of L such that
A12: z in X & z <= x & z <= y by A2,A9,WAYBEL_0:def 2;
z <= x "/\" y by A12,YELLOW_0:23;
then z <= l by A10,ORDERS_1:26;
then l in X by A2,A9,A12,WAYBEL_0:def 20;
hence contradiction by A11,XBOOLE_0:def 4;
end;
hence x <= l or y <= l;
end;
end;
theorem Th27: ::3.12 (1-4), p.70
for L being distributive LATTICE
for l being Element of L holds
l is prime iff l is irreducible
proof
let L be distributive LATTICE,l be Element of L;
thus l is prime implies l is irreducible by Th24;
thus l is irreducible implies l is prime
proof
assume A1: l is irreducible;
let x,y be Element of L; assume x "/\" y <= l;
then l = l "\/" (x "/\" y) by YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:6;
then l = l "\/" x or l = l "\/" y by A1,Def2;
hence x <= l or y <= l by YELLOW_0:24;
end;
end;
theorem Th28:
for L being distributive LATTICE holds
PRIME L = IRR L
proof
let L be distributive LATTICE;
now let l1 be set; assume A1: l1 in PRIME L;
then reconsider l = l1 as Element of PRIME L;
reconsider l as Element of L by A1;
l is prime by A1,Def7;
then l is irreducible by Th27;
hence l1 in IRR L by Def4;
end;
hence PRIME L c= IRR L by TARSKI:def 3;
now let l1 be set; assume A2: l1 in IRR L;
then reconsider l = l1 as Element of IRR L;
reconsider l as Element of L by A2;
l is irreducible by A2,Def4;
then l is prime by Th27;
hence l1 in PRIME L by Def7;
end;
hence IRR L c= PRIME L by TARSKI:def 3;
end;
theorem ::3.12 (1-5), p.70
for L being Boolean LATTICE
for l being Element of L st l <> Top L holds
l is prime iff for x be Element of L st x > l holds x = Top L
proof
let L be Boolean LATTICE,
l be Element of L; assume
A1: l <> Top L;
thus l is prime implies (for x be Element of L st x > l holds x = Top L)
proof
assume A2: l is prime;
let x be Element of L; assume A3: x > l;
consider y being Element of L such that
A4: y is_a_complement_of x by WAYBEL_1:def 24;
A5: x "\/" y = Top L & x "/\" y = Bottom L by A4,WAYBEL_1:def 23;
then x "/\" y <= l by YELLOW_0:44;
then x <= l or y <= l by A2,Def6;
then y < x by A3,ORDERS_1:32;
then y <= x by ORDERS_1:def 10;
hence thesis by A5,YELLOW_0:24;
end;
thus (for x be Element of L st x > l holds x = Top L) implies l is prime
proof
assume A6: for z be Element of L st z > l holds z = Top L;
let x,y be Element of L; assume A7: x "/\" y <= l;
assume A8: not x <= l & not y <= l;
A9: l = l "\/" (x "/\" y) by A7,YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:6;
then A10: l <= (l "\/" x) & l <= (l "\/" y) by YELLOW_0:23;
l <> (l "\/" x) by A8,YELLOW_0:24;
then l < (l "\/" x) by A10,ORDERS_1:def 10;
then A11: (l "\/" x) = Top L by A6;
l <> (l "\/" y) by A8,YELLOW_0:24;
then l < (l "\/" y) by A10,ORDERS_1:def 10;
then (l "\/" y) = Top L by A6;
hence contradiction by A1,A9,A11,YELLOW_5:2;
end;
end;
theorem ::3.12 (1-6), p.70
for L being continuous distributive lower-bounded LATTICE
for l being Element of L st l <> Top L holds
l is prime iff ex F being Open Filter of L st l is_maximal_in (F`)
proof
let L be continuous distributive lower-bounded LATTICE,
l be Element of L; assume A1: l <> Top L;
set F = (downarrow l)`;
A2: (downarrow l)` = [#](L) \ (downarrow l) by PRE_TOPC:17
.= (the carrier of L) \ (downarrow l) by PRE_TOPC:12;
thus l is prime implies ex F being Open Filter of L st l is_maximal_in (F`)
proof
assume A3: l is prime;
A4: (for x being Element of L holds waybelow x is non empty directed) &
L is up-complete satisfying_axiom_of_approximation;
now let x be Element of L; assume x in F;
then not x in (downarrow l) by A2,XBOOLE_0:def 4;
then not x <= l by WAYBEL_0:17;
then consider y be Element of L such that
A5: y << x & not y <= l by A4,WAYBEL_3:24;
not y in (downarrow l) by A5,WAYBEL_0:17;
then y in F by A2,XBOOLE_0:def 4;
hence ex y be Element of L st y in F & y << x by A5;
end;
then reconsider F as Open Filter of L by A1,A3,Def1,Th26;
take F;
l <= l;
then A6: l in (F`) by WAYBEL_0:17;
now given y being Element of L such that A7: y in (F`) & y > l;
y <= l by A7,WAYBEL_0:17;
hence contradiction by A7,ORDERS_1:30;
end;
hence l is_maximal_in (F`) by A6,WAYBEL_4:56;
end;
thus (ex F being Open Filter of L st l is_maximal_in (F`)) implies l is prime
proof
assume ex O being Open Filter of L st l is_maximal_in (O`);
then A8: l is irreducible by Th13;
now let x,y be Element of L; assume A9: x "/\" y <= l;
assume A10: not x <= l & not y <= l;
l = l "\/" (x "/\" y) by A9,YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:6;
then l = (l "\/" x) or l = (l "\/" y) by A8,Def2;
hence contradiction by A10,YELLOW_0:24;
end;
hence l is prime by Def6;
end;
end;
theorem Th31:
for L being RelStr, X being Subset of L holds
chi(X, the carrier of L) is map of L, BoolePoset {{}}
proof
let L be RelStr, X be Subset of L;
the carrier of BoolePoset {{}} = the carrier of InclPoset bool {{}}
by YELLOW_1:4
.= bool {{}} by YELLOW_1:1
.= {0,1} by CARD_5:1,ZFMISC_1:30;
hence thesis;
end;
theorem Th32:
for L being non empty RelStr, p,x being Element of L holds
chi((downarrow p)`,the carrier of L).x = {} iff x <= p
proof
let L be non empty RelStr, p,x be Element of L;
not x in (downarrow p)` iff x in downarrow p by YELLOW_6:10;
hence thesis by FUNCT_3:def 3,WAYBEL_0:17;
end;
theorem Th33:
for L being upper-bounded LATTICE, f being map of L,BoolePoset {{}},
p being prime Element of L st
chi((downarrow p)`,the carrier of L) = f holds
f is meet-preserving join-preserving
proof
let L be upper-bounded LATTICE, f be map of L,BoolePoset {{}},
p be prime Element of L; assume
chi((downarrow p)`,the carrier of L) = f;
then for x being Element of L holds f.x = {} iff x <= p by Th32;
hence thesis by Th25;
end;
theorem Th34: ::3.13, p.71
for L being complete LATTICE st PRIME L is order-generating holds
L is distributive meet-continuous
proof
let L be complete LATTICE; assume A1: PRIME L is order-generating;
set H = {chi((downarrow p)`, the carrier of L) where p is Element of L:
p is prime};
consider p' being prime Element of L;
A2: chi((downarrow p')`, the carrier of L) in H;
now let x be set; assume x in H;
then
ex p being Element of L st x = chi((downarrow p)`, the carrier of L) &
p is prime;
hence x is Function;
end;
then reconsider H as functional non empty set by A2,FRAENKEL:def 1;
A3: the carrier of BoolePoset H = the carrier of InclPoset bool H
by YELLOW_1:4
.= bool H by YELLOW_1:1;
deffunc F(set) = {f where f is Element of H: f.$1 = 1};
consider F being Function such that
A4: dom F = the carrier of L and
A5: for x being set st x in the carrier of L holds F.x = F(x) from Lambda;
rng F c= the carrier of BoolePoset H
proof
let y; assume y in rng F;
then consider x such that A6: x in dom F & y = F.x by FUNCT_1:def 5;
A7: y = {f where f is Element of H: f.x = 1} by A4,A5,A6;
y c= H
proof
let p be set; assume p in y;
then ex f be Element of H st p = f & f.x = 1 by A7;
hence thesis;
end;
hence y in the carrier of BoolePoset H by A3;
end;
then F is Function of the carrier of L,the carrier of BoolePoset H
by A4,FUNCT_2:def 1,RELSET_1:11;
then reconsider F as map of L, BoolePoset H;
A8: F is meet-preserving
proof
let x,y be Element of L;
assume ex_inf_of {x,y},L;
thus ex_inf_of F.:{x,y},BoolePoset H by YELLOW_0:17;
A9: F.:{x,y} = {F.x,F.y} by A4,FUNCT_1:118;
A10: {f where f is Element of H: f.x = 1} /\ {f where f is Element of H: f.y =
1}
c= {f where f is Element of H: f.(x "/\" y) = 1}
proof
let p be set; assume
p in ({f where f is Element of H: f.x = 1} /\
{f where f is Element of H: f.y = 1});
then A11: p in {f where f is Element of H: f.x = 1} &
p in {f where f is Element of H: f.y = 1} by XBOOLE_0:def 3;
then consider f1 be Element of H such that A12: f1 = p & f1.x = 1;
consider f2 be Element of H such that A13: f2 = p & f2.y = 1 by A11;
f1 in H;
then consider a be Element of L such that
A14: chi((downarrow a)`, the carrier of L) = f1 & a is prime;
reconsider f1 as map of L,BoolePoset {{}} by A14,Th31;
dom f1 = the carrier of L by FUNCT_2:def 1;
then A15: {f1.x,f1.y} = f1.:{x,y} by FUNCT_1:118;
for x being Element of L holds f1.x = {} iff x <= a by A14,Th32;
then f1 is meet-preserving by A14,Th25;
then f1 preserves_inf_of {x,y} & ex_inf_of {x,y}, L &
x"/\"y = inf {x,y} & (f1.x)"/\"(f1.y) = inf {f1.x,f1.y}
by WAYBEL_0:def 34,YELLOW_0:17,40;
then f1.(x "/\" y) = (f1.x)"/\"(f1.y) by A15,WAYBEL_0:def 30
.= 1 by A12,A13,YELLOW_5:2;
hence thesis by A12;
end;
A16: {f where f is Element of H: f.(x "/\" y) = 1} c=
{f where f is Element of H: f.x = 1} /\ {f where f is Element of H: f.y = 1}
proof
let p be set; assume
p in {f where f is Element of H: f.(x "/\" y) = 1};
then consider g be Element of H such that A17: g = p & g.(x "/\" y) = 1;
g in H;
then consider a be Element of L such that
A18: chi((downarrow a)`, the carrier of L) = g & a is prime;
reconsider g as map of L,BoolePoset {{}} by A18,Th31;
dom g = the carrier of L by FUNCT_2:def 1;
then A19: {g.x,g.y} = g.:{x,y} by FUNCT_1:118;
A20: 1 = Top BoolePoset {{}} by CARD_5:1,YELLOW_1:19;
A21: g.x <= Top BoolePoset {{}} & g.y <= Top BoolePoset {{}} by YELLOW_0:45;
g is meet-preserving by A18,Th33;
then g preserves_inf_of {x,y} & ex_inf_of {x,y}, L &
x"/\"y = inf {x,y} & (g.x)"/\"(g.y) = inf {g.x,g.y}
by WAYBEL_0:def 34,YELLOW_0:17,40;
then g.(x "/\" y) = (g.x)"/\"(g.y) by A19,WAYBEL_0:def 30;
then A22: g.x >= Top BoolePoset {{}} & g.y >= Top BoolePoset {{}}
by A17,A20,YELLOW_0:23;
then A23: g.x = 1 by A20,A21,ORDERS_1:25;
g.y = 1 by A20,A21,A22,ORDERS_1:25;
then p in {f where f is Element of H: f.x = 1} &
p in {f where f is Element of H: f.y = 1} by A17,A23;
hence thesis by XBOOLE_0:def 3;
end;
thus inf (F.:{x,y}) = F.x "/\" F.y by A9,YELLOW_0:40
.= (F.x) /\ (F.y) by YELLOW_1:17
.= {f where f is Element of H: f.x = 1} /\ (F.y) by A5
.= {f where f is Element of H: f.x = 1} /\
{f where f is Element of H: f.y = 1} by A5
.= {f where f is Element of H: f.(x "/\" y) = 1} by A10,A16,XBOOLE_0:
def 10
.= F.(x "/\" y) by A5
.= F.inf {x,y} by YELLOW_0:40;
end;
A24: F is join-preserving
proof
let x,y be Element of L;
assume ex_sup_of {x,y},L;
thus ex_sup_of F.:{x,y},BoolePoset H by YELLOW_0:17;
A25: F.:{x,y} = {F.x,F.y} by A4,FUNCT_1:118;
A26: {f where f is Element of H: f.x = 1} \/ {f where f is Element of H: f.y =
1}
c= {f where f is Element of H: f.(x "\/" y) = 1}
proof
let p be set; assume
A27: p in ({f where f is Element of H: f.x = 1} \/
{f where f is Element of H: f.y = 1});
per cases by A27,XBOOLE_0:def 2;
suppose p in {f where f is Element of H: f.x = 1};
then consider f1 be Element of H such that A28: f1 = p & f1.x = 1;
f1 in H;
then consider a be Element of L such that
A29: chi((downarrow a)`, the carrier of L) = f1 & a is prime;
reconsider f1 as map of L,BoolePoset {{}} by A29,Th31;
dom f1 = the carrier of L by FUNCT_2:def 1;
then A30: {f1.x,f1.y} = f1.:{x,y} by FUNCT_1:118;
A31: 1 = Top BoolePoset {{}} by CARD_5:1,YELLOW_1:19;
A32: f1.y <= Top BoolePoset {{}} by YELLOW_0:45;
for x being Element of L holds f1.x = {} iff x <= a by A29,Th32;
then f1 is join-preserving by A29,Th25;
then f1 preserves_sup_of {x,y} & ex_sup_of {x,y}, L &
x"\/"y = sup {x,y} & (f1.x)"\/"(f1.y) = sup {f1.x,f1.y}
by WAYBEL_0:def 35,YELLOW_0:17,41;
then f1.(x "\/" y) = (f1.x)"\/"(f1.y) by A30,WAYBEL_0:def 31
.= 1 by A28,A31,A32,YELLOW_0:24;
hence thesis by A28;
suppose p in {f where f is Element of H: f.y = 1};
then consider f1 be Element of H such that A33: f1 = p & f1.y = 1;
f1 in H;
then consider b be Element of L such that
A34: chi((downarrow b)`, the carrier of L) = f1 & b is prime;
reconsider f1 as map of L,BoolePoset {{}} by A34,Th31;
dom f1 = the carrier of L by FUNCT_2:def 1;
then A35: {f1.x,f1.y} = f1.:{x,y} by FUNCT_1:118;
A36: 1 = Top BoolePoset {{}} by CARD_5:1,YELLOW_1:19;
A37: f1.x <= Top BoolePoset {{}} by YELLOW_0:45;
for x being Element of L holds f1.x = {} iff x <= b by A34,Th32;
then f1 is join-preserving by A34,Th25;
then f1 preserves_sup_of {x,y} & ex_sup_of {x,y}, L &
x"\/"y = sup {x,y} & (f1.x)"\/"(f1.y) = sup {f1.x,f1.y}
by WAYBEL_0:def 35,YELLOW_0:17,41;
then f1.(x "\/" y) = (f1.y)"\/"(f1.x) by A35,WAYBEL_0:def 31
.= 1 by A33,A36,A37,YELLOW_0:24;
hence thesis by A33;
end;
A38: {f where f is Element of H: f.(x "\/" y) = 1} c=
{f where f is Element of H: f.x = 1} \/ {f where f is Element of H: f.y = 1}
proof
let p be set; assume
p in {f where f is Element of H: f.(x "\/" y) = 1};
then consider g be Element of H such that A39: g = p & g.(x "\/" y) = 1;
g in H;
then consider a be Element of L such that
A40: chi((downarrow a)`, the carrier of L) = g & a is prime;
reconsider g as map of L,BoolePoset {{}} by A40,Th31;
A41: dom g = the carrier of L & rng g c= the carrier of BoolePoset {{}}
by FUNCT_2:def 1;
A42: the carrier of BoolePoset {{}} = the carrier of InclPoset bool {{}}
by YELLOW_1:4
.= bool {{}} by YELLOW_1:1
.= { {} , {{}}} by ZFMISC_1:30;
A43: g.:{x,y} = {g.x,g.y} by A41,FUNCT_1:118;
A44: (g.x = {} or g.x = {{}}) & (g.y = {} or g.y = {{}}) by A42,TARSKI:def 2;
A45: 1 = Top BoolePoset {{}} by CARD_5:1,YELLOW_1:19;
g is join-preserving by A40,Th33;
then A46: g preserves_sup_of {x,y} & ex_sup_of {x,y}, L &
x"\/"y = sup {x,y} & (g.x)"\/"(g.y) = sup {g.x,g.y}
by WAYBEL_0:def 35,YELLOW_0:17,41;
now assume g.x = {} & g.y = {};
then (g.x)"\/"(g.y) = {} \/ {} by YELLOW_1:17
.= 0;
hence contradiction by A39,A43,A46,WAYBEL_0:def 31;
end;
then g.x = Top BoolePoset {{}} or g.y = Top BoolePoset {{}}
by A44,YELLOW_1:19;
then p in {f where f is Element of H: f.x = 1} or
p in {f where f is Element of H: f.y = 1} by A39,A45;
hence thesis by XBOOLE_0:def 2;
end;
thus sup (F.:{x,y}) = F.x "\/" F.y by A25,YELLOW_0:41
.= (F.x) \/ (F.y) by YELLOW_1:17
.= {f where f is Element of H: f.x = 1} \/ (F.y) by A5
.= {f where f is Element of H: f.x = 1} \/
{f where f is Element of H: f.y = 1} by A5
.= {f where f is Element of H: f.(x "\/" y) = 1} by A26,A38,XBOOLE_0:
def 10
.= F.(x "\/" y) by A5
.= F.sup {x,y} by YELLOW_0:41;
end;
A47: F is one-to-one
proof
let x1,x2 be set; assume A48: x1 in dom F & x2 in
dom F & F.x1 = F.x2;
then reconsider l1 = x1 as Element of L by A4;
reconsider l2 = x2 as Element of L by A4,A48;
now assume A49: l1 <> l2;
A50: F.l1 = {f where f is Element of H: f.l1 = 1} by A5;
A51: F.l2 = {f where f is Element of H: f.l2 = 1} by A5;
per cases by A49,ORDERS_1:25;
suppose not l1 <= l2;
then consider p be Element of L such that
A52: p in PRIME L & l2 <= p & not l1 <= p by A1,Th17;
set CH = chi((downarrow p)`,the carrier of L);
p is prime by A52,Def7;
then CH in H;
then reconsider CH as Element of H;
A53: dom CH = the carrier of L & rng CH c= {0,1} by FUNCT_2:def 1,RELSET_1:12;
then CH.l1 in rng CH by FUNCT_1:def 5;
then A54: CH.l1 = 0 or CH.l1 = 1 by A53,TARSKI:def 2;
now assume CH in F.l2;
then ex f be Element of H st f = CH & f.l2 = 1 by A51;
hence contradiction by A52,Th32;
end;
hence contradiction by A48,A50,A52,A54,Th32;
suppose not l2 <= l1;
then consider p be Element of L such that
A55: p in PRIME L & l1 <= p & not l2 <= p by A1,Th17;
set CH = chi((downarrow p)`,the carrier of L);
p is prime by A55,Def7;
then CH in H;
then reconsider CH as Element of H;
A56: dom CH = the carrier of L & rng CH c= {0,1} by FUNCT_2:def 1,RELSET_1:12;
then CH.l2 in rng CH by FUNCT_1:def 5;
then A57: CH.l2 = 0 or CH.l2 = 1 by A56,TARSKI:def 2;
now assume CH in F.l1;
then ex f be Element of H st f = CH & f.l1 = 1 by A50;
hence contradiction by A55,Th32;
end;
hence contradiction by A48,A51,A55,A57,Th32;
end;
hence thesis;
end;
hence L is distributive by A8,A24,Th3;
F is sups-preserving
proof
let X be Subset of L;
F preserves_sup_of X
proof
assume ex_sup_of X,L;
thus ex_sup_of (F.:X),BoolePoset H by YELLOW_0:17;
A58: F.(sup X) = {g where g is Element of H: g.(sup X) = 1} by A5;
A59: sup (F.:X) c= F.(sup X)
proof
let a be set; assume a in sup (F.:X);
then a in union (F.:X) by YELLOW_1:21;
then consider Y be set such that
A60: a in Y & Y in (F.:X) by TARSKI:def 4;
consider z be set such that
A61: z in dom F & z in X & Y = F.z by A60,FUNCT_1:def 12;
reconsider z as Element of L by A61;
F.z = {f where f is Element of H: f.z = 1} by A5;
then consider f be Element of H such that
A62: a = f & f.z = 1 by A60,A61;
f in H;
then consider p be Element of L such that
A63: f = chi((downarrow p)`, the carrier of L) & p is prime;
A64: dom f = the carrier of L & rng f c= {0,1}
by A63,FUNCT_2:def 1,RELSET_1:12;
then f.(sup X) in rng f by FUNCT_1:def 5;
then A65: f.(sup X) = 0 or f.(sup X) = 1 by A64,TARSKI:def 2;
now assume f.(sup X) = 0;
then A66: sup X <= p by A63,Th32;
sup X is_>=_than X by YELLOW_0:32;
then z <= sup X by A61,LATTICE3:def 9;
then z <= p by A66,ORDERS_1:26;
hence contradiction by A62,A63,Th32;
end;
hence a in F.(sup X) by A58,A62,A65;
end;
F.(sup X) c= sup (F.:X)
proof
let a be set; assume a in F.(sup X);
then consider f be Element of H such that A67: a = f & f.(sup X) = 1
by A58;
f in H;
then consider p be Element of L such that
A68: f = chi((downarrow p)`, the carrier of L) & p is prime;
A69: not sup X <= p by A67,A68,Th32;
now assume for l be Element of L st l in X holds l <= p;
then X is_<=_than p by LATTICE3:def 9;
hence contradiction by A69,YELLOW_0:32;
end;
then consider l be Element of L such that
A70: l in X & not l <= p;
A71: dom f = the carrier of L & rng f c= {0,1}
by A68,FUNCT_2:def 1,RELSET_1:12;
then f.l in rng f by FUNCT_1:def 5;
then f.l = 0 or f.l = 1 by A71,TARSKI:def 2;
then f in {g where g is Element of H: g.l = 1} by A68,A70,Th32;
then A72: f in F.l by A5;
(F.l) in (F.:X) by A4,A70,FUNCT_1:def 12;
then a in union (F.:X) by A67,A72,TARSKI:def 4;
hence a in sup (F.:X) by YELLOW_1:21;
end;
hence sup (F.:X) = F.(sup X) by A59,XBOOLE_0:def 10;
end;
hence thesis;
end;
hence L is meet-continuous by A8,A47,Th4;
end;
theorem Th35: ::3.14 (1-3), p.71
for L being lower-bounded continuous LATTICE holds
L is distributive iff PRIME L is order-generating
proof
let L be lower-bounded continuous LATTICE;
thus L is distributive implies PRIME L is order-generating
proof
assume L is distributive;
then A1: PRIME L = IRR L by Th28;
A2: IRR L \ {Top L} c= IRR L by XBOOLE_1:36;
IRR L \ {Top L} is order-generating by Th18;
hence thesis by A1,A2,Th19;
end;
thus PRIME L is order-generating implies L is distributive by Th34;
end;
theorem ::3.14 (1-2), p.71
for L being lower-bounded continuous LATTICE holds
L is distributive iff L is Heyting
proof
let L be lower-bounded continuous LATTICE;
thus L is distributive implies L is Heyting
proof
assume L is distributive;
then PRIME L is order-generating by Th35;
then L is distributive meet-continuous by Th34;
hence thesis by WAYBEL_2:56;
end;
thus L is Heyting implies L is distributive by WAYBEL_1:69;
end;
theorem Th37:
for L being continuous complete LATTICE st
for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime
for l being Element of L holds l = "\/"((waybelow l) /\ PRIME(L opp), L)
proof
let L be continuous complete LATTICE; assume
A1: for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime;
let l be Element of L;
defpred P[set,set] means $2 c= PRIME L~ & $1 = "\/"($2,L);
A2: for e be set st e in the carrier of L ex u be set st P[e,u]
proof
let e be set; assume e in the carrier of L;
then reconsider l = e as Element of L;
consider X being Subset of L such that A3: l = sup X &
for x being Element of L st x in X holds x is co-prime by A1;
now let p1 be set; assume A4: p1 in X;
then reconsider p = p1 as Element of L;
p is co-prime by A3,A4;
then A5: p~ is prime by Def8;
p = p~ by LATTICE3:def 6;
hence p1 in PRIME L~ by A5,Def7;
end;
then X c= PRIME L~ by TARSKI:def 3;
hence thesis by A3;
end;
consider f being Function such that
A6: dom f = the carrier of L and
A7: for e be set st e in the carrier of L holds P[e, f.e]
from NonUniqFuncEx(A2);
A8:l = sup waybelow l by WAYBEL_3:def 5;
A9: waybelow l c= {sup X where X is Subset of L :
X in rng f & sup X in waybelow l}
proof
let e be set; assume A10: e in waybelow l;
then A11: e = "\/"((f.e),L) & e is Element of L by A7;
A12: f.e in rng f by A6,A10,FUNCT_1:def 5;
A13: L~= RelStr(#the carrier of L,(the InternalRel of L)~#)
by LATTICE3:def 5;
f.e c= PRIME L~ by A7,A10;
then f.e c= the carrier of L~ by XBOOLE_1:1;
then f.e is Subset of L by A13;
hence thesis by A10,A11,A12;
end;
defpred P[Subset of L] means $1 in rng f & sup $1 in waybelow l;
{sup X where X is Subset of L : P[X] } c= waybelow l
proof
let e be set; assume
e in {sup X where X is Subset of L : X in rng f & sup X in
waybelow l};
then consider X be Subset of L such that
A14: e = sup X & X in rng f & sup X in waybelow l;
thus thesis by A14;
end;
then
A15:l = "\/"({sup X where X is Subset of L : P[X]}, L) by A8,A9,XBOOLE_0:def 10
.= "\/"(union {X where X is Subset of L : P[X]}, L) from Sup_of_Sups;
set Z = union {X where X is Subset of L : X in rng f & sup X in waybelow l};
A16: ex_sup_of Z,L by YELLOW_0:17;
A17: ex_sup_of ((waybelow l) /\ PRIME(L~)),L by YELLOW_0:17;
A18: ex_sup_of (waybelow l),L by YELLOW_0:17;
Z c= (waybelow l) /\ PRIME(L~)
proof
let e be set; assume e in Z;
then consider Y be set such that
A19: e in Y & Y in {X where X is Subset of L : X in rng f & sup X in
waybelow l}
by TARSKI:def 4;
consider X be Subset of L such that
A20: Y = X & X in rng f & sup X in waybelow l by A19;
consider r be set such that A21: r in dom f & X = f.r by A20,FUNCT_1:def 5;
A22: X c= PRIME(L~) by A6,A7,A21;
reconsider e1 = e as Element of L by A19,A20;
e1 <= sup X by A19,A20,YELLOW_2:24;
then e in waybelow l by A20,WAYBEL_0:def 19;
hence thesis by A19,A20,A22,XBOOLE_0:def 3;
end;
then A23:l <= "\/"((waybelow l) /\ PRIME(L~),L) by A15,A16,A17,YELLOW_0:34;
(waybelow l) /\ PRIME(L~) c= waybelow l by XBOOLE_1:17;
then "\/"((waybelow l) /\
PRIME(L~),L) <= "\/"(waybelow l,L) by A17,A18,YELLOW_0:34
;
hence l = "\/"((waybelow l) /\ PRIME(L~), L) by A8,A23,ORDERS_1:25;
end;
Lm2: ::3.15 (1->2)
for L being continuous complete LATTICE st
for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime
holds L is completely-distributive
proof
let L be continuous complete LATTICE such that
A1: for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime;
thus L is complete;
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K,L;
A2: Inf Sups F >= Sup Infs Frege F by WAYBEL_5:16;
set l = Inf Sups F;
set X = (waybelow l) /\ PRIME(L~);
A3: X c= waybelow l by XBOOLE_1:17;
then X c= the carrier of L by XBOOLE_1:1;
then reconsider X as Subset of L;
A4: Inf Sups F = sup X by A1,Th37;
A5: dom F = J by PBOOLE:def 3;
A6: for x being Element of L st x in X holds x is co-prime
proof
let x be Element of L; assume x in X;
then A7: x in PRIME(L~) by XBOOLE_0:def 3;
x = x~ by LATTICE3:def 6;
then x~ is prime by A7,Def7;
hence x is co-prime by Def8;
end;
A8: inf rng Sups F = Inf Sups F by YELLOW_2:def 6;
X is_<=_than Sup Infs Frege F
proof
let p be Element of L; assume A9: p in X;
defpred P[set,set] means
$2 in K.$1 & [p,(F.$1).$2] in the InternalRel of L;
A10: for j being set st j in J ex k being set st P[j,k]
proof
let j1 be set; assume j1 in J;
then reconsider j = j1 as Element of J;
A11: p << l by A3,A9,WAYBEL_3:7;
dom (Sups F) = J by A5,FUNCT_2:def 1;
then A12: (Sups F).j in rng Sups F by FUNCT_1:def 5;
Sup (F.j) = (Sups F).j by A5,WAYBEL_5:def 1;
then A13: l <= Sup (F.j) by A8,A12,YELLOW_2:24;
Sup (F.j) = sup rng (F.j) by YELLOW_2:def 5;
then consider A being finite Subset of L such that
A14: A c= rng (F.j) & p <= sup A by A11,A13,WAYBEL_3:18;
consider k be Element of K.j;
A c= A \/ {F.j.k} &
ex_sup_of A,L & ex_sup_of (A \/ {F.j.k}),L by XBOOLE_1:7,YELLOW_0:17
;
then sup A <= sup (A \/ {F.j.k}) by YELLOW_0:34;
then A15: p <= sup (A \/ {F.j.k}) by A14,ORDERS_1:26;
p is co-prime by A6,A9;
then consider a be Element of L such that
A16: a in (A \/ {F.j.k}) & p <= a by A15,Th23;
per cases by A16,XBOOLE_0:def 2;
suppose a in A;
then consider k1 be set such that
A17: k1 in dom (F.j) & a = F.j.k1 by A14,FUNCT_1:def 5;
reconsider k1 as Element of K.j by A17,FUNCT_2:def 1;
[p,(F.j).k1] in the InternalRel of L by A16,A17,ORDERS_1:def 9;
hence thesis;
suppose a in {F.j.k};
then a = F.j.k by TARSKI:def 1;
then [p,(F.j).k] in the InternalRel of L by A16,ORDERS_1:def 9;
hence thesis;
end;
consider f1 being Function such that
A18: dom f1 = J and
A19: for j being set st j in J holds P[j, f1.j] from NonUniqFuncEx(A10);
now let g be set; assume A20: g in dom f1;
F.g is Function;
then g in F"SubFuncs rng F by A5,A18,A20,FUNCT_6:28;
hence g in dom doms F by FUNCT_6:def 2;
end;
then A21: dom f1 c= dom doms F by TARSKI:def 3;
now let g be set; assume g in dom doms F;
then g in F"SubFuncs rng F by FUNCT_6:def 2;
hence g in dom f1 by A5,A18,FUNCT_6:28;
end;
then A22: dom doms F c= dom f1 by TARSKI:def 3;
then A23: dom f1 = dom doms F by A21,XBOOLE_0:def 10;
A24: for b be set st b in dom doms F holds f1.b in (doms F).b
proof
let b be set; assume A25: b in dom doms F;
then A26: F.b is Function of K.b, the carrier of L by A18,A22,WAYBEL_5:6;
(doms F).b = dom (F.b) by A5,A18,A22,A25,FUNCT_6:31
.= K.b by A26,FUNCT_2:def 1;
hence f1.b in (doms F).b by A18,A19,A22,A25;
end;
then A27: f1 in product doms F by A23,CARD_3:18;
reconsider f = f1 as Element of product doms F by A23,A24,CARD_3:18;
reconsider F1 = F as Function-yielding Function;
A28: (Frege F1).f1 = F1..f1 by A27,PRALG_2:def 8;
p is_<=_than rng ((Frege F).f)
proof
let b be Element of L; assume b in rng ((Frege F).f);
then consider a be set such that
A29: a in dom ((Frege F).f) & b = ((Frege F).f).a by FUNCT_1:def 5;
reconsider a as Element of J by A5,A28,A29,PRALG_1:def 18;
f in dom Frege F & a in dom F by A5,A27,PBOOLE:def 3;
then ((Frege F).f).a = (F.a).(f1.a) by WAYBEL_5:9;
then [p,((Frege F).f).a] in the InternalRel of L by A19;
hence p <= b by A29,ORDERS_1:def 9;
end;
then p <= inf rng ((Frege F).f) by YELLOW_0:33;
then A30: p <= Inf((Frege F).f) by YELLOW_2:def 6;
reconsider D = product doms F as non empty set by A23,A24,CARD_3:18;
reconsider f2 = f as Element of D;
reconsider P= D --> J as ManySortedSet of D;
reconsider R = Frege F as DoubleIndexedSet of P, L;
Inf(R.f2) in rng Infs (R) by WAYBEL_5:14;
then Inf((Frege F).f) <= sup rng Infs Frege F by YELLOW_2:24;
then Inf((Frege F).f) <= Sup Infs Frege F by YELLOW_2:def 5;
hence thesis by A30,ORDERS_1:26;
end;
then sup X <= Sup Infs Frege F by YELLOW_0:32;
hence Inf Sups F = Sup Infs Frege F by A2,A4,ORDERS_1:25;
end;
Lm3: ::3.15 (2->3)
for L being completely-distributive complete LATTICE holds
L is distributive continuous & L~ is continuous
proof
let L be completely-distributive complete LATTICE;
L~ is completely-distributive by YELLOW_7:51;
hence thesis by WAYBEL_5:24;
end;
Lm4: ::3.15 (3->1)
for L being complete LATTICE st
L is distributive continuous & L~ is continuous holds
for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime
proof
let L be complete LATTICE; assume that
A1: L is distributive continuous and
A2: L~ is continuous;
let l be Element of L;
reconsider L as distributive continuous complete LATTICE by A1;
l = l~ by LATTICE3:def 6;
then reconsider l1 = l as Element of L~;
PRIME L~ is order-generating by A2,Th35;
then consider Y be Subset of (PRIME L~) such that
A3:l1 = "/\" (Y,L~) by Th15;
A4: L~= RelStr(#the carrier of L,(the InternalRel of L)~#)
by LATTICE3:def 5;
Y c= the carrier of L~ by XBOOLE_1:1;
then reconsider Y as Subset of L by A4;
A5:for x being Element of L st x in Y holds x is co-prime
proof
let x be Element of L; assume A6: x in Y;
x = x~ by LATTICE3:def 6;
then x~ is prime by A6,Def7;
hence thesis by Def8;
end;
ex_sup_of Y,L by YELLOW_0:17;
then "\/"(Y,L) = "/\"(Y,L~) by YELLOW_7:12;
hence thesis by A3,A5;
end;
theorem ::3.15 (2-1), p.72
for L being complete LATTICE holds
L is completely-distributive iff
L is continuous &
for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime
proof
let L be complete LATTICE;
thus L is completely-distributive implies
L is continuous &
for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime
proof
assume L is completely-distributive;
then reconsider L as completely-distributive LATTICE;
L is distributive continuous & L~ is continuous by Lm3;
hence thesis by Lm4;
end;
thus L is continuous &
(for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime) implies
L is completely-distributive by Lm2;
end;
theorem ::3.15 (2-3), p.72
for L being complete LATTICE holds
L is completely-distributive iff
L is distributive continuous & L opp is continuous
proof
let L be complete LATTICE;
thus L is completely-distributive implies
L is distributive continuous & L~ is continuous by Lm3;
assume A1: L is distributive continuous & L~ is continuous;
then reconsider L as distributive continuous LATTICE;
for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime by A1,Lm4;
hence thesis by Lm2;
end;