:: The Scott Topology, Part II
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received August 27, 1997
:: Copyright (c) 1997 Association of Mizar Users
environ
vocabulary WAYBEL14, WAYBEL11, WAYBEL_9, ORDERS_A, TOPCON, RELATION, SFAMILY,
WAYBEL_0, CARDINAL, LATTOP_2, REL_REL, ONOP_1, QUANTALE, BOOLE, BORSUK,
FAM_OP, LOCSP, RCOMP, SUB_OP, REAL_1, YELLOW_0, TOP1, GRAPH, YELLOW_6,
FUNC, WAYBEL_5, FUNC_REL, WAYBEL_3, CANTOR, WAYBEL_2, YELLOW_1, WAYBEL_6,
NT_LAT, FILTER, LATTICES, TMAP_1, YELLOW_8, TSP_1, TOP2, OPPCAT,
WAYBEL_8;
constructors CARD_2, NAT_1, DOMAIN_1, TOPS_1, TOPS_2, TMAP_1, CANTOR_1,
T_0TOPSP, YELLOW_4, YELLOW_8, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_6,
WAYBEL_8, WAYBEL11, SUBSET_1;
requirements ARYTM, BOOLE, SUBSET;
notation TARSKI, BOOLE, ZFMISC_1, NAT_1, SETFAM_1, FINSET_1, DOMAIN_1,
RELAT_1, FUNCT_1, FUNCT_2, ORDERS_1, LATTICE3, CARD_1, SUBSET_1,
STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, BORSUK_1, TMAP_1, CANTOR_1,
TSP_1, COMPTS_1, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4,
YELLOW_6, YELLOW_7, YELLOW_8, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3,
WAYBEL_5, WAYBEL_6, WAYBEL_8, WAYBEL_9, WAYBEL11;
clusters SUBSET_1, STRUCT_0, FINSET_1, LATTICE3, BORSUK_1, PRE_TOPC, CANTOR_1,
YELLOW_1, YELLOW_4, YELLOW_6, YELLOW_8, WAYBEL_0, WAYBEL_3, WAYBEL_6,
WAYBEL_7, WAYBEL_8, WAYBEL11, RELSET_1;
definitions TARSKI, BOOLE, WAYBEL_0, WAYBEL_6, TMAP_1, YELLOW_8, COMPTS_1,
WAYBEL_3, WAYBEL_1, WAYBEL_8, TOPS_2;
theorems STRUCT_0, TARSKI, BOOLE, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1,
FUNCT_1, FUNCT_2, SETFAM_1, REAL_1, LATTICE3, CARD_2, ORDERS_1, PRE_TOPC,
TOPS_1, TOPS_2, BORSUK_1, TMAP_1, CONNSP_2, COMPTS_1, CANTOR_1, YELLOW_0,
YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4, YELLOW_6, YELLOW_7, YELLOW_8,
WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_8, WAYBEL11,
WAYBEL12;
schemes NAT_1;
begin :: Preliminaries
theorem Th1:
for X being set, F being finite Subset-Family of X
ex G being finite Subset-Family of X st G c= F & union G = union F &
for g being Subset of X st g î G holds not g c= union (G\{g})
proof let X be set;
defpred P[Nat] means for F being finite Subset-Family of X st card F = $1
ex G being finite Subset-Family of X st G c= F & union G = union F &
for g being Subset of X st g î G holds not g c= union (G\{g});
A1: now let F be finite Subset-Family of X; assume
A2: card F = 0;
take G = F;
thus G c= F;
thus union G = union F;
F is empty by A2, CARD_2:59;
hence for g being Subset of X st g î G holds not g c= union (G\{g});
end;
A3: now let n be Nat; assume
A4: P[n];
let F be finite Subset-Family of X; assume
A5: card F = n+1;
per cases;
suppose ex g being Subset of X st g î F & g c= union (F\{g}); then
consider g being Subset of X such that
A6: g î F & g c= union (F\{g});
set FF = F\{g};
reconsider FF as finite Subset-Family of X;
{g} c= F by A6, ZFMISC_1:37; then
A7: F = FF U {g} by BOOLE:54;
g î {g} by TARSKI:def 1; then
not g î FF by BOOLE:def 4; then
card (FF U {g}) = card FF + 1 by CARD_2:54; then
card FF = n by A5, A7, REAL_1:10; then
consider G being finite Subset-Family of X such that
A8: G c= FF and
A9: union G = union FF and
A10: for g being Subset of X st g î G holds not g c= union (G\{g})
by A4;
take G;
A11: FF c= F by A7, BOOLE:31;
hence G c= F by A8, BOOLE:29;
A12: union FF c= union F by A11, ZFMISC_1:95;
union F c= union FF proof let x be set; assume x î union F; then
consider X being set such that
A13: x î X & X î F by TARSKI:def 4;
A14: X î FF or X î {g} by A13, A7, BOOLE:def 2;
per cases by A14;
suppose X î FF; then X c= union FF by ZFMISC_1:92;
hence thesis by A13;
suppose X î {g}; then X = g by TARSKI:def 1;
hence thesis by A13, A6;
end; then
union FF = union F by A12, BOOLE:def 8;
hence union G = union F by A9;
thus for g being Subset of X st g î G holds not g c= union (G\{g})
by A10;
suppose
A15: not ex g being Subset of X st g î F & g c= union (F\{g});
take G = F;
thus G c= F;
thus union G = union F;
thus for g being Subset of X st g î G holds not g c= union (G\{g})
by A15;
end;
A16: for n being Nat holds P[n] from Ind(A1, A3);
let F be finite Subset-Family of X;
card F = card F;
hence thesis by A16;
end;
Lm1:
for S being 1-sorted, X, Y being Subset of the carrier of S
holds X c= -Y iff Y c= -X
proof let S be 1-sorted, X, Y be Subset of the carrier of S;
Y = --Y by PRE_TOPC:20;
hence X c= -Y iff Y c= -X by PRE_TOPC:19;
end;
theorem Th2:
for S being 1-sorted, X being Subset of the carrier of S
holds -X = the carrier of S iff X is empty
proof let S be 1-sorted, X be Subset of the carrier of S;
hereby assume -X = the carrier of S; then
-X = ê(the carrier of S) by SUBSET_1:def 4; then
--X = -ê(the carrier of S); then
X = -ê(the carrier of S) by PRE_TOPC:20; then
X = -êS by PRE_TOPC:def 3; then X = íS by TOPS_1:8;
hence X is empty;
end; assume X is empty; then X = íS; then -X = êS by PRE_TOPC:27;
hence -X = the carrier of S by PRE_TOPC:12;
end;
theorem Th3:
for R being antisymmetric with_infima transitive non empty RelStr,
x, y being Element of R
holds downarrow (xÚ¿y) = (downarrow x) ï downarrow y
proof let R be antisymmetric with_infima transitive non empty RelStr,
x,y be Element of R;
now let z be set;
hereby assume
A1: z î downarrow (xÚ¿y); then
reconsider z' = z as Element of R by STRUCT_0:def 2;
A2: z' ó (xÚ¿y) by A1, WAYBEL_0:17;
(xÚ¿y) ó x & (xÚ¿y) ó y by YELLOW_0:23; then
z' ó x & z' ó y by A2, YELLOW_0:def 2; then
z' î downarrow x & z' î downarrow y by WAYBEL_0:17;
hence z î (downarrow x) ï downarrow y by BOOLE:def 3;
end; assume z î (downarrow x) ï downarrow y; then
A3: z î (downarrow x) & z î downarrow y by BOOLE:def 3; then
reconsider z' = z as Element of R by STRUCT_0:def 2;
z' ó x & z' ó y by A3, WAYBEL_0:17; then
xÚ¿y ò z' by YELLOW_0:23;
hence z î downarrow (xÚ¿y) by WAYBEL_0:17;
end;
hence downarrow (xÚ¿y) = (downarrow x) ï downarrow y by TARSKI:2;
end;
theorem
for R being antisymmetric with_suprema transitive non empty RelStr,
x, y being Element of R
holds uparrow (xÀÙy) = (uparrow x) ï uparrow y
proof let R be antisymmetric with_suprema transitive non empty RelStr,
x,y be Element of R;
now let z be set;
hereby assume
A1: z î uparrow (xÀÙy); then
reconsider z' = z as Element of R by STRUCT_0:def 2;
A2: z' ò (xÀÙy) by A1, WAYBEL_0:18;
(xÀÙy) ò x & (xÀÙy) ò y by YELLOW_0:22; then
z' ò x & z' ò y by A2, YELLOW_0:def 2; then
z' î uparrow x & z' î uparrow y by WAYBEL_0:18;
hence z î (uparrow x) ï uparrow y by BOOLE:def 3;
end; assume z î (uparrow x) ï uparrow y; then
A3: z î (uparrow x) & z î uparrow y by BOOLE:def 3; then
reconsider z' = z as Element of R by STRUCT_0:def 2;
z' ò x & z' ò y by A3, WAYBEL_0:18; then
xÀÙy ó z' by YELLOW_0:22;
hence z î uparrow (xÀÙy) by WAYBEL_0:18;
end;
hence uparrow (xÀÙy) = (uparrow x) ï uparrow y by TARSKI:2;
end;
theorem Th5:
for L being complete antisymmetric (non empty RelStr),
X being lower Subset of L
st sup X î X holds X = downarrow sup X
proof let L be complete antisymmetric (non empty RelStr),
X be lower Subset of L such that
A1: sup X î X;
X is_ó_than sup X by YELLOW_0:32;
hence X c= downarrow sup X by YELLOW_2:1;
thus downarrow sup X c= X by A1, WAYBEL11:6;
end;
theorem
for L being complete antisymmetric (non empty RelStr),
X being upper Subset of L
st inf X î X holds X = uparrow inf X
proof let L be complete antisymmetric (non empty RelStr),
X be upper Subset of L such that
A1: inf X î X;
X is_ò_than inf X by YELLOW_0:33;
hence X c= uparrow inf X by YELLOW_2:2;
thus uparrow inf X c= X by A1, WAYBEL11:42;
end;
theorem Th7:
for R being non empty reflexive transitive RelStr, x, y being Element of R
holds x << y iff uparrow y c= wayabove x
proof let R be non empty reflexive transitive RelStr,
x, y be Element of R;
hereby assume
A1: x << y;
thus uparrow y c= wayabove x proof let z be set; assume
A2: z î uparrow y; then
reconsider z' = z as Element of R by STRUCT_0:def 2;
y ó z' by A2, WAYBEL_0:18; then
x << z' by A1, WAYBEL_3:2;
hence z î wayabove x by WAYBEL_3:8;
end;
end; assume
A3: uparrow y c= wayabove x; y ó y; then
y î uparrow y by WAYBEL_0:18; then
y î wayabove x by A3;
hence x << y by WAYBEL_3:8;
end;
theorem
for R being non empty reflexive transitive RelStr, x, y being Element of R
holds x << y iff downarrow x c= waybelow y
proof let R be non empty reflexive transitive RelStr,
x, y be Element of R;
hereby assume
A1: x << y;
thus downarrow x c= waybelow y proof let z be set; assume
A2: z î downarrow x; then
reconsider z' = z as Element of R by STRUCT_0:def 2;
z' ó x by A2, WAYBEL_0:17; then
z' << y by A1, WAYBEL_3:2;
hence z î waybelow y by WAYBEL_3:7;
end;
end; assume
A3: downarrow x c= waybelow y; x ó x; then
x î downarrow x by WAYBEL_0:17; then
x î waybelow y by A3;
hence x << y by WAYBEL_3:7;
end;
theorem Th9:
for R being complete reflexive antisymmetric (non empty RelStr),
x being Element of R
holds sup waybelow x ó x & x ó inf wayabove x
proof let R be complete reflexive antisymmetric (non empty RelStr),
x be Element of R;
x is_ò_than waybelow x by WAYBEL_3:9;
hence sup waybelow x ó x by YELLOW_0:32;
x is_ó_than wayabove x by WAYBEL_3:10;
hence thesis by YELLOW_0:33;
end;
theorem Th10:
for L being lower-bounded antisymmetric non empty RelStr
holds uparrow ÁL = the carrier of L
proof let L be lower-bounded antisymmetric non empty RelStr;
set uL = uparrow ÁL, cL = the carrier of L;
now let x be set;
thus x î uL implies x î cL;
assume x î cL; then
reconsider x' = x as Element of L by STRUCT_0:def 2;
ÁL ó x' by YELLOW_0:44;
hence x î uL by WAYBEL_0:18;
end;
hence uparrow ÁL = the carrier of L by TARSKI:2;
end;
theorem
for L being upper-bounded antisymmetric non empty RelStr
holds downarrow ÂL = the carrier of L
proof let L be upper-bounded antisymmetric non empty RelStr;
set uL = downarrow ÂL, cL = the carrier of L;
now let x be set;
thus x î uL implies x î cL;
assume x î cL; then
reconsider x' = x as Element of L by STRUCT_0:def 2;
ÂL ò x' by YELLOW_0:45;
hence x î uL by WAYBEL_0:17;
end;
hence thesis by TARSKI:2;
end;
theorem Th12:
for P being with_suprema Poset, x, y being Element of P
holds (wayabove x)ÀÙ(wayabove y) c= uparrow (xÀÙy)
proof let R be with_suprema Poset, x, y be Element of R;
wayabove x c= uparrow x & wayabove y c= uparrow y by WAYBEL_3:11; then
A1: (wayabove x)ÀÙ(wayabove y) c= (uparrow x)ÀÙ(uparrow y)
by YELLOW_4:21;
A2: uparrow x = uparrow {x} & uparrow y = uparrow {y} by WAYBEL_0:def 18;
A3: {x}ÀÙ{y} = {xÀÙy} by YELLOW_4:19;
A4: uparrow {xÀÙy} = uparrow (xÀÙy) by WAYBEL_0:def 18;
(uparrow x)ÀÙ(uparrow y) c=
uparrow ((uparrow x)ÀÙ(uparrow y)) by WAYBEL_0:16; then
(uparrow x)ÀÙ(uparrow y) c= uparrow (xÀÙy)
by A2, A3, A4, YELLOW_4:35;
hence thesis by A1, BOOLE:29;
end;
theorem
for P being with_infima Poset, x, y being Element of P
holds (waybelow x)Ú¿(waybelow y) c= downarrow (xÚ¿y)
proof let R be with_infima Poset, x, y be Element of R;
waybelow x c= downarrow x & waybelow y c= downarrow y by WAYBEL_3:11; then
A1: (waybelow x)Ú¿(waybelow y) c= (downarrow x)Ú¿(downarrow y)
by YELLOW_4:48;
A2: downarrow x=downarrow {x} & downarrow y=downarrow {y} by WAYBEL_0:def 17;
A3: {x}Ú¿{y} = {xÚ¿y} by YELLOW_4:46;
A4: downarrow {xÚ¿y} = downarrow (xÚ¿y) by WAYBEL_0:def 17;
(downarrow x)Ú¿(downarrow y) c=
downarrow ((downarrow x)Ú¿(downarrow y)) by WAYBEL_0:16; then
(downarrow x)Ú¿(downarrow y) c= downarrow (xÚ¿y)
by A2, A3, A4, YELLOW_4:62;
hence thesis by A1, BOOLE:29;
end;
theorem Th14:
for R being with_suprema non empty Poset, l being Element of R holds
l is co-prime iff
for x,y be Element of R st l ó x ÀÙ y holds l ó x or l ó y
proof let R be with_suprema non empty Poset, l be Element of R;
hereby assume l is co-prime; then
A1: l~ is prime by WAYBEL_6:def 8;
let x, y be Element of R; assume
l ó x ÀÙ y; then
A2: (x ÀÙ y)~ ó l~ by LATTICE3:9;
(x ÀÙ y)~ = xÀÙy by LATTICE3:def 6
.= (x~)Ú¿(y~) by YELLOW_7:23; then
(x~)Ú¿(y~) ó l~ by A2; then
x~ ó l~ or y~ ó l~ by A1, WAYBEL_6:def 6;
hence l ó x or l ó y by LATTICE3:9;
end; assume
A3: for x,y be Element of R st l ó x ÀÙ y holds l ó x or l ó y;
let x,y be Element of R~; assume
A4: x Ú¿ y ó l~;
~(x Ú¿ y) = x Ú¿ y by LATTICE3:def 7
.= ~xÀÙ~y by YELLOW_7:24; then
l ó ~xÀÙ~y by A4, YELLOW_7:2; then
l ó ~x or l ó ~y by A3;
hence x ó l~ or y ó l~ by YELLOW_7:2;
end;
theorem Th15:
for P being complete (non empty Poset),
V being non empty Subset of P
holds downarrow inf V = meet {downarrow u where u is Element of P : u î V}
proof let P be complete (non empty Poset),
V be non empty Subset of P;
set F = {downarrow u where u is Element of P : u î V};
consider u being set such that
A1: u î V by ZFMISC_1:136;
reconsider u as Element of P by A1, STRUCT_0:def 2;
downarrow u î F by A1; then
A2: F is non empty;
F c= bool the carrier of P proof let X be set; assume X î F; then
consider u being Element of P such that
A3: X = downarrow u & u î V;
thus X î bool the carrier of P by A3;
end; then
reconsider F as Subset-Family of P by STRUCT_0:def 4;
now let x be set;
hereby assume
A4: x î downarrow inf V; then
reconsider d = x as Element of P by STRUCT_0:def 2;
A5: d ó inf V by A4, WAYBEL_0:17;
now let Y be set; assume Y î F; then
consider u being Element of P such that
A6: Y = downarrow u & u î V;
inf V is_ó_than V by YELLOW_0:33; then
inf V ó u by A6, LATTICE3:def 8; then
d ó u by A5, ORDERS_1:26;
hence x î Y by A6, WAYBEL_0:17;
end;
hence x î meet F by A2, SETFAM_1:def 1;
end; assume
A7: x î meet F; then
reconsider d = x as Element of P by STRUCT_0:def 2;
now let b be Element of P; assume b î V; then
downarrow b î F; then
d î downarrow b by A7, SETFAM_1:def 1;
hence d ó b by WAYBEL_0:17;
end; then
d is_ó_than V by LATTICE3:def 8; then
d ó inf V by YELLOW_0:33;
hence x î downarrow inf V by WAYBEL_0:17;
end;
hence thesis by TARSKI:2;
end;
theorem
for P being complete (non empty Poset),
V being non empty Subset of P
holds uparrow sup V = meet {uparrow u where u is Element of P : u î V}
proof let P be complete (non empty Poset),
V be non empty Subset of P;
set F = {uparrow u where u is Element of P : u î V};
consider u being set such that
A1: u î V by ZFMISC_1:136;
reconsider u as Element of P by A1, STRUCT_0:def 2;
uparrow u î F by A1; then
A2: F is non empty;
F c= bool the carrier of P proof let X be set; assume X î F; then
consider u being Element of P such that
A3: X = uparrow u & u î V;
thus X î bool the carrier of P by A3;
end; then
reconsider F as Subset-Family of P by STRUCT_0:def 4;
now let x be set;
hereby assume
A4: x î uparrow sup V; then
reconsider d = x as Element of P by STRUCT_0:def 2;
A5: d ò sup V by A4, WAYBEL_0:18;
now let Y be set; assume Y î F; then
consider u being Element of P such that
A6: Y = uparrow u & u î V;
sup V is_ò_than V by YELLOW_0:32; then
sup V ò u by A6, LATTICE3:def 9; then
d ò u by A5, ORDERS_1:26;
hence x î Y by A6, WAYBEL_0:18;
end;
hence x î meet F by A2, SETFAM_1:def 1;
end; assume
A7: x î meet F; then
reconsider d = x as Element of P by STRUCT_0:def 2;
now let b be Element of P; assume b î V; then
uparrow b î F; then
d î uparrow b by A7, SETFAM_1:def 1;
hence d ò b by WAYBEL_0:18;
end; then
d is_ò_than V by LATTICE3:def 9; then
d ò sup V by YELLOW_0:32;
hence x î uparrow sup V by WAYBEL_0:18;
end;
hence thesis by TARSKI:2;
end;
definition let L be sup-Semilattice,
x be Element of L;
cluster compactbelow x -> directed;
coherence proof set cX = compactbelow x;
let xx, yy be Element of L such that
A1: xx î cX & yy î cX;
set z = xx ÀÙ yy;
take z;
xx ó x & yy ó x by A1, WAYBEL_8:4; then
A2: z ó x by YELLOW_0:22;
A3: xx ó z & yy ó z by YELLOW_0:22;
xx is compact & yy is compact by A1, WAYBEL_8:4; then
xx << xx & yy << yy by WAYBEL_3:def 2; then
xx << z & yy << z by A3, WAYBEL_3:2; then
z << z by WAYBEL_3:3; then
z is compact by WAYBEL_3:def 2;
hence z î cX by A2, WAYBEL_8:4;
thus xx ó z & yy ó z by YELLOW_0:22;
end;
end;
theorem Th17:
:: See a parenthetical remark in the middle of p. 106.
:: This fact is needed in the proof of II-1.11(ii), p. 105.
for T being non empty TopSpace, S being irreducible Subset of T,
V being Element of InclPoset the topology of T
st V = -S holds V is prime
proof let T be non empty TopSpace, S being irreducible Subset of T,
V be Element of InclPoset the topology of T such that
A1: V =-S;
A2: the carrier of InclPoset the topology of T = the topology of T
by YELLOW_1:1;
A3: S is closed by YELLOW_8:def 4;
set sL = the topology of T;
let X, Y be Element of InclPoset sL; assume
A4: X Ú¿ Y ó V;
X î sL & Y î sL by A2; then
X is Subset of the carrier of T & Y is Subset of the carrier of T; then
reconsider X' = X, Y' = Y as Subset of T by STRUCT_0:def 3;
X' is open & Y' is open by A2, PRE_TOPC:def 5; then
-X' is closed & -Y' is closed by TOPS_1:30; then
A5: (-X')ïS is closed & (-Y')ïS is closed by A3, TOPS_1:35;
X' ï Y' î sL by A2, PRE_TOPC:8; then
X ï Y = X Ú¿ Y by YELLOW_1:9; then
X ï Y c= V by A4, YELLOW_1:3; then
X'ïY' c= -S by A1; then
S c= -(X'ïY') by Lm1; then
S c= -X' U -Y' by WAYBEL12:6; then
S = (-X' U -Y')ïS by BOOLE:42; then
S = (-X')ïS U (-Y')ïS by BOOLE:70; then
S = (-X')ïS or S = (-Y')ïS by A5, YELLOW_8:def 4; then
S c= -X' or S c= -Y' by BOOLE:37; then
X c= V or Y c= V by A1, Lm1;
hence X ó V or Y ó V by YELLOW_1:3;
end;
theorem Th18:
for T being non empty TopSpace,
x, y be Element of InclPoset the topology of T
holds x ÀÙ y = x U y & x Ú¿ y = x ï y
proof let T be non empty TopSpace,
x, y be Element of InclPoset the topology of T;
set IPt = InclPoset the topology of T;
A1: the carrier of IPt = the topology of T by YELLOW_1:1;
then A2: x î the topology of T & y î the topology of T; then
reconsider x' = x, y' = y as Subset of T by STRUCT_0:def 3;
x' is open & y' is open by A2, PRE_TOPC:def 5; then
x' U y' is open by TOPS_1:37; then
x' U y' î the topology of T by PRE_TOPC:def 5;
hence x ÀÙ y = x U y by YELLOW_1:8;
x' ï y' î the topology of T by A1, PRE_TOPC:8;
hence x Ú¿ y = x ï y by YELLOW_1:9;
end;
theorem Th19:
for T being non empty TopSpace,
V being Element of InclPoset the topology of T
holds V is prime iff
for X, Y being Element of InclPoset the topology of T
st XïY c= V holds X c= V or Y c= V
proof let T be non empty TopSpace,
V be Element of InclPoset the topology of T;
hereby assume
A1: V is prime;
let X, Y be Element of InclPoset the topology of T; assume
A2: XïY c= V;
XïY = XÚ¿Y by Th18; then
XÚ¿Y ó V by A2, YELLOW_1:3; then
X ó V or Y ó V by A1, WAYBEL_6:def 6;
hence X c= V or Y c= V by YELLOW_1:3;
end; assume
A3: for X, Y being Element of InclPoset the topology of T
st XïY c= V holds X c= V or Y c= V;
let X, Y be Element of InclPoset the topology of T such that
A4: X Ú¿ Y ó V;
XïY = XÚ¿Y by Th18; then
XïY c= V by A4, YELLOW_1:3; then
X c= V or Y c= V by A3;
hence X ó V or Y ó V by YELLOW_1:3;
end;
theorem
for T being non empty TopSpace,
V being Element of InclPoset the topology of T
holds V is co-prime iff
for X, Y being Element of InclPoset the topology of T
st V c= X U Y holds V c= X or V c= Y
proof let T be non empty TopSpace,
V be Element of InclPoset the topology of T;
hereby assume
A1: V is co-prime;
let X, Y be Element of InclPoset the topology of T; assume
A2: V c= X U Y;
X U Y = X ÀÙ Y by Th18; then
V ó XÀÙY by A2, YELLOW_1:3; then
V ó X or V ó Y by A1, Th14;
hence V c= X or V c= Y by YELLOW_1:3;
end; assume
A3: for X, Y being Element of InclPoset the topology of T
st V c= X U Y holds V c= X or V c= Y;
now let X, Y be Element of InclPoset the topology of T such that
A4: V ó XÀÙY;
X U Y = XÀÙY by Th18; then
V c= X U Y by A4, YELLOW_1:3; then
V c= X or V c= Y by A3;
hence V ó X or V ó Y by YELLOW_1:3;
end;
hence thesis by Th14;
end;
definition let T be non empty TopSpace;
cluster InclPoset the topology of T -> distributive;
coherence proof set IPt = InclPoset the topology of T;
let x, y, z be Element of IPt;
thus x Ú¿ (y ÀÙ z)
= x ï (y ÀÙ z) by Th18
.= x ï (y U z) by Th18
.= x ï y U x ï z by BOOLE:70
.= (x Ú¿ y) U x ï z by Th18
.= (x Ú¿ y) U (x Ú¿ z) by Th18
.= (x Ú¿ y) ÀÙ (x Ú¿ z) by Th18;
end;
end;
theorem Th21:
for T being non empty TopSpace, L being TopLattice,
t being Point of T, l being Point of L,
X being Subset-Family of L
st the TopStruct of T = the TopStruct of L & t = l & X is basis of l
holds X is basis of t
proof let T be non empty TopSpace, L be TopLattice,
t be Point of T, l be Point of L,
X be Subset-Family of L;
assume
A1: the TopStruct of T = the TopStruct of L; assume
A2: t = l; assume
A3: X c= the topology of L; assume
A4: l î Intersect X; assume
A5: for S being Subset of L st S is open & l î S
ex V being Subset of L st V î X & V c= S;
X is Subset-Family of the carrier of T by A1; then
reconsider X' = X as Subset-Family of T by STRUCT_0:def 4;
now let S be Subset of T such that
A6: S is open and
A7: t î S;
reconsider S' = S as Subset of L by A1, STRUCT_0:def 3;
S î the topology of T by A6, PRE_TOPC:def 5; then
S' is open by A1, PRE_TOPC:def 5; then
consider V being Subset of L such that
A8: V î X & V c= S' by A2, A7, A5;
reconsider V as Subset of T by A1, STRUCT_0:def 3;
take V;
thus V î X' & V c= S by A8;
end;
hence X is basis of t by A1, A2, A3, A4, YELLOW_8:def 2;
end;
theorem Th22:
for L being TopLattice, x being Element of L
st for X being Subset of L st X is open holds X is upper
holds uparrow x is compact
proof let L be TopLattice, x be Element of L such that
A1: for X being Subset of L st X is open holds X is upper;
set P = uparrow x;
let F be Subset-Family of L such that
A2: F is_a_cover_of P and
A3: F is open;
x ó x; then
A4: x î P by WAYBEL_0:18;
P c= union F by A2, COMPTS_1:def 1; then x î union F by A4; then
consider Y being set such that
A5: x î Y & Y î F by TARSKI:def 4;
reconsider Y as Subset of L by A5, STRUCT_0:def 3;
Y is open by A3, A5, TOPS_2:def 1; then
Y is upper by A1; then
A6: P c= Y by A5, WAYBEL11:42;
reconsider G = {Y} as Subset-Family of L by STRUCT_0:def 4;
take G;
thus G c= F by A5, ZFMISC_1:37;
thus P c= union G by A6, ZFMISC_1:31;
thus G is finite;
end;
begin :: Scott topology, continuation of WAYBEl11
reserve L for complete Scott TopLattice,
x for Element of L,
X, Y for Subset of L,
V, W for Element of InclPoset sigma L,
VV for Subset of InclPoset sigma L;
definition let L be complete LATTICE;
cluster sigma L -> non empty;
coherence proof
sigma L = the topology of ConvergenceSpace Scott-Convergence L
by WAYBEL11:def 12;
hence thesis;
end;
end;
theorem Th23:
sigma L = the topology of L
proof
A1: sigma L = the topology of ConvergenceSpace Scott-Convergence L
by WAYBEL11:def 12;
the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
hence sigma L = the topology of L by A1;
end;
theorem Th24:
X î sigma L iff X is open
proof sigma L =the topology of L by Th23; hence thesis by PRE_TOPC:def 5;end;
Lm2:
for L being complete Scott TopLattice,
V being filtered Subset of L,
F being Subset-Family of L, CF being Subset of InclPoset sigma L
st F = {downarrow u where u is Element of L : u î V} &
CF = COMPLEMENT F
holds CF is directed
proof let L be complete Scott TopLattice,
V be filtered Subset of L,
F be Subset-Family of L, CF be Subset of InclPoset sigma L such that
A1: F = {downarrow u where u is Element of L : u î V} and
A2: CF = COMPLEMENT F;
set IPs = InclPoset sigma L;
A3: sigma L = the topology of L by Th23;
then A4: the carrier of IPs = the topology of L by YELLOW_1:1;
let x, y be Element of IPs such that
A5: x î CF & y î CF;
x î sigma L & y î sigma L by A3, A4; then
reconsider x' = x, y' = y as Subset of L by STRUCT_0:def 3;
-x' î F by A2, A5, YELLOW_8:13; then
consider ux being Element of L such that
A6: -x' = downarrow ux & ux î V by A1;
-y' î F by A2, A5, YELLOW_8:13; then
consider uy being Element of L such that
A7: -y' = downarrow uy & uy î V by A1;
consider uz being Element of L such that
A8: uz î V & uz ó ux & uz ó uy by A6, A7, WAYBEL_0:def 2;
-downarrow uz is open by WAYBEL11:12; then
-downarrow uz î the topology of L by PRE_TOPC:def 5; then
reconsider z = -downarrow uz as Element of IPs by A4, STRUCT_0:def 2;
take z;
downarrow uz î F by A1, A8;
hence z î CF by A2, YELLOW_8:14;
downarrow uz c= downarrow ux & downarrow uz c= downarrow uy
by A8, WAYBEL_0:21; then
-downarrow ux c= -downarrow uz & -downarrow uy c= -downarrow uz
by PRE_TOPC:19; then
x c= z & y c= z by A6, A7, PRE_TOPC:20;
hence x ó z & y ó z by YELLOW_1:3;
end;
theorem Th25:
for X being filtered Subset of L
st VV = {-downarrow x : x î X} holds VV is directed
proof let V be filtered Subset of L; assume
A1: VV = {-downarrow x : x î V};
set F = {downarrow u where u is Element of L : u î V};
F c= bool the carrier of L proof let x be set; assume x î F; then
ex u being Element of L st x = downarrow u & u î V;
hence thesis;
end; then
reconsider F as Subset-Family of L by STRUCT_0:def 4;
VV c= bool the carrier of L proof let x be set; assume x î VV; then
ex u being Element of L st x = -downarrow u & u î V by A1;
hence thesis;
end; then
reconsider VV as Subset-Family of L by STRUCT_0:def 4;
now let x be set;
hereby assume x î VV; then
consider u being Element of L such that
A2: x = -downarrow u & u î V by A1;
downarrow u î F by A2;
hence x î COMPLEMENT F by A2, YELLOW_8:14;
end; assume
A3: x î COMPLEMENT F; then
reconsider X = x as Subset of the carrier of L;
-X î F by A3, YELLOW_8:13; then
consider u being Element of L such that
A4: -X = downarrow u & u î V;
X = -downarrow u by A4, PRE_TOPC:20;
hence x î VV by A4, A1;
end; then
VV = COMPLEMENT F by TARSKI:2;
hence thesis by Lm2;
end;
theorem Th26:
X is open & x î X implies inf X << x
proof assume that
A1: X is open and
A2: x î X;
A3: X is upper property(S) by A1, WAYBEL11:15;
now let D be non empty directed Subset of L; assume
x ó sup D;
then sup D î X by A2, A3, WAYBEL_0:def 20; then
consider y being Element of L such that
A4: y î D and
A5: for x being Element of L st x î D & x ò y holds x î X
by A3, WAYBEL11:def 3;
take y;
thus y î D by A4;
A6: inf X is_ó_than X by YELLOW_0:33;
y ó y; then
y î X by A4, A5;
hence inf X ó y by A6, LATTICE3:def 8;
end;
hence inf X << x by WAYBEL_3:def 1;
end;
:: p. 105
definition let R be non empty reflexive RelStr, f be map of [:R, R:], R;
attr f is jointly_Scott-continuous means
:Def1: for T being non empty TopSpace
st the TopStruct of T = ConvergenceSpace Scott-Convergence R
ex ft being map of [:T, T:], T st ft = f & ft is continuous;
end;
theorem Th27: :: Proposition 1.11 (i) p. 105
V = X implies (V is co-prime iff X is filtered upper)
proof assume
A1: V = X;
A2: sigma L = the topology of ConvergenceSpace Scott-Convergence L
by WAYBEL11:def 12;
A3: the carrier of InclPoset sigma L = sigma L by YELLOW_1:1;
then A4: X is upper by A1, A2, WAYBEL11:31;
the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
then A5: sigma L = the topology of L by A2;
A6: InclPoset the topology of L is with_suprema with_infima antisymmetric;
hereby assume
A7: V is co-prime;
thus X is filtered proof let v, w be Element of L such that
A8: v î X & w î X;
-downarrow w is open & -downarrow v is open by WAYBEL11:12; then
-downarrow w î sigma L & -downarrow v î sigma L
by A5, PRE_TOPC:def 5; then
reconsider mdw = -downarrow w, mdv = -downarrow v as
Element of InclPoset sigma L by A3, STRUCT_0:def 2;
v ó v & w ó w; then
v î downarrow v & w î downarrow w by WAYBEL_0:17; then
not v î -downarrow v & not w î -downarrow w by YELLOW_6:10; then
not V c= -downarrow v & not V c= -downarrow w by A1, A8;then
not V ó mdv & not V ó mdw by YELLOW_1:3; then
not V ó mdv ÀÙ mdw by A7, A5, A6, Th14; then
A9: not V c= mdv ÀÙ mdw by YELLOW_1:3;
mdv U mdw c= mdv ÀÙ mdw by A5, A6, YELLOW_1:6; then
A10: not V c= mdv U mdw by A9, BOOLE:29;
mdv U mdw = -((downarrow v) ï downarrow w) by WAYBEL12:6
.= -downarrow(vÚ¿w) by Th3; then
Xï--downarrow(vÚ¿w) <> í by A1, A10, TOPS_1:20; then
Xïdownarrow(vÚ¿w) <> í by PRE_TOPC:20; then
consider zz being set such that
A11: zz î Xïdownarrow(vÚ¿w) by ZFMISC_1:136;
A12: zz î X & zz î downarrow(vÚ¿w) by A11, BOOLE:def 3;
then reconsider zz as Element of L by STRUCT_0:def 2;
A13: zz ó vÚ¿w by A12, WAYBEL_0:17;
take z = vÚ¿w;
thus z î X by A13, A12, A4, WAYBEL_0:def 20;
thus z ó v & z ó w by YELLOW_0:23;
end;
thus X is upper by A4;
end; assume
A14: X is filtered upper; assume not V is co-prime; then
consider Xx, Y being Element of InclPoset sigma L such that
A15: V ó Xx ÀÙ Y & not V ó Xx & not V ó Y by A5, A6, Th14;
Xx î sigma L & Y î sigma L by A3; then
Xx is Subset of the carrier of L & Y is Subset of the carrier of L; then
reconsider Xx' = Xx, Y' = Y as Subset of L by STRUCT_0:def 3;
A16: Xx' is open & Y' is open by A3, A5, PRE_TOPC:def 5; then
Xx' U Y' is open by TOPS_1:37; then
Xx U Y î sigma L by A5, PRE_TOPC:def 5; then
Xx U Y = Xx ÀÙ Y by YELLOW_1:8; then
A17: V c= Xx U Y by A15, YELLOW_1:3;
A18: not V c= Xx & not V c= Y by A15, YELLOW_1:3;
then consider v being set such that
A19: v î V & not v î Xx by TARSKI:def 3;
consider w being set such that
A20: w î V & not w î Y by A18, TARSKI:def 3;
A21: Xx' is upper & Y' is upper by A16, WAYBEL11:def 4;
reconsider v, w as Element of L by A1, A19, A20, STRUCT_0:def 2;
A22: now assume vÚ¿w î Xx' U Y'; then
A23: vÚ¿w î Xx' or vÚ¿w î Y' by BOOLE:def 2;
per cases by A23;
suppose A24: vÚ¿w î Xx';
vÚ¿w ó v by YELLOW_0:23;
hence contradiction by A24, A19, A21, WAYBEL_0:def 20;
suppose A25: vÚ¿w î Y';
vÚ¿w ó w by YELLOW_0:23;
hence contradiction by A25, A20, A21, WAYBEL_0:def 20;
end;
vÚ¿w î X by A1, A19, A20, A14, WAYBEL_0:41;
hence contradiction by A1, A22, A17;
end;
theorem :: Proposition 1.11 (ii) p. 105
(V = X & ex x st X = -downarrow x) implies V is prime & V <> the carrier of L
proof assume
A1: V = X;
A2: sigma L = the topology of ConvergenceSpace Scott-Convergence L
by WAYBEL11:def 12;
the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
then A3: sigma L = the topology of L by A2;
given u being Element of L such that
A4: X = -downarrow u;
A5: Cl {u} = downarrow u by WAYBEL11:9;
Cl {u} is irreducible by YELLOW_8:26;
hence V is prime by A1, A4, A5, A3, Th17;
assume V = the carrier of L; then downarrow u = í by A1, A4, Th2;
hence contradiction;
end;
theorem Th29: :: Proposition 1.11 (iii) p. 105
V = X & sup_op L is jointly_Scott-continuous & V is prime &
V <> the carrier of L
implies ex x st X = -downarrow x
proof assume that
A1: V = X and
A2: sup_op L is jointly_Scott-continuous and
A3: V is prime and
A4: V <> the carrier of L;
A5: sigma L = the topology of ConvergenceSpace Scott-Convergence L
by WAYBEL11:def 12;
A6: the carrier of InclPoset sigma L = sigma L by YELLOW_1:1;
A7: the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
then A8: sigma L = the topology of L by A5;
then A9: X is open by A1, A6, PRE_TOPC:def 5;
set A = -X;
A is closed by A9, TOPS_1:30; then
A10: A is directly_closed lower by WAYBEL11:7;
take u = sup A;
A11: A is directed proof given a, b being Element of L such that
A12: a î A & b î A and
A13: for z being Element of L holds not (z î A & a ó z & b ó z);
a ó aÀÙb & b ó aÀÙb by YELLOW_0:22; then
not aÀÙb î A by A13; then
A14: aÀÙb î X by YELLOW_6:10;
set LxL = [:L qua non empty TopSpace, L:];
consider Tsup being map of LxL, L such that
A15: Tsup = sup_op L & Tsup is continuous by A2, A7, Def1;
A16: Tsup"X is open by A15, A9, TOPS_2:55;
A17: the carrier of LxL = [:the carrier of L, the carrier of L:]
by BORSUK_1:def 5; then
A18: [a,b] î the carrier of LxL by ZFMISC_1:def 1;
Tsup. [a,b] = aÀÙb by A15, WAYBEL_2:def 5; then
A19: [a,b] î Tsup"X by A14, A18, FUNCT_2:106;
consider AA being Subset-Family of the carrier of LxL such that
A20:Tsup"X = union AA and
A21:for e being set st e î AA ex X1 being Subset of L,
Y1 being Subset of L st
e = [:X1,Y1:] & X1 is open & Y1 is open by A16, BORSUK_1:45;
consider AAe being set such that
A22: [a,b] î AAe & AAe î AA by A20, A19, TARSKI:def 4;
consider Va, Vb being Subset of L such that
A23: AAe = [:Va, Vb:] & Va is open & Vb is open by A22, A21;
reconsider Va' = Va, Vb' = Vb as Subset of L;
now let x be set;
hereby assume x î TsupøAAe; then
consider cd being set such that
A24: cd î the carrier of LxL and
A25: cd î AAe & Tsup.cd = x by FUNCT_2:43;
consider c, d being Element of the carrier of L such that
A26: cd = [c,d] by A24, A17, DOMAIN_1:9;
reconsider c, d as Element of L by STRUCT_0:def 2;
A27: x = cÀÙd by A25, A26, A15, WAYBEL_2:def 5;
A28: c ó cÀÙd & d ó cÀÙd by YELLOW_0:22;
A29: Va' is upper & Vb' is upper by A23, WAYBEL11:def 4;
c î Va & d î Vb by A25, A26, A23, ZFMISC_1:106; then
x î Va & x î Vb by A29, A28, A27, WAYBEL_0:def 20;
hence x î VaïVb by BOOLE:def 3;
end; assume x î VaïVb; then
A30: x î Va & x î Vb by BOOLE:def 3;
then reconsider c = x as Element of L by STRUCT_0:def 2;
A31: [c,c] î AAe by A30, A23, ZFMISC_1:106;
A32: [c,c] î the carrier of LxL by A17, ZFMISC_1:106;
c ó c; then
c = cÀÙc by YELLOW_0:24; then
A33: c = Tsup. [c,c] by A15, WAYBEL_2:def 5;
the carrier of L is non empty;
hence x î TsupøAAe by A31, A32, A33, FUNCT_2:43;
end; then
A34: TsupøAAe = VaïVb by TARSKI:2;
AAe c= union AA by A22, ZFMISC_1:92; then
TsupøAAe c= Tsupø(Tsup"X) & Tsupø(Tsup"X) c= X
by A20, RELAT_1:156, FUNCT_1:145; then
A35: TsupøAAe c= X by BOOLE:29;
Va î sigma L & Vb î sigma L by A23, A8, PRE_TOPC:def 5; then
Va is Element of InclPoset the topology of L &
Vb is Element of InclPoset the topology of L by A6, A8, STRUCT_0:def 2; then
A36: Va c= X or Vb c= X by A1, A3, A8, A35, A34, Th19;
a î Va & b î Vb by A22, A23, ZFMISC_1:106; then
a î X or b î X by A36;
hence contradiction by A12, YELLOW_6:10;
end;
now assume A = í; then -A = the carrier of L by Th2;
hence contradiction by A1, A4, PRE_TOPC:20;
end; then
u î A by A11, A10, WAYBEL11:def 2; then
A = downarrow u by A10, Th5;
hence X = -downarrow u by PRE_TOPC:20;
end;
theorem Th30: :: Proposition 1.11 (iv) p. 105
L is continuous implies sup_op L is jointly_Scott-continuous
proof assume
A1: L is continuous;
let T be non empty TopSpace such that
A2: the TopStruct of T = ConvergenceSpace Scott-Convergence L;
A3: the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
A4: the carrier of T = the carrier of L by A2, YELLOW_6:def 27;
set Tsup = sup_op L;
the carrier of L is non empty; then
A5: dom Tsup = the carrier of [:L, L:] by FUNCT_2:def 1;
A6: the carrier of [:T, T:] = [:the carrier of T, the carrier of T:]
by BORSUK_1:43; then
A7: the carrier of [:T,T:] = the carrier of [:L,L:] by A4,YELLOW_3:def 2;then
A8: dom Tsup = the carrier of [:T, T:] by A5;
rng Tsup c= the carrier of T by A4; then
Tsup is Function of the carrier of [:T, T:], the carrier of T
by A8, FUNCT_2:1; then
reconsider Tsup as map of [:T, T:], T by PRE_TOPC:def 11;
take Tsup;
thus Tsup = sup_op L;
for x being Point of [:T, T:] holds Tsup is_continuous_at x
proof let ab be Point of [:T, T:];
consider a, b being Point of T such that
A9: ab = [a,b] by A6, DOMAIN_1:9;
let G be a_neighborhood of Tsup.ab;
reconsider Tsab = Tsup.ab as Point of T;
A10: Tsab î Int G by CONNSP_2:def 1;
A11: Int G is open by TOPS_1:51;
reconsider Tsab' = Tsab as Element of L by A4, STRUCT_0:def 2;
set basab = { wayabove q where q is Element of L: q << Tsab' };
reconsider basab as basis of Tsab' by A1, WAYBEL11:44;
basab is basis of Tsab by A2, A3, Th21; then
consider V being Subset of T such that
A12: V î basab & V c= Int G by A10, A11, YELLOW_8: def 2;
consider u being Element of L such that
A13: V = wayabove u & u << Tsab' by A12;
reconsider a' = a, b' = b as Element of L by A4, STRUCT_0:def 2;
reconsider Lc = L as continuous complete Scott TopLattice by A1;
Lc = L;then
A14: a' = sup waybelow a' & b' = sup waybelow b' by WAYBEL_3:def 5;
A15: Tsab' = a'ÀÙb' by A9, WAYBEL_2:def 5
.= sup ((waybelow a')ÀÙ(waybelow b')) by A14, WAYBEL_2:4;
set D1 = waybelow a', D2 = waybelow b';
set D = D1ÀÙD2;
consider xy being Element of L such that
A16: xy î D & u << xy by A13, A15, A1, WAYBEL_4:50;
D = { x ÀÙ y where x, y is Element of L : x î D1 & y î D2 }
by YELLOW_4:def 3; then
consider x, y being Element of L such that
A17: xy = xÀÙy & x î D1 & y î D2 by A16;
A18: x << a' & y << b' by A17, WAYBEL_3:7;
A19: wayabove x is open & wayabove y is open by A1, WAYBEL11:36;
A20: a' î wayabove x & b' î wayabove y by A18, WAYBEL_3:8;
set H = [:wayabove x, wayabove y:];
reconsider wx = wayabove x, wy = wayabove y as Subset of T
by A4, STRUCT_0:def 3;
wayabove x î the topology of L & wayabove y î the topology of L
by A19, PRE_TOPC:def 5; then
wx î the topology of T & wy î the topology of T by A2, A3; then
A21: wx is open & wy is open by PRE_TOPC:def 5;
reconsider H as Subset of [:T, T:] by A7, STRUCT_0:def 3;
H is open by A21, BORSUK_1:46; then
A22: H = Int H by TOPS_1:55;
[a',b'] î H by A20, ZFMISC_1:106; then
reconsider H as a_neighborhood of ab by A9, A22, CONNSP_2:def 1;
take H;
A23: TsupøH = (wayabove x)ÀÙ(wayabove y) by WAYBEL_2:35;
A24: (wayabove x)ÀÙ(wayabove y) c= uparrow (xÀÙy) by Th12;
uparrow (xÀÙy) c= wayabove u by A16, A17, Th7; then
A25: TsupøH c= V by A23, A24, A13, BOOLE:29;
Int G c= G by TOPS_1:44; then
V c= G by A12, BOOLE:29;
hence TsupøH c= G by A25, BOOLE:29;
end;
hence Tsup is continuous by TMAP_1:49;
end;
theorem Th31: :: Corollary 1.12 p. 106
sup_op L is jointly_Scott-continuous implies L is sober
proof assume
A1: sup_op L is jointly_Scott-continuous;
A2: sigma L = the topology of ConvergenceSpace Scott-Convergence L
by WAYBEL11:def 12;
A3: the carrier of InclPoset sigma L = sigma L by YELLOW_1:1;
the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
then A4: sigma L = the topology of L by A2;
let S be irreducible Subset of L;
A5: S is non empty closed by YELLOW_8:def 4;
then A6: -S is open by TOPS_1:29;
A7: -S <> the carrier of L by Th2;
-S î sigma L by A6, A4, PRE_TOPC:def 5; then
reconsider V = -S as Element of InclPoset sigma L by A3, STRUCT_0:def 2;
V is prime by A4, Th17; then
consider p being Element of L such that
A8: V = -downarrow p by A1, A7, Th29;
A9: S = downarrow p by A8, TOPS_1:21;
take p;
A10: Cl {p} = downarrow p by WAYBEL11:9;
hence p is_dense_point_of S by A9, YELLOW_8:27;
let q be Point of L; assume
q is_dense_point_of S;
then A11: Cl {q} = S by A5, YELLOW_8:25;
L is T_0 by WAYBEL11:10;
hence p = q by A11, A10, A9, YELLOW_8:32;
end;
theorem :: Corollary 1.13 p. 106
L is continuous implies L is compact locally-compact sober Baire
proof assume
A1: L is continuous;
A2: uparrow ÁL = the carrier of L by Th10;
A3
: for X being Subset of L st X is open holds X is upper by WAYBEL11:def 4;then
A4: uparrow ÁL is compact by Th22;
êL = the carrier of L by PRE_TOPC:12;
hence L is compact by A2, A4, COMPTS_1:10;
thus A5: L is locally-compact
proof let x be Point of L, X be Subset of L such that
A6: x î X and
A7: X is open;
reconsider x' = x as Element of L by STRUCT_0:def 2;
set bas = { wayabove q where q is Element of L: q << x' };
A8: bas is basis of x by A1, WAYBEL11:44;
consider y being Element of L such that
A9: y << x' & y î X by A1, A6, A7, WAYBEL11:43;
X is upper by A7, WAYBEL11:def 4; then
A10: uparrow y c= X by A9, WAYBEL11:42;
set Y = uparrow y;
take Y;
wayabove y î bas by A9; then
A11: wayabove y is open & x î wayabove y by A8, YELLOW_8:21;
wayabove y c= Y by WAYBEL_3:11; then
wayabove y c= Int Y by A11, TOPS_1:56;
hence x î Int Y by A11;
thus Y c= X by A10;
thus Y is compact by A3, Th22;
end;
sup_op L is jointly_Scott-continuous by A1, Th30;
hence L is sober by Th31;
hence L is Baire by A5, WAYBEL12:48;
end;
theorem Th33: :: Theorem 1.14 (1) implies (2) p. 107
L is continuous & X î sigma L implies X = union {wayabove x : x î X}
proof assume that
A1: L is continuous and
A2: X î sigma L;
A3: X is open by A2, Th24;
set WAV = {wayabove x where x is Element of L : x î X};
now let x be set;
hereby assume
A4: x î X; then
reconsider x' = x as Element of L by STRUCT_0:def 2;
set bas = { wayabove q where q is Element of L: q << x' };
A5: bas is basis of x' by A1, WAYBEL11:44;
consider q being Element of L such that
A6: q << x' & q î X by A1, A4, A3, WAYBEL11:43;
wayabove q î bas by A6; then
A7: x' î wayabove q by A5, YELLOW_8:21;
wayabove q î WAV by A6;
hence x î union WAV by A7, TARSKI:def 4;
end; assume x î union WAV; then consider Y being set such that
A8: x î Y & Y î WAV by TARSKI:def 4;
consider q being Element of L such that
A9: Y = wayabove q & q î X by A8;
X is upper by A3, WAYBEL11:def 4; then
A10: uparrow q c= X by A9, WAYBEL11:42;
wayabove q c= uparrow q by WAYBEL_3:11; then
Y c= X by A10, A9, BOOLE:29;
hence x î X by A8;
end;
hence X = union {wayabove x where x is Element of L : x î X} by TARSKI:2;
end;
theorem :: Theorem 1.14 (2) implies (1) p. 107
(for X st X î sigma L holds X = union {wayabove x : x î X})
implies L is continuous
proof assume
A1: for X being Subset of L st X î sigma L
holds X = union {wayabove x where x is Element of L : x î X};
thus for x being Element of L holds waybelow x is non empty directed;
thus L is up-complete;
let x being Element of L;
set y = sup waybelow x, X = -downarrow y;
A2: y ó x by Th9;
assume
A3: x <> sup waybelow x;
now assume x î downarrow y; then x ó y by WAYBEL_0:17;
hence contradiction by A3, A2, ORDERS_1:25;
end; then
A4: x î X by YELLOW_6:10;
A5: X is open by WAYBEL11:12;
set Z = {wayabove z where z is Element of L : z î X};
X î sigma L by A5, Th24; then
X = union Z by A1; then consider Y being set such that
A6: x î Y & Y î Z by A4, TARSKI:def 4;
consider z being Element of L such that
A7: Y = wayabove z & z î X by A6;
z << x by A6, A7, WAYBEL_3:8; then
A8: z î waybelow x by WAYBEL_3:7;
y is_ò_than waybelow x by YELLOW_0:32; then
z ó y by A8, LATTICE3:def 9; then z î downarrow y by WAYBEL_0:17;
hence contradiction by A7, YELLOW_6:10;
end;
theorem :: Theorem 1.14 (1) implies (3 first conjunct) p. 107
L is continuous implies
ex B being basis of x st for X st X î B holds X is open filtered
proof assume
A1: L is continuous;
set A = { wayabove q where q is Element of L: q << x };
reconsider A as basis of x by A1, WAYBEL11:44;
set B = { V where V is Subset of L :
ex q being Element of L st V c= wayabove q & q< y;
set VVl = -downarrow y;
now assume x î downarrow y; then x ó y by WAYBEL_0:17;
hence contradiction by A7, A6, ORDERS_1:25;
end; then
A8: x î VVl by YELLOW_6:10;
VVl is open by WAYBEL11:12;
then VVl î sigma L by Th24; then
reconsider VVp = VVl as Element of IPs by A3, A4, STRUCT_0:def 2;
IPs is satisfying_axiom_of_approximation by A3, A2, WAYBEL_3:def 6; then
VVp = sup waybelow VVp by WAYBEL_3:def 5; then
VVp = union waybelow VVp by YELLOW_1:22; then
consider Vp being set such that
A9: x î Vp & Vp î waybelow VVp by A8, TARSKI:def 4;
reconsider Vp as Element of IPs by A9, STRUCT_0:def 2;
A10: Vp << VVp by A9, WAYBEL_3:7;
Vp î sigma L by A3, A4; then
reconsider Vl = Vp as Subset of L by STRUCT_0:def 3;
consider bas being basis of x such that
A11: for Y being Subset of L st Y î bas holds Y is open filtered by A1;
Vp î sigma L by A3, A4; then
Vl is open by A3, PRE_TOPC:def 5; then
consider Ul being Subset of L such that
A12: Ul î bas & Ul c= Vl by A9, YELLOW_8:def 2;
A13: Ul is open & x î Ul by A12, YELLOW_8:21; then
Ul î sigma L by A3, PRE_TOPC:def 5; then
A14: inf Ul î IU by A13;
y is_ò_than IU by YELLOW_0:32; then
inf Ul ó y by A14, LATTICE3:def 9; then
downarrow inf Ul c= downarrow y by WAYBEL_0:21; then
A15: -downarrow y c= -downarrow inf Ul by PRE_TOPC:19;
set F = {downarrow u where u is Element of L : u î Ul};
A16: downarrow x î F by A13;
F c= bool the carrier of L proof let X be set; assume X î F; then
consider u being Element of L such that
A17: X = downarrow u & u î Ul;
thus X î bool the carrier of L by A17;
end; then
F is non empty Subset-Family of the carrier of L by A16; then
reconsider F as non empty Subset-Family of L by STRUCT_0:def 4;
downarrow inf Ul = meet F by A13, Th15; then
A18: -downarrow inf Ul = - meet F
.= union COMPLEMENT F by TOPS_2:12;
A19: Ul is filtered by A12, A11;
A20: -downarrow x î COMPLEMENT F by A16, YELLOW_8:14;
COMPLEMENT F c= the topology of L proof let X be set; assume
A21: X î COMPLEMENT F;
then reconsider X' = X as Subset of L by STRUCT_0:def 3;
-X' î F by A21, YELLOW_8:13; then
consider u being Element of L such that
A22: -X' = downarrow u & u î Ul;
X' = -downarrow u by A22, PRE_TOPC:20; then
X' is open by WAYBEL11:12;
hence X î the topology of L by PRE_TOPC:def 5;
end; then
reconsider CF = COMPLEMENT F as Subset of IPs by A4, STRUCT_0:def 3;
A23: CF is directed by A3, A19, Lm2;
VVp c= union CF by A15, A18; then
VVp c= sup CF by YELLOW_1:22; then
VVp ó sup CF by YELLOW_1:3; then
consider d being Element of IPs such that
A24: d î CF & Vp << d by A20, A10, A23, A3, A2, WAYBEL_4:50;
d î sigma L by A3, A4; then
reconsider d' = d as Subset of L by STRUCT_0:def 3;
-d' î F by A24, YELLOW_8:13; then
consider u being Element of L such that
A25: -d' = downarrow u & u î Ul;
A26: d = -downarrow u by A25, PRE_TOPC:20;
Vp ó d by A24, WAYBEL_3:1; then
A27: Vp c= d by YELLOW_1:3;
u ó u; then
u î downarrow u by WAYBEL_0:17; then
not u î d by A26, YELLOW_6:10; then
not u î Vp by A27;
hence contradiction by A12, A25;
end;
theorem Th38: :: Theorem 1.14 (4) implies (1) p. 107
(for x holds x = \/ ({inf X : x î X & X î sigma L}, L))
implies L is continuous
proof assume
A1: for x being Element of L
holds x = \/ ({inf V where V is Subset of L : x î V & V î sigma L}, L);
thus for x being Element of L holds waybelow x is non empty directed;
thus L is up-complete;
let x be Element of L;
set VV = {inf V where V is Subset of L : x î V & V î sigma L};
A2: VV c= waybelow x proof let d be set; assume d î VV; then
consider V being Subset of L such that
A3: inf V = d & x î V & V î sigma L;
V is open by A3, Th24; then
inf V << x by A3, Th26;
hence d î waybelow x by A3, WAYBEL_3:7;
end;
ex_sup_of VV, L & ex_sup_of waybelow x, L by YELLOW_0:17; then
A4: \/ (VV, L) ó sup waybelow x by A2, YELLOW_0:34;
x = \/ (VV, L) & sup waybelow x ó x by A1, Th9;
hence x = sup waybelow x by A4, ORDERS_1:25;
end;
theorem Th39: :: Theorem 1.14 (3) iff (5) p. 107
:: The conjunct InclPoset sigma L is continuous is dropped
(for x ex B being basis of x st for Y st Y î B holds Y is open filtered)
iff (for V ex VV st V = sup VV & for W st W î VV holds W is co-prime)
proof set IPs = InclPoset the topology of L;
A1: sigma L = the topology of L by Th23;
then A2: the carrier of IPs = sigma L by YELLOW_1:1;
hereby assume
A3: for x being Element of L ex X being basis of x st
for Y being Subset of L st Y î X holds Y is open filtered;
let V be Element of InclPoset sigma L;
A4: V î sigma L by A1, A2; then
reconsider Vl = V as Subset of L by STRUCT_0:def 3;
A5: Vl is open by A4, Th24;
set X = {Y where Y is Subset of L : Y c= V &
ex x being Element of L, bas being basis of x
st x î V & Y î bas &
for Yx being Subset of L st Yx î bas holds Yx is open filtered};
now let YY be set; assume YY î X; then
consider Y being Subset of L such that
A6: Y = YY and Y c= V and
A7: ex x being Element of L, bas being basis of x
st x î V & Y î bas &
for Yx being Subset of L st Yx î bas holds Yx is open filtered;
consider x be Element of L, bas being basis of x such that
A8: x î V & Y î bas by A7;
Y is open by A8, YELLOW_8:21; then
Y î sigma L by Th24;
hence YY î the carrier of InclPoset sigma L by A6, YELLOW_1:1;
end; then
X c= the carrier of InclPoset sigma L by TARSKI:def 3; then
reconsider X as Subset of InclPoset sigma L by STRUCT_0:def 3;
take X;
now let x be set;
hereby assume
A9: x î V; Vl = V; then
reconsider d = x as Element of L by A9, STRUCT_0:def 2;
consider bas being basis of d such that
A10: for Y being Subset of L st Y î bas holds Y is open filtered by A3;
consider Y being Subset of L such that
A11: Y î bas & Y c= V by A9, A5, YELLOW_8:22;
x î Y & Y î X by A11, YELLOW_8:21, A9, A10;
hence x î union X by TARSKI:def 4;
end; assume x î union X; then consider YY being set such that
A12: x î YY & YY î X by TARSKI:def 4;
consider Y being Subset of L such that
A13: Y = YY and
A14: Y c= V and
ex x being Element of L, bas being basis of x
st x î V & Y î bas &
for Yx being Subset of L st Yx î bas holds Yx is open filtered
by A12;
thus x î V by A12, A13, A14;
end; then
V = union X by TARSKI:2;
hence V = sup X by A1, YELLOW_1:22;
let Yp be Element of InclPoset sigma L; assume Yp î X; then
consider Y being Subset of L such that
A15: Y = Yp and Y c= V and
A16: ex x being Element of L, bas being basis of x
st x î V & Y î bas &
for Yx being Subset of L st Yx î bas holds Yx is open filtered;
consider x being Element of L, bas being basis of x such that
x î V and
A17: Y î bas and
A18: for Yx being Subset of L st Yx î bas holds Yx is open filtered by A16;
A19: Y is open filtered by A17, A18; then
Y is upper by WAYBEL11:def 4;
hence Yp is co-prime by A15, A19, Th27;
end; assume
A20: for V being Element of InclPoset sigma L
ex X being Subset of InclPoset sigma L st V = sup X &
for x being Element of InclPoset sigma L
st x î X holds x is co-prime;
let x be Element of L;
set bas = {V where V is Element of InclPoset sigma L :
x î V & V is co-prime};
bas c= bool the carrier of L proof let VV be set; assume VV î bas; then
ex V being Element of InclPoset sigma L st VV= V &
x î V & V is co-prime; then VV î sigma L by A1, A2;
hence thesis;
end; then
reconsider bas as Subset-Family of L by STRUCT_0:def 4;
bas is basis of x proof
thus bas c= the topology of L proof let VV be set; assume VV î bas; then
ex V being Element of InclPoset sigma L st VV= V &
x î V & V is co-prime; then VV î sigma L by A1, A2;
hence thesis by A1;
end;
now
per cases;
suppose bas is empty; then
Intersect bas = the carrier of L by CANTOR_1:def 3;
hence x î Intersect bas;
suppose A21: bas is non empty; then
A22: Intersect bas = meet bas by CANTOR_1:def 3;
now let Y be set; assume Y î bas; then
ex V being Element of InclPoset sigma L st Y = V &
x î V & V is co-prime;
hence x î Y;
end;
hence x î Intersect bas by A22, A21, SETFAM_1:def 1;
end;
hence x î Intersect bas;
let S be Subset of L; assume
A23: S is open & x î S;
then S î sigma L by Th24; then
reconsider S' = S as Element of IPs by A2, STRUCT_0:def 2;
consider X being Subset of IPs such that
A24: S' = sup X and
A25: for x being Element of IPs st x î X holds x is co-prime by A20, A1;
S' = union X by A24, YELLOW_1:22; then
consider V being set such that
A26: x î V & V î X by A23, TARSKI:def 4;
A27: V î sigma L by A2, A26; then
reconsider V as Subset of L by STRUCT_0:def 3;
reconsider Vp = V as Element of IPs by A2, A27, STRUCT_0:def 2;
take V;
Vp is co-prime by A25, A26;
hence V î bas by A26, A1;
sup X is_ò_than X by YELLOW_0:32; then
Vp ó sup X by A26, LATTICE3:def 9;
hence V c= S by A24, YELLOW_1:3;
end; then
reconsider bas as basis of x;
take bas;
let V be Subset of L; assume V î bas; then
consider Vp being Element of InclPoset sigma L such that
A28: V = Vp and x î Vp and
A29: Vp is co-prime;
Vp î sigma L by A1, A2;
hence V is open filtered by A28, A29, Th27, Th24;
end;
theorem :: Theorem 1.14 (5) iff (6) p. 107
(for V ex VV st V = sup VV & for W st W î VV holds W is co-prime)
& InclPoset sigma L is continuous
iff InclPoset sigma L is completely-distributive
proof InclPoset sigma L = InclPoset the topology of L by Th23;
hence thesis by WAYBEL_6:38;
end;
theorem :: Theorem 1.14 (6) iff (7) p. 107
InclPoset sigma L is completely-distributive
iff InclPoset sigma L is continuous & (InclPoset sigma L) opp is continuous
proof InclPoset sigma L = InclPoset the topology of L by Th23;
hence thesis by WAYBEL_6:39;
end;
theorem :: Corollary 1.15 (1) implies (2) p. 108
L is algebraic implies
ex B being basis of L st B = {uparrow x : x î the carrier of CompactSublatt L}
proof assume
A1: L is algebraic; then
reconsider L' = L as algebraic LATTICE;
A2: L is satisfying_axiom_K by A1, WAYBEL_8:def 4;
set P = {uparrow k where k is Element of L :
k î the carrier of CompactSublatt L};
P c= bool the carrier of L proof let x be set; assume x î P; then
ex k being Element of L st x = uparrow k &
k î the carrier of CompactSublatt L;
hence thesis;
end; then
reconsider P as Subset-Family of L by STRUCT_0:def 4;
A3: P c= the topology of L proof let x be set; assume x î P; then
consider k being Element of L such that
A4: x = uparrow k & k î the carrier of CompactSublatt L;
k is compact by A4, WAYBEL_8:def 1; then
uparrow k is Open by WAYBEL_8:2; then
uparrow k is open by WAYBEL11:41;
hence x î the topology of L by A4, PRE_TOPC:def 5;
end;
now let x be Point of L;
set B = {uparrow k where k is Element of L :
uparrow k î P & x î uparrow k};
B c= bool the carrier of L proof let y be set; assume y î B; then
ex k being Element of L st
y = uparrow k & uparrow k î P & x î uparrow k;
hence thesis;
end; then
reconsider B as Subset-Family of L by STRUCT_0:def 4;
B is basis of x proof
thus B c= the topology of L proof let y be set; assume y î B; then
ex k being Element of L st
y = uparrow k & uparrow k î P & x î uparrow k;
hence thesis by A3;
end;
now
per cases;
suppose B is empty; then
Intersect B = the carrier of L by CANTOR_1:def 3;
hence x î Intersect B;
suppose A5: B is non empty; then
A6: Intersect B = meet B by CANTOR_1:def 3;
now let Y be set; assume Y î B; then
ex k being Element of L st
Y = uparrow k & uparrow k î P & x î uparrow k;
hence x î Y;
end;
hence x î Intersect B by A6, A5, SETFAM_1:def 1;
end;
hence x î Intersect B;
let S be Subset of L such that
A7: S is open and
A8: x î S;
reconsider x' = x as Element of L by STRUCT_0:def 2;
A9: x = sup compactbelow x' by A2, WAYBEL_8:def 3;
S is inaccessible by A7, WAYBEL11:def 4; then
(compactbelow x') meets S by A8, A9, WAYBEL11:def 1; then
consider k being set such that
A10: k î compactbelow x' & k î S by BOOLE:def 5;
A11: compactbelow x' = downarrow x' ï the carrier of CompactSublatt L
by WAYBEL_8:5;
reconsider k as Element of L by A10, STRUCT_0:def 2;
take V = uparrow k;
k î the carrier of CompactSublatt L by A10, A11, BOOLE:def 3; then
A12: uparrow k î P;
k î downarrow x' by A10, A11, BOOLE:def 3; then
k ó x' by WAYBEL_0:17; then
x î uparrow k by WAYBEL_0:18;
hence V î B by A12;
S is upper by A7, WAYBEL11:def 4;
hence V c= S by A10, WAYBEL11:42;
end; then
reconsider B as basis of x;
take B;
thus B c= P proof let y be set; assume y î B; then
ex k being Element of L st
y = uparrow k & uparrow k î P & x î uparrow k;
hence y î P;
end;
end; then
P is basis of L by A3, YELLOW_8:23;
hence thesis;
end;
theorem :: Corollary 1.15 (2) implies (3) p. 108
(ex B being basis of L st B = {uparrow x :x î the carrier of CompactSublatt L})
implies InclPoset sigma L is algebraic &
for V ex VV st V = sup VV & for W st W î VV holds W is co-prime
proof given B being basis of L such that
A1: B = {uparrow k where k is Element of L :
k î the carrier of CompactSublatt L};
set IPt = InclPoset the topology of L;
set IPs = InclPoset sigma L;
A2: sigma L = the topology of L by Th23;
A3: the carrier of IPs = sigma L by YELLOW_1:1;
A4: IPs = IPt by A2;
thus InclPoset sigma L is algebraic proof
hereby let X be Element of IPs;
reconsider X' = X as Element of IPt by A4;
compactbelow X' is non empty;
hence compactbelow X is non empty by A4;
compactbelow X' is directed;
hence compactbelow X is directed by A4;
end;
thus IPs is up-complete by A4;
let X be Element of IPs;
set cX = compactbelow X;
A5: sup cX = union cX by A4, YELLOW_1:22;
set GB = { G where G is Subset of L: G î B & G c= X };
X î sigma L by A3; then
reconsider X' = X as Subset of L by STRUCT_0:def 3;
X' is open by A3, Th24; then
A6: X = union GB by YELLOW_8:18;
now let x be set;
hereby assume x î X; then consider GG being set such that
A7: x î GG & GG î GB by A6, TARSKI:def 4;
consider G being Subset of L such that
A8: G = GG & G î B & G c= X by A7;
consider k being Element of L such that
A9: G = uparrow k & k î the carrier of CompactSublatt L by A1, A8;
k is compact by A9, WAYBEL_8:def 1; then
uparrow k is Open by WAYBEL_8:2; then
uparrow k is open by WAYBEL11:41; then
uparrow k î the topology of L by PRE_TOPC:def 5; then
reconsider G as Element of IPs by A2, A3, A9, STRUCT_0:def 2;
A10: G ó X by A8, YELLOW_1:3;
for X being Subset of L st X is open holds X is upper by WAYBEL11:def 4;
then uparrow k is compact by Th22; then
G is compact by A9, A4, WAYBEL_3:36; then
G î cX by A10, WAYBEL_8:4;
hence x î union cX by A7, A8, TARSKI:def 4;
end; assume x î union cX; then consider G being set such that
A11: x î G & G î cX by TARSKI:def 4;
reconsider G as Element of IPs by A11, STRUCT_0:def 2;
G ó X by A11, WAYBEL_8:4; then
G c= X by YELLOW_1:3;
hence x î X by A11;
end;
hence X = sup compactbelow X by A5, TARSKI:2;
end;
let V be Element of InclPoset sigma L;
set GB = { G where G is Subset of L: G î B & G c= V };
GB c= the carrier of IPs proof let x be set; assume x î GB; then
consider G being Subset of L such that
A12: G = x & G î B & G c= V;
G is open by A12, YELLOW_8:19; then
G î sigma L by Th24;
hence x î the carrier of IPs by A12, A3;
end; then
reconsider GB as Subset of InclPoset sigma L by STRUCT_0:def 3;
take GB;
V î sigma L by A3; then
reconsider V' = V as Subset of L by STRUCT_0:def 3;
V' is open by A3, Th24; then
V = union GB by YELLOW_8:18;
hence V = sup GB by A4, YELLOW_1:22;
let x be Element of InclPoset sigma L; assume
x î GB; then consider G being Subset of L such that
A13: G = x & G î B & G c= V;
consider k being Element of L such that
A14: G = uparrow k & k î the carrier of CompactSublatt L by A1, A13;
thus x is co-prime by A13, A14, Th27;
end;
theorem :: Corollary 1.15 (3) implies (2) p. 108
:: The proof of ((3) implies (1)) is split into two parts
:: This one proves ((3) implies (2)) and the next is ((2) implies (1)).
InclPoset sigma L is algebraic &
(for V ex VV st V = sup VV & for W st W î VV holds W is co-prime)
implies
ex B being basis of L st B = {uparrow x : x î the carrier of CompactSublatt L}
proof assume that
A1: InclPoset sigma L is algebraic and
A2: for V being Element of InclPoset sigma L
ex X being Subset of InclPoset sigma L st V = sup X &
for x being Element of InclPoset sigma L
st x î X holds x is co-prime;
set IPt = InclPoset the topology of L;
set IPs = InclPoset sigma L;
A3: sigma L = the topology of L by Th23;
A4: the carrier of IPs = sigma L by YELLOW_1:1;
A5: IPs = IPt by A3;
A6: InclPoset sigma L is satisfying_axiom_K by A1, WAYBEL_8:def 4;
reconsider ips = InclPoset sigma L as algebraic LATTICE by A1, A5;
ips is continuous; then
A7: InclPoset sigma L is continuous;
(for x being Element of L ex X being basis of x st
for Y being Subset of L st Y î X holds Y is open filtered)
by A2, Th39; then
for x being Element of L holds
x = \/ ({inf V where V is Subset of L : x î V & V î sigma L}, L)
by A7, Th37;
then
A8: L is continuous by Th38;
set B = {uparrow k where k is Element of L :
k î the carrier of CompactSublatt L};
B c= bool the carrier of L proof let x be set; assume x î B; then
ex k being Element of L st x = uparrow k &
k î the carrier of CompactSublatt L;
hence thesis;
end; then
reconsider B as Subset-Family of L by STRUCT_0:def 4;
A9: B c= the topology of L proof let x be set; assume x î B; then
consider k being Element of L such that
A10: x = uparrow k & k î the carrier of CompactSublatt L;
k is compact by A10, WAYBEL_8:def 1; then
uparrow k is Open by WAYBEL_8:2; then
uparrow k is open by WAYBEL11:41;
hence x î the topology of L by A10, PRE_TOPC:def 5;
end;
now let x be Point of L;
set Bx = {uparrow k where k is Element of L :
uparrow k î B & x î uparrow k};
Bx c= bool the carrier of L proof let y be set; assume y î Bx; then
ex k being Element of L st
y = uparrow k & uparrow k î B & x î uparrow k;
hence thesis;
end; then
reconsider Bx as Subset-Family of L by STRUCT_0:def 4;
Bx is basis of x proof
thus Bx c= the topology of L proof let y be set; assume y î Bx; then
ex k being Element of L st
y = uparrow k & uparrow k î B & x î uparrow k;
hence thesis by A9;
end;
now
per cases;
suppose Bx is empty; then
Intersect Bx = the carrier of L by CANTOR_1:def 3;
hence x î Intersect Bx;
suppose A11: Bx is non empty; then
A12: Intersect Bx = meet Bx by CANTOR_1:def 3;
now let Y be set; assume Y î Bx; then
ex k being Element of L st
Y = uparrow k & uparrow k î B & x î uparrow k;
hence x î Y;
end;
hence x î Intersect Bx by A12, A11, SETFAM_1:def 1;
end;
hence x î Intersect Bx;
let S be Subset of L such that
A13: S is open and
A14: x î S;
S î the topology of L by A13, PRE_TOPC:def 5; then
reconsider S' = S as Element of IPt by A3, A4, STRUCT_0:def 2;
S' = sup compactbelow S' by A5, A6, WAYBEL_8:def 3; then
S' = union compactbelow S' by YELLOW_1:22; then
consider UA being set such that
A15: x î UA & UA î compactbelow S' by A14, TARSKI:def 4;
reconsider UA as Element of IPt by A15, STRUCT_0:def 2;
A16: UA ó S' & UA is compact by A15, WAYBEL_8:4;
consider F being Subset of InclPoset sigma L such that
A17: UA = sup F and
A18: for x being Element of InclPoset sigma L
st x î F holds x is co-prime by A2, A5;
A19: UA = union F by A5, A17, YELLOW_1:22;
UA î the topology of L by A3, A4; then
reconsider UA' = UA as Subset of L by STRUCT_0:def 3;
A20: UA << UA by A16, WAYBEL_3:def 2;
F is Subset of the topology of L by A3, A4; then
F is Subset-Family of the carrier of L by BOOLE:29; then
reconsider F' = F as Subset-Family of L by STRUCT_0:def 4;
F' is open proof let P be Subset of L;
assume P î F'; then P î the topology of L by A3, A4;
hence P is open by PRE_TOPC:def 5;
end; then
consider G being finite Subset of F' such that
A21: UA c= union G by A20, A19, WAYBEL_3:34;
union G c= union F by ZFMISC_1:95; then
A22: UA = union G by A19, A21, BOOLE:def 8;
G is finite Subset-Family of the carrier of L by BOOLE:29; then
reconsider G as finite Subset-Family of L by STRUCT_0:def 4;
consider Gg being finite Subset-Family of the carrier of L such that
A23: Gg c= G and
A24: union Gg = union G and
A25: for g being Subset of the carrier of L
st g î Gg holds not g c= union (Gg\{g}) by Th1;
consider U1 being set such that
A26: x î U1 & U1 î Gg by A15, A22, A24, TARSKI:def 4;
Gg c= F by A23, BOOLE:29; then
A27: U1 î F by A26; then
reconsider U1 as Element of IPs by STRUCT_0:def 2;
A28: U1 î the topology of L by A3, A4; then
reconsider U1' = U1 as Subset of L by STRUCT_0:def 3;
U1 is co-prime by A18, A27; then
A29: U1' is filtered upper by Th27;
set k = inf U1';
::
:: We simplify the proof from CCL a bit.
::
:: Our proof follows their idea but we use UA (their U) as the compact set
:: in InclPoset to get a contradiction after assumming that inf U1 is not
:: in U1.
::
now assume
A30: not k î U1';
set D = {-downarrow u where u is Element of L : u î U1'};
now assume U1' is empty; then
U1' c= union (Gg\{U1'}) by BOOLE:27;
hence contradiction by A26, A25;
end; then consider u being set such that
A31: u î U1' by ZFMISC_1:136;
reconsider u as Element of L by A31, STRUCT_0:def 2;
A32: -downarrow u î D by A31;
D c= the topology of L proof let d be set; assume
d î D; then consider u being Element of L such that
A33: d = -downarrow u & u î U1';
-downarrow u is open by WAYBEL11:12;
hence thesis by A33, PRE_TOPC:def 5;
end; then
reconsider D as non empty Subset of IPt
by A32, A4, A3, STRUCT_0:def 3;
A34: D is directed by A29, A5, Th25;
now assume not UA c= union D; then
consider l being set such that
A35: l î UA' & not l î union D by TARSKI:def 3;
reconsider l as Element of L by A35, STRUCT_0:def 2;
consider Uk being set such that
A36: l î Uk & Uk î Gg by A35, A22, A24, TARSKI:def 4;
Gg c= F by A23, BOOLE:29; then
A37: Uk î F by A36; then
reconsider Uk as Element of IPs by STRUCT_0:def 2;
Uk î the topology of L by A3, A4; then
reconsider Uk' = Uk as Subset of L by STRUCT_0:def 3;
Uk is co-prime by A18, A37; then
A38: Uk' is filtered upper by Th27;
A39: k is_ó_than U1' by YELLOW_0:33;
now assume not l is_ó_than U1'; then
consider m being Element of L such that
A40: m î U1' & not l ó m by LATTICE3:def 8;
-downarrow m î D by A40; then
not l î -downarrow m by A35, TARSKI:def 4; then
l î downarrow m by YELLOW_6:10;
hence contradiction by A40, WAYBEL_0:17;
end; then
l ó k by YELLOW_0:33; then
A41: k î Uk' by A36, A38, WAYBEL_0:def 20;
A42: U1' c= Uk proof let u be set; assume
A43: u î U1';
then reconsider d = u as Element of L by STRUCT_0:def 2;
k ó d by A43, A39, LATTICE3:def 8; then
d î Uk' by A41, A38, WAYBEL_0:def 20;
hence thesis;
end;
A44: U1' <> Uk by A41, A30;
U1' c= union (Gg\{U1'}) proof let u be set;
assume u î U1'; then
A45: u î Uk by A42;
Uk î Gg\{U1'} by A36, A44, ZFMISC_1:64;
hence u î union (Gg\{U1'}) by A45, TARSKI:def 4;
end;
hence contradiction by A25, A26;
end; then
UA c= sup D by YELLOW_1:22; then
UA ó sup D by YELLOW_1:3; then
consider d being Element of IPt such that
A46: d î D and
A47: UA ó d by A20, A34, WAYBEL_3:def 1;
consider u being Element of L such that
A48: d = -downarrow u & u î U1' by A46;
U1 c= UA by A27, A19, ZFMISC_1:92; then
A49: u î UA by A48;
UA c= d by A47, YELLOW_1:3; then
u î -downarrow u by A48, A49; then
A50: not u î downarrow u by YELLOW_6:10;
u ó u;
hence contradiction by A50, WAYBEL_0:17;
end; then
A51: uparrow k c= U1' by A29, WAYBEL11:42;
U1' c= uparrow k proof let x be set; assume
A52: x î U1'; then
reconsider x' = x as Element of L by STRUCT_0:def 2;
k is_ó_than U1' by YELLOW_0:33; then
k ó x' by A52, LATTICE3:def 8;
hence x î uparrow k by WAYBEL_0:18;
end; then
A53: U1' = uparrow k by A51, BOOLE:def 8;
U1' is open by A28, PRE_TOPC:def 5; then
U1' is Open by A29, A8, WAYBEL11:46; then
A54: k is compact by A53, WAYBEL_8:2;
take V = uparrow k;
k î the carrier of CompactSublatt L by A54, WAYBEL_8:def 1; then
uparrow k î B;
hence V î Bx by A53, A26;
A55: UA c= S by A16, YELLOW_1:3;
U1 c= UA by A26, A24, A22, ZFMISC_1:92;
hence V c= S by A55, A53, BOOLE:29;
end; then
reconsider Bx as basis of x;
take Bx;
thus Bx c= B proof let y be set; assume y î Bx; then
ex k being Element of L st
y = uparrow k & uparrow k î B & x î uparrow k;
hence y î B;
end;
end; then
reconsider B as basis of L by A9, YELLOW_8:23;
take B;
thus thesis;
end;
theorem :: Corollary 1.15 (2) implies (1) p. 108
(ex B being basis of L st B = {uparrow x :x î the carrier of CompactSublatt L})
implies L is algebraic
proof given B being basis of L such that
A1: B = {uparrow k where k is Element of L :
k î the carrier of CompactSublatt L};
thus for x being Element of L holds compactbelow x is non empty directed;
thus L is up-complete;
let x be Element of L;
set y = sup compactbelow x;
set cx = compactbelow x;
set dx = downarrow x;
set dy = downarrow y;
now assume
A2: y <> x;
now let z be Element of L; assume z î dx;
hence z ó x by WAYBEL_0:17;
end; then
x is_ò_than dx by LATTICE3:def 9; then
A3: sup dx ó x by YELLOW_0:32;
A4: ex_sup_of cx, L & ex_sup_of dx, L by YELLOW_0:17;
cx = dx ï the carrier of CompactSublatt L by WAYBEL_8:5; then
compactbelow x c= dx by BOOLE:37; then
sup compactbelow x ó sup dx by A4, YELLOW_0:34; then
A5: y ó x by A3, ORDERS_1:26;
now assume x î dy; then x ó y by WAYBEL_0:17;
hence contradiction by A5, A2, ORDERS_1:25;
end; then
A6: x î -dy by YELLOW_6:10;
set GB = { G where G is Subset of L: G î B & G c= -dy};
-dy is open by WAYBEL11:12; then
-dy = union GB by YELLOW_8:18;
then consider X being set such that
A7: x î X & X î GB by A6, TARSKI:def 4;
consider G being Subset of L such that
A8: G = X & G î B & G c= -dy by A7;
consider k being Element of L such that
A9: G = uparrow k & k î the carrier of CompactSublatt L by A1, A8;
A10: k ó x by A8, A9, A7, WAYBEL_0:18;
k is compact by A9, WAYBEL_8:def 1; then
A11: k î cx by A10, WAYBEL_8:4;
y is_ò_than cx by YELLOW_0:32; then
k ó y by A11, LATTICE3:def 9; then y î uparrow k by WAYBEL_0:18; then
y î -dy by A8, A9; then y ó y & not y î dy by YELLOW_6:10;
hence contradiction by WAYBEL_0:17;
end;
hence x = sup compactbelow x;
end;