:: The Scott Topology, Part II
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received August 27, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSET_1, SETFAM_1, TARSKI, SUBSET_1, XBOOLE_0, NAT_1, CARD_1,
ARYTM_3, STRUCT_0, RELAT_2, LATTICE3, ORDERS_2, WAYBEL_0, LATTICES,
XXREAL_0, EQREL_1, REWRITE1, ORDINAL2, WAYBEL_3, WAYBEL_6, RELAT_1,
INT_2, ZFMISC_1, WAYBEL_8, RCOMP_1, PRE_TOPC, YELLOW_8, YELLOW_1,
WAYBEL_9, RLVECT_3, WAYBEL11, PROB_1, YELLOW_6, FUNCT_1, WAYBEL_2,
TMAP_1, CONNSP_2, TOPS_1, CARD_FIL, YELLOW_0, WAYBEL_5, ARYTM_0,
WAYBEL14;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XCMPLX_0, NAT_1,
SETFAM_1, FINSET_1, DOMAIN_1, FUNCT_1, RELSET_1, BINOP_1, FUNCT_2,
ORDERS_2, LATTICE3, CARD_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2,
BORSUK_1, TMAP_1, CANTOR_1, COMPTS_1, YELLOW_0, YELLOW_1, 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;
constructors SETFAM_1, FINSUB_1, NAT_1, TOPS_1, TOPS_2, BORSUK_1, TMAP_1,
T_0TOPSP, CANTOR_1, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_5, WAYBEL_6,
WAYBEL_8, YELLOW_8, WAYBEL11, COMPTS_1, BINOP_1, WAYBEL_2, NUMBERS;
registrations SUBSET_1, RELSET_1, FINSET_1, XCMPLX_0, STRUCT_0, PRE_TOPC,
BORSUK_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_4, WAYBEL_3,
YELLOW_6, WAYBEL_6, WAYBEL_8, YELLOW_8, WAYBEL11, ORDINAL1, CARD_1,
TOPS_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, WAYBEL_0, WAYBEL_6, TMAP_1, YELLOW_8, COMPTS_1, WAYBEL_3,
WAYBEL_1, WAYBEL_8, TOPS_2, XBOOLE_0, SETFAM_1;
equalities WAYBEL_0, WAYBEL_3, WAYBEL_8, XBOOLE_0, SUBSET_1, BINOP_1,
STRUCT_0;
expansions TARSKI, WAYBEL_0, WAYBEL_6, COMPTS_1, WAYBEL_3, TOPS_2, XBOOLE_0;
theorems TARSKI, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, FUNCT_1, FUNCT_2,
SETFAM_1, LATTICE3, CARD_2, ORDERS_2, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1,
TMAP_1, CONNSP_2, 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, XBOOLE_0, XBOOLE_1, XCMPLX_1;
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 in 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 in G holds not g c= union (G\{g});
A1: now
let n be Nat;
assume
A2: P[n];
thus P[n+1]
proof
let F be finite Subset-Family of X;
assume
A3: card F = n+1;
per cases;
suppose
ex g being Subset of X st g in F & g c= union (F\{g});
then consider g being Subset of X such that
A4: g in F and
A5: g c= union (F\{g});
reconsider FF = F\{g} as finite Subset-Family of X;
{g} c= F by A4,ZFMISC_1:31;
then
A6: F = FF \/ {g} by XBOOLE_1:45;
A7: union F c= union FF
proof
let x be object;
assume x in union F;
then consider X being set such that
A8: x in X and
A9: X in F by TARSKI:def 4;
per cases by A6,A9,XBOOLE_0:def 3;
suppose
X in FF;
then X c= union FF by ZFMISC_1:74;
hence thesis by A8;
end;
suppose
X in {g};
then X = g by TARSKI:def 1;
hence thesis by A5,A8;
end;
end;
g in {g} by TARSKI:def 1;
then not g in FF by XBOOLE_0:def 5;
then card (FF \/ {g}) = card FF + 1 by CARD_2:41;
then consider G being finite Subset-Family of X such that
A10: G c= FF and
A11: union G = union FF and
A12: for g being Subset of X st g in G holds not g c= union (G\{g}
) by A2,A3,A6,XCMPLX_1:2;
take G;
FF c= F by A6,XBOOLE_1:7;
hence G c= F by A10;
union FF c= union F by A6,XBOOLE_1:7,ZFMISC_1:77;
hence union G = union F by A11,A7;
thus thesis by A12;
end;
suppose
A13: not ex g being Subset of X st g in F & g c= union (F\{g});
take G = F;
thus G c= F;
thus union G = union F;
thus thesis by A13;
end;
end;
end;
let F be finite Subset-Family of X;
A14: card F = card F;
A15: P[0]
proof
let F be finite Subset-Family of X;
assume
A16: card F = 0;
take G = F;
thus G c= F;
thus union G = union F;
thus thesis by A16;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A15, A1);
hence thesis by A14;
end;
Lm1: for S being 1-sorted, X, Y being Subset of S holds X c= Y` iff Y c= X`
proof
let S be 1-sorted, X, Y be Subset of S;
Y = Y``;
hence thesis by SUBSET_1:12;
end;
theorem Th2:
for S being 1-sorted, X being Subset of S holds X` = the carrier
of S iff X is empty
proof
let S be 1-sorted, X be Subset of S;
hereby
assume X` = the carrier of S;
then X = ([#](the carrier of S))`;
hence X is empty by XBOOLE_1:37;
end;
assume X is empty;
hence thesis;
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 object;
hereby
assume
A1: z in downarrow (x"/\"y);
then reconsider z9 = z as Element of R;
A2: z9 <= (x"/\"y) by A1,WAYBEL_0:17;
(x"/\"y) <= y by YELLOW_0:23;
then z9 <= y by A2,YELLOW_0:def 2;
then
A3: z9 in downarrow y by WAYBEL_0:17;
(x"/\"y) <= x by YELLOW_0:23;
then z9 <= x by A2,YELLOW_0:def 2;
then z9 in downarrow x by WAYBEL_0:17;
hence z in (downarrow x) /\ downarrow y by A3,XBOOLE_0:def 4;
end;
assume
A4: z in (downarrow x) /\ downarrow y;
then reconsider z9 = z as Element of R;
z in downarrow y by A4,XBOOLE_0:def 4;
then
A5: z9 <= y by WAYBEL_0:17;
z in (downarrow x) by A4,XBOOLE_0:def 4;
then z9 <= x by WAYBEL_0:17;
then x"/\"y >= z9 by A5,YELLOW_0:23;
hence z in downarrow (x"/\"y) by WAYBEL_0:17;
end;
hence thesis 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 object;
hereby
assume
A1: z in uparrow (x"\/"y);
then reconsider z9 = z as Element of R;
A2: z9 >= (x"\/"y) by A1,WAYBEL_0:18;
(x"\/"y) >= y by YELLOW_0:22;
then z9 >= y by A2,YELLOW_0:def 2;
then
A3: z9 in uparrow y by WAYBEL_0:18;
(x"\/"y) >= x by YELLOW_0:22;
then z9 >= x by A2,YELLOW_0:def 2;
then z9 in uparrow x by WAYBEL_0:18;
hence z in (uparrow x) /\ uparrow y by A3,XBOOLE_0:def 4;
end;
assume
A4: z in (uparrow x) /\ uparrow y;
then reconsider z9 = z as Element of R;
z in uparrow y by A4,XBOOLE_0:def 4;
then
A5: z9 >= y by WAYBEL_0:18;
z in (uparrow x) by A4,XBOOLE_0:def 4;
then z9 >= x by WAYBEL_0:18;
then x"\/"y <= z9 by A5,YELLOW_0:22;
hence z in uparrow (x"\/"y) by WAYBEL_0:18;
end;
hence thesis by TARSKI:2;
end;
theorem Th5:
for L being complete antisymmetric non empty RelStr, X being
lower Subset of L st sup X in 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 in X;
X is_<=_than sup X by YELLOW_0:32;
hence X c= downarrow sup X by YELLOW_2:1;
thus thesis by A1,WAYBEL11:6;
end;
theorem
for L being complete antisymmetric non empty RelStr, X being upper
Subset of L st inf X in 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 in X;
X is_>=_than inf X by YELLOW_0:33;
hence X c= uparrow inf X by YELLOW_2:2;
thus thesis 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 object;
assume
A2: z in uparrow y;
then reconsider z9 = z as Element of R;
y <= z9 by A2,WAYBEL_0:18;
then x << z9 by A1,WAYBEL_3:2;
hence thesis;
end;
end;
y <= y;
then
A3: y in uparrow y by WAYBEL_0:18;
assume uparrow y c= wayabove x;
hence thesis by A3,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 object;
assume
A2: z in downarrow x;
then reconsider z9 = z as Element of R;
z9 <= x by A2,WAYBEL_0:17;
then z9 << y by A1,WAYBEL_3:2;
hence thesis;
end;
end;
x <= x;
then
A3: x in downarrow x by WAYBEL_0:17;
assume downarrow x c= waybelow y;
hence thesis by A3,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 Bottom L = the carrier of L
proof
let L be lower-bounded antisymmetric non empty RelStr;
set uL = uparrow Bottom L, cL = the carrier of L;
for x being object holds x in uL iff x in cL by WAYBEL_0:18,YELLOW_0:44;
hence thesis by TARSKI:2;
end;
theorem
for L being upper-bounded antisymmetric non empty RelStr holds
downarrow Top L = the carrier of L
proof
let L be upper-bounded antisymmetric non empty RelStr;
set uL = downarrow Top L, cL = the carrier of L;
for x being object holds x in uL iff x in cL by WAYBEL_0:17,YELLOW_0:45;
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;
{x}"\/"{y} = {x"\/"y} & (uparrow x)"\/"(uparrow y) c= uparrow ((uparrow
x) "\/"(uparrow y)) by WAYBEL_0:16,YELLOW_4:19;
then
A1: (uparrow x)"\/"(uparrow y) c= uparrow (x"\/"y) by YELLOW_4:35;
wayabove x c= uparrow x & wayabove y c= uparrow y by WAYBEL_3:11;
then (wayabove x)"\/"(wayabove y) c= (uparrow x)"\/"(uparrow y) by
YELLOW_4:21;
hence thesis by A1;
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;
{x}"/\"{y} = {x"/\"y} & (downarrow x)"/\"(downarrow y) c= downarrow ((
downarrow x)"/\"(downarrow y)) by WAYBEL_0:16,YELLOW_4:46;
then
A1: (downarrow x)"/\"(downarrow y) c= downarrow (x"/\"y) by YELLOW_4:62;
waybelow x c= downarrow x & waybelow y c= downarrow y by WAYBEL_3:11;
then (waybelow x)"/\"(waybelow y) c= (downarrow x)"/\"(downarrow y) by
YELLOW_4:48;
hence thesis by A1;
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;
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~ <= l~ or y~ <= l~ by A1,A2;
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~;
A4: ~(x "/\" y) = x "/\" y by LATTICE3:def 7
.= ~x"\/"~y by YELLOW_7:24;
assume x "/\" y <= l~;
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 in 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 in V};
consider u being object such that
A1: u in V by XBOOLE_0:def 1;
A2: F c= bool the carrier of P
proof
let X be object;
assume X in F;
then ex u being Element of P st X = downarrow u & u in V;
hence thesis;
end;
reconsider u as Element of P by A1;
A3: downarrow u in F by A1;
reconsider F as Subset-Family of P by A2;
reconsider F as Subset-Family of P;
now
let x be object;
hereby
assume
A4: x in downarrow inf V;
then reconsider d = x as Element of P;
A5: d <= inf V by A4,WAYBEL_0:17;
now
let Y be set;
assume Y in F;
then consider u being Element of P such that
A6: Y = downarrow u and
A7: u in V;
inf V is_<=_than V by YELLOW_0:33;
then inf V <= u by A7,LATTICE3:def 8;
then d <= u by A5,ORDERS_2:3;
hence x in Y by A6,WAYBEL_0:17;
end;
hence x in meet F by A3,SETFAM_1:def 1;
end;
assume
A8: x in meet F;
then reconsider d = x as Element of P;
now
let b be Element of P;
assume b in V;
then downarrow b in F;
then d in downarrow b by A8,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 in 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 in 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 in V};
consider u being object such that
A1: u in V by XBOOLE_0:def 1;
A2: F c= bool the carrier of P
proof
let X be object;
assume X in F;
then ex u being Element of P st X = uparrow u & u in V;
hence thesis;
end;
reconsider u as Element of P by A1;
A3: uparrow u in F by A1;
reconsider F as Subset-Family of P by A2;
reconsider F as Subset-Family of P;
now
let x be object;
hereby
assume
A4: x in uparrow sup V;
then reconsider d = x as Element of P;
A5: d >= sup V by A4,WAYBEL_0:18;
now
let Y be set;
assume Y in F;
then consider u being Element of P such that
A6: Y = uparrow u and
A7: u in V;
sup V is_>=_than V by YELLOW_0:32;
then sup V >= u by A7,LATTICE3:def 9;
then d >= u by A5,ORDERS_2:3;
hence x in Y by A6,WAYBEL_0:18;
end;
hence x in meet F by A3,SETFAM_1:def 1;
end;
assume
A8: x in meet F;
then reconsider d = x as Element of P;
now
let b be Element of P;
assume b in V;
then uparrow b in F;
then d in uparrow b by A8,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 in uparrow sup V by WAYBEL_0:18;
end;
hence thesis by TARSKI:2;
end;
registration
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 in cX and
A2: yy in cX;
set z = xx "\/" yy;
yy is compact by A2,WAYBEL_8:4;
then yy <= z & yy << yy by YELLOW_0:22;
then
A3: yy << z by WAYBEL_3:2;
xx is compact by A1,WAYBEL_8:4;
then xx <= z & xx << xx by YELLOW_0:22;
then xx << z by WAYBEL_3:2;
then z << z by A3,WAYBEL_3:3;
then
A4: z is compact;
take z;
xx <= x & yy <= x by A1,A2,WAYBEL_8:4;
then z <= x by YELLOW_0:22;
hence z in cX by A4;
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 be irreducible Subset of T, V be Element of
InclPoset the topology of T such that
A1: V =S`;
set sL = the topology of T;
let X, Y be Element of InclPoset sL;
A2: the carrier of InclPoset the topology of T = the topology of T by
YELLOW_1:1;
then X in sL & Y in sL;
then reconsider X9 = X, Y9 = Y as Subset of T;
X9 /\ Y9 in sL by A2,PRE_TOPC:def 1;
then
A3: X /\ Y = X "/\" Y by YELLOW_1:9;
assume X "/\" Y <= V;
then X /\ Y c= V by A3,YELLOW_1:3;
then S c= (X9/\Y9)` by A1,Lm1;
then S c= X9` \/ Y9` by XBOOLE_1:54;
then S = (X9` \/ Y9`)/\S by XBOOLE_1:28;
then
A4: S = (X9`)/\S \/ (Y9`)/\S by XBOOLE_1:23;
A5: S is closed by YELLOW_8:def 3;
Y9 is open by A2,PRE_TOPC:def 2;
then Y9` is closed;
then
A6: (Y9`)/\S is closed by A5;
X9 is open by A2,PRE_TOPC:def 2;
then X9` is closed;
then (X9`)/\S is closed by A5;
then S = (X9`)/\S or S = (Y9`)/\S by A6,A4,YELLOW_8:def 3;
then S c= X9` or S c= Y9` by XBOOLE_1:17;
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 \/ y & x "/\" y = x /\ y
proof
let T be non empty TopSpace, x, y be Element of InclPoset the topology of T;
A1: the carrier of InclPoset the topology of T = the topology of T by
YELLOW_1:1;
then x in the topology of T & y in the topology of T;
then reconsider x9 = x, y9 = y as Subset of T;
x9 is open & y9 is open by A1,PRE_TOPC:def 2;
then x9 \/ y9 is open;
then x9 \/ y9 in the topology of T by PRE_TOPC:def 2;
hence x "\/" y = x \/ y by YELLOW_1:8;
x9 /\ y9 in the topology of T by A1,PRE_TOPC:def 1;
hence thesis 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;
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 \/ 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 \/ Y;
X \/ 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 \/ 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 \/ Y = X"\/"Y by Th18;
then V c= X \/ 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;
registration
let T be non empty TopSpace;
cluster InclPoset the topology of T -> distributive;
coherence
proof
let x, y, z be Element of InclPoset the topology of T;
thus x "/\" (y "\/" z) = x /\ (y "\/" z) by Th18
.= x /\ (y \/ z) by Th18
.= x /\ y \/ x /\ z by XBOOLE_1:23
.= (x "/\" y) \/ x /\ z by Th18
.= (x "/\" y) \/ (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;
then reconsider X9 = X as Subset-Family of T;
assume
A2: t = l;
assume
A3: X is Basis of l;
then
A4: X c= the topology of L by TOPS_2:64;
A5: l in Intersect X by A3,YELLOW_8:def 1;
A6: for S being Subset of L st S is open & l in S ex V being Subset of L
st V in X & V c= S by A3,YELLOW_8:def 1;
now
let S be Subset of T such that
A7: S is open and
A8: t in S;
reconsider S9 = S as Subset of L by A1;
S in the topology of T by A7,PRE_TOPC:def 2;
then S9 is open by A1,PRE_TOPC:def 2;
then consider V being Subset of L such that
A9: V in X & V c= S9 by A2,A6,A8;
reconsider V as Subset of T by A1;
take V;
thus V in X9 & V c= S by A9;
end;
hence thesis by A1,A2,A4,A5,TOPS_2:64,YELLOW_8:def 1;
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 Cover of P and
A3: F is open;
x <= x;
then
A4: x in P by WAYBEL_0:18;
P c= union F by A2,SETFAM_1:def 11;
then consider Y being set such that
A5: x in Y and
A6: Y in F by A4,TARSKI:def 4;
reconsider Y as Subset of L by A6;
reconsider G = {Y} as Subset-Family of L;
reconsider G as Subset-Family of L;
take G;
thus G c= F by A6,ZFMISC_1:31;
Y is open by A3,A6;
then Y is upper by A1;
then P c= Y by A5,WAYBEL11:42;
hence P c= union G by ZFMISC_1:25;
thus thesis;
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;
registration
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
the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
hence thesis by WAYBEL11:def 12;
end;
theorem Th24:
X in sigma L iff X is open
proof
sigma L =the topology of L by Th23;
hence thesis by PRE_TOPC:def 2;
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 in 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 in V} and
A2: CF = COMPLEMENT F;
set IPs = InclPoset sigma L;
let x, y be Element of IPs such that
A3: x in CF and
A4: y in CF;
A5: sigma L = the topology of L by Th23;
then
A6: the carrier of IPs = the topology of L by YELLOW_1:1;
then x in sigma L & y in sigma L by A5;
then reconsider x9 = x, y9 = y as Subset of L;
x9` in F by A2,A3,SETFAM_1:def 7;
then consider ux being Element of L such that
A7: x9` = downarrow ux and
A8: ux in V by A1;
y9` in F by A2,A4,SETFAM_1:def 7;
then consider uy being Element of L such that
A9: y9` = downarrow uy and
A10: uy in V by A1;
consider uz being Element of L such that
A11: uz in V and
A12: uz <= ux and
A13: uz <= uy by A8,A10,WAYBEL_0:def 2;
(downarrow uz)` is open by WAYBEL11:12;
then reconsider z = (downarrow uz)` as Element of IPs by A6,PRE_TOPC:def 2;
take z;
downarrow uz in F by A1,A11;
hence z in CF by A2,YELLOW_8:5;
downarrow uz c= downarrow uy by A13,WAYBEL_0:21;
then
A14: (downarrow uy)` c= (downarrow uz)` by SUBSET_1:12;
downarrow uz c= downarrow ux by A12,WAYBEL_0:21;
then (downarrow ux)` c= (downarrow uz)` by SUBSET_1:12;
hence x <= z & y <= z by A7,A9,A14,YELLOW_1:3;
end;
theorem Th25:
for X being filtered Subset of L st VV = {(downarrow x)` : x in
X} holds VV is directed
proof
let V be filtered Subset of L;
set F = {downarrow u where u is Element of L : u in V};
F c= bool the carrier of L
proof
let x be object;
assume x in F;
then ex u being Element of L st x = downarrow u & u in V;
hence thesis;
end;
then reconsider F as Subset-Family of L;
reconsider F as Subset-Family of L;
assume
A1: VV = {(downarrow x)` : x in V};
VV c= bool the carrier of L
proof
let x be object;
assume x in VV;
then ex u being Element of L st x = (downarrow u)` & u in V by A1;
hence thesis;
end;
then reconsider VV as Subset-Family of L;
reconsider VV as Subset-Family of L;
now
let x be object;
hereby
assume x in VV;
then consider u being Element of L such that
A2: x = (downarrow u)` and
A3: u in V by A1;
downarrow u in F by A3;
hence x in COMPLEMENT F by A2,YELLOW_8:5;
end;
assume
A4: x in COMPLEMENT F;
then reconsider X = x as Subset of L;
X` in F by A4,SETFAM_1:def 7;
then consider u being Element of L such that
A5: X` = downarrow u and
A6: u in V;
X = (downarrow u)` by A5;
hence x in VV by A1,A6;
end;
then VV = COMPLEMENT F by TARSKI:2;
hence thesis by Lm2;
end;
theorem Th26:
X is open & x in X implies inf X << x
proof
assume that
A1: X is open and
A2: x in 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 in X by A2,A3;
then consider y being Element of L such that
A4: y in D and
A5: for x being Element of L st x in D & x >= y holds x in X by A3,
WAYBEL11:def 3;
take y;
thus y in D by A4;
y <= y;
then inf X is_<=_than X & y in X by A4,A5,YELLOW_0:33;
hence inf X <= y by LATTICE3:def 8;
end;
hence thesis;
end;
:: p. 105
definition
let R be non empty reflexive RelStr, f be Function of [:R, R:], R;
attr f is jointly_Scott-continuous means
for T being non empty
TopSpace st the TopStruct of T = ConvergenceSpace Scott-Convergence R ex ft
being Function 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: the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
A3: sigma L = the topology of ConvergenceSpace Scott-Convergence L by
WAYBEL11:def 12;
A4: the carrier of InclPoset sigma L = sigma L by YELLOW_1:1;
then
A5: X is upper by A1,A3,WAYBEL11:31;
hereby
assume
A6: V is co-prime;
thus X is filtered
proof
let v, w be Element of L such that
A7: v in X and
A8: w in X;
(downarrow w)` is open & (downarrow v)` is open by WAYBEL11:12;
then reconsider mdw = (downarrow w)`, mdv = (downarrow v)` as Element of
InclPoset sigma L by A3,A4,A2,PRE_TOPC:def 2;
w <= w;
then w in downarrow w by WAYBEL_0:17;
then not V c= (downarrow w)` by A1,A8,XBOOLE_0:def 5;
then
A9: not V <= mdw by YELLOW_1:3;
v <= v;
then v in downarrow v by WAYBEL_0:17;
then not V c= (downarrow v)` by A1,A7,XBOOLE_0:def 5;
then not V <= mdv by YELLOW_1:3;
then not V <= mdv "\/" mdw by A3,A6,A9,Th14;
then
A10: not V c= mdv "\/" mdw by YELLOW_1:3;
take z = v"/\"w;
A11: mdv \/ mdw = ((downarrow v) /\ downarrow w)` by XBOOLE_1:54
.= (downarrow(v"/\"w))` by Th3;
mdv \/ mdw c= mdv "\/" mdw by A3,YELLOW_1:6;
then not V c= mdv \/ mdw by A10;
then X meets (downarrow(v"/\"w))`` by A1,A11,SUBSET_1:24;
then X/\(downarrow(v"/\"w))`` <> {};
then consider zz being object such that
A12: zz in X/\downarrow(v"/\"w) by XBOOLE_0:def 1;
A13: zz in downarrow(v"/\"w) by A12,XBOOLE_0:def 4;
A14: zz in X by A12,XBOOLE_0:def 4;
reconsider zz as Element of L by A12;
zz <= v"/\"w by A13,WAYBEL_0:17;
hence z in X by A5,A14;
thus z <= v & z <= w by YELLOW_0:23;
end;
thus X is upper by A1,A3,A4,WAYBEL11:31;
end;
assume
A15: X is filtered upper;
assume not V is co-prime;
then consider Xx, Y being Element of InclPoset sigma L such that
A16: V <= Xx "\/" Y and
A17: not V <= Xx and
A18: not V <= Y by A3,Th14;
Xx in sigma L & Y in sigma L by A4;
then reconsider Xx9 = Xx, Y9 = Y as Subset of L;
A19: Y9 is open by A3,A4,A2,PRE_TOPC:def 2;
then
A20: Y9 is upper by WAYBEL11:def 4;
A21: Xx9 is open by A3,A4,A2,PRE_TOPC:def 2;
then Xx9 \/ Y9 is open by A19;
then Xx \/ Y in sigma L by A3,A2,PRE_TOPC:def 2;
then Xx \/ Y = Xx "\/" Y by YELLOW_1:8;
then
A22: V c= Xx \/ Y by A16,YELLOW_1:3;
not V c= Y by A18,YELLOW_1:3;
then consider w being object such that
A23: w in V and
A24: not w in Y;
not V c= Xx by A17,YELLOW_1:3;
then consider v being object such that
A25: v in V and
A26: not v in Xx;
reconsider v, w as Element of L by A1,A25,A23;
A27: Xx9 is upper by A21,WAYBEL11:def 4;
A28: now
assume
A29: v"/\"w in Xx9 \/ Y9;
per cases by A29,XBOOLE_0:def 3;
suppose
A30: v"/\"w in Xx9;
v"/\"w <= v by YELLOW_0:23;
hence contradiction by A26,A27,A30;
end;
suppose
A31: v"/\"w in Y9;
v"/\"w <= w by YELLOW_0:23;
hence contradiction by A24,A20,A31;
end;
end;
v"/\"w in X by A1,A15,A25,A23,WAYBEL_0:41;
hence contradiction by A1,A22,A28;
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 & the
TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32,def 12;
given u being Element of L such that
A3: X = (downarrow u)`;
Cl {u} = downarrow u & Cl {u} is irreducible by WAYBEL11:9,YELLOW_8:17;
hence V is prime by A1,A2,A3,Th17;
assume V = the carrier of L;
hence contradiction by A1,A3,Th2;
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: the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
set A = X`;
A6: sigma L = the topology of ConvergenceSpace Scott-Convergence L by
WAYBEL11:def 12;
A7: the carrier of InclPoset sigma L = sigma L by YELLOW_1:1;
then
A8: X is open by A1,A6,A5,PRE_TOPC:def 2;
then A is closed;
then
A9: A is directly_closed lower by WAYBEL11:7;
A10: A is directed
proof
set LxL = [:L qua non empty TopSpace, L:];
given a, b being Element of L such that
A11: a in A & b in A and
A12: for z being Element of L holds not (z in A & a <= z & b <= z);
a <= a"\/"b & b <= a"\/"b by YELLOW_0:22;
then not a"\/"b in A by A12;
then
A13: a"\/"b in X by XBOOLE_0:def 5;
consider Tsup being Function of LxL, L such that
A14: Tsup = sup_op L and
A15: Tsup is continuous by A2,A5;
A16: Tsup.(a,b) = a"\/"b by A14,WAYBEL_2:def 5;
[#]L <> {};
then Tsup"X is open by A8,A15,TOPS_2:43;
then consider AA being Subset-Family of LxL such that
A17: Tsup"X = union AA and
A18: for e being set st e in AA ex X1 being Subset of L, Y1 being
Subset of L st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
A19: the carrier of LxL = [:the carrier of L, the carrier of L:] by
BORSUK_1:def 2;
then [a,b] in the carrier of LxL by ZFMISC_1:def 2;
then [a,b] in Tsup"X by A13,A16,FUNCT_2:38;
then consider AAe being set such that
A20: [a,b] in AAe and
A21: AAe in AA by A17,TARSKI:def 4;
consider Va, Vb being Subset of L such that
A22: AAe = [:Va, Vb:] and
A23: Va is open and
A24: Vb is open by A18,A21;
A25: a in Va & b in Vb by A20,A22,ZFMISC_1:87;
reconsider Va9 = Va, Vb9 = Vb as Subset of L;
now
let x be object;
hereby
assume x in Tsup.:AAe;
then consider cd being object such that
A26: cd in the carrier of LxL and
A27: cd in AAe and
A28: Tsup.cd = x by FUNCT_2:64;
consider c, d being Element of L such that
A29: cd = [c,d] by A19,A26,DOMAIN_1:1;
reconsider c, d as Element of L;
A30: x = Tsup.(c,d) by A28,A29
.= c"\/"d by A14,WAYBEL_2:def 5;
A31: d <= c"\/"d & Vb9 is upper by A24,WAYBEL11:def 4,YELLOW_0:22;
d in Vb by A22,A27,A29,ZFMISC_1:87;
then
A32: x in Vb by A30,A31;
A33: c <= c"\/"d & Va9 is upper by A23,WAYBEL11:def 4,YELLOW_0:22;
c in Va by A22,A27,A29,ZFMISC_1:87;
then x in Va by A30,A33;
hence x in Va/\Vb by A32,XBOOLE_0:def 4;
end;
assume
A34: x in Va/\Vb;
then reconsider c = x as Element of L;
x in Va & x in Vb by A34,XBOOLE_0:def 4;
then
A35: [c,c] in AAe by A22,ZFMISC_1:87;
c <= c;
then c = c"\/"c by YELLOW_0:24;
then
A36: c = Tsup.(c,c) by A14,WAYBEL_2:def 5;
[c,c] in the carrier of LxL by A19,ZFMISC_1:87;
hence x in Tsup.:AAe by A35,A36,FUNCT_2:35;
end;
then
A37: Tsup.:AAe = Va/\Vb by TARSKI:2;
A38: Tsup.:(Tsup"X) c= X by FUNCT_1:75;
Tsup.:AAe c= Tsup.:(Tsup"X) by A17,A21,RELAT_1:123,ZFMISC_1:74;
then
A39: Tsup.:AAe c= X by A38;
Va in sigma L & Vb in sigma L by A6,A5,A23,A24,PRE_TOPC:def 2;
then Va c= X or Vb c= X by A1,A3,A6,A7,A37,A39,Th19;
hence contradiction by A11,A25,XBOOLE_0:def 5;
end;
take u = sup A;
now
assume A = {};
then A` = the carrier of L;
hence contradiction by A1,A4;
end;
then u in A by A9,A10,WAYBEL11:def 2;
then A = downarrow u by A9,Th5;
hence thesis;
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;
set Tsup = sup_op L;
let T be non empty TopSpace such that
A2: the TopStruct of T = ConvergenceSpace Scott-Convergence L;
A3: the carrier of [:T, T:] = [:the carrier of T, the carrier of T:] by
BORSUK_1:def 2;
A4: the carrier of T = the carrier of L by A2,YELLOW_6:def 24;
then the carrier of [:T,T:] = the carrier of [:L,L:] by A3,YELLOW_3:def 2;
then reconsider Tsup as Function of [:T, T:], T by A4;
take Tsup;
thus Tsup = sup_op L;
A5: the TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32;
for x being Point of [:T, T:] holds Tsup is_continuous_at x
proof
reconsider Lc = L as continuous complete Scott TopLattice by A1;
let ab be Point of [:T, T:];
reconsider Tsab = Tsup.ab as Point of T;
consider a, b being Point of T such that
A6: ab = [a,b] by A3,DOMAIN_1:1;
reconsider a9 = a, b9 = b as Element of L by A2,YELLOW_6:def 24;
set D1 = waybelow a9, D2 = waybelow b9;
set D = D1"\/"D2;
reconsider Tsab9 = Tsab as Element of L by A2,YELLOW_6:def 24;
let G be a_neighborhood of Tsup.ab;
A7: Tsab in Int G by CONNSP_2:def 1;
reconsider basab = { wayabove q where q is Element of L: q << Tsab9 } as
Basis of Tsab9 by A1,WAYBEL11:44;
basab is Basis of Tsab by A2,A5,Th21;
then consider V being Subset of T such that
A8: V in basab and
A9: V c= Int G by A7,YELLOW_8:def 1;
consider u being Element of L such that
A10: V = wayabove u and
A11: u << Tsab9 by A8;
A12: D = { x "\/" y where x, y is Element of L : x in D1 & y in D2 } by
YELLOW_4:def 3;
Lc = L;
then
A13: a9 = sup waybelow a9 & b9 = sup waybelow b9 by WAYBEL_3:def 5;
Tsab9 = Tsup.(a,b) by A6
.= a9"\/"b9 by WAYBEL_2:def 5
.= sup ((waybelow a9)"\/"(waybelow b9)) by A13,WAYBEL_2:4;
then consider xy being Element of L such that
A14: xy in D and
A15: u << xy by A1,A11,WAYBEL_4:53;
consider x, y being Element of L such that
A16: xy = x"\/"y and
A17: x in D1 and
A18: y in D2 by A14,A12;
reconsider H = [:wayabove x, wayabove y:] as Subset of [:T, T:] by A4,A3,
YELLOW_3:def 2;
y << b9 by A18,WAYBEL_3:7;
then
A19: b9 in wayabove y;
Int G c= G by TOPS_1:16;
then
A20: V c= G by A9;
reconsider wx = wayabove x, wy = wayabove y as Subset of T by A2,
YELLOW_6:def 24;
wayabove y is open by A1,WAYBEL11:36;
then wayabove y in the topology of L by PRE_TOPC:def 2;
then
A21: wy is open by A2,A5,PRE_TOPC:def 2;
wayabove x is open by A1,WAYBEL11:36;
then wayabove x in the topology of L by PRE_TOPC:def 2;
then wx is open by A2,A5,PRE_TOPC:def 2;
then H is open by A21,BORSUK_1:6;
then
A22: H = Int H by TOPS_1:23;
x << a9 by A17,WAYBEL_3:7;
then a9 in wayabove x;
then [a9,b9] in H by A19,ZFMISC_1:87;
then reconsider H as a_neighborhood of ab by A6,A22,CONNSP_2:def 1;
take H;
A23: Tsup.:H = (wayabove x)"\/"(wayabove y) & (wayabove x)"\/"(wayabove y)
c= uparrow (x"\/"y) by Th12,WAYBEL_2:35;
uparrow (x"\/"y) c= wayabove u by A15,A16,Th7;
then Tsup.:H c= V by A10,A23;
hence thesis by A20;
end;
hence thesis by TMAP_1:44;
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;
let S be irreducible Subset of L;
A2: sigma L = the topology of ConvergenceSpace Scott-Convergence L & the
TopStruct of L = ConvergenceSpace Scott-Convergence L by WAYBEL11:32,def 12;
A3: S is non empty closed by YELLOW_8:def 3;
then the carrier of InclPoset sigma L = sigma L & S` is open by YELLOW_1:1;
then reconsider V = S` as Element of InclPoset sigma L by A2,PRE_TOPC:def 2;
S` <> the carrier of L by Th2;
then consider p being Element of L such that
A4: V = (downarrow p)` by A1,A2,Th17,Th29;
A5: L is T_0 by WAYBEL11:10;
take p;
A6: Cl {p} = downarrow p by WAYBEL11:9;
A7: S = downarrow p by A4,TOPS_1:1;
hence p is_dense_point_of S by A6,YELLOW_8:18;
let q be Point of L;
assume q is_dense_point_of S;
then Cl {q} = S by A3,YELLOW_8:16;
hence thesis by A7,A6,A5,YELLOW_8:23;
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 Bottom L = the carrier of L & [#]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 uparrow Bottom L is compact by Th22;
hence L is compact by A2;
thus
A4: L is locally-compact
proof
let x be Point of L, X be Subset of L such that
A5: x in X and
A6: X is open;
reconsider x9 = x as Element of L;
consider y being Element of L such that
A7: y << x9 and
A8: y in X by A1,A5,A6,WAYBEL11:43;
set Y = uparrow y;
set bas = { wayabove q where q is Element of L: q << x9 };
A9: bas is Basis of x by A1,WAYBEL11:44;
wayabove y in bas by A7;
then wayabove y is open by A9,YELLOW_8:12;
then
A10: wayabove y c= Int Y by TOPS_1:24,WAYBEL_3:11;
take Y;
x in wayabove y by A7;
hence x in Int Y by A10;
X is upper by A6,WAYBEL11:def 4;
hence Y c= X by A8,WAYBEL11:42;
thus thesis by A3,Th22;
end;
sup_op L is jointly_Scott-continuous by A1,Th30;
hence L is sober by Th31;
hence thesis by A4,WAYBEL12:44;
end;
theorem Th33: :: Theorem 1.14 (1) implies (2) p. 107
L is continuous & X in sigma L implies X = union {wayabove x : x in X}
proof
assume that
A1: L is continuous and
A2: X in sigma L;
set WAV = {wayabove x where x is Element of L : x in X};
A3: X is open by A2,Th24;
now
let x be object;
hereby
assume
A4: x in X;
then reconsider x9 = x as Element of L;
consider q being Element of L such that
A5: q << x9 & q in X by A1,A3,A4,WAYBEL11:43;
x9 in wayabove q & wayabove q in WAV by A5;
hence x in union WAV by TARSKI:def 4;
end;
assume x in union WAV;
then consider Y being set such that
A6: x in Y and
A7: Y in WAV by TARSKI:def 4;
consider q being Element of L such that
A8: Y = wayabove q and
A9: q in X by A7;
A10: wayabove q c= uparrow q by WAYBEL_3:11;
X is upper by A3,WAYBEL11:def 4;
then uparrow q c= X by A9,WAYBEL11:42;
then Y c= X by A8,A10;
hence x in X by A6;
end;
hence thesis by TARSKI:2;
end;
theorem :: Theorem 1.14 (2) implies (1) p. 107
(for X st X in sigma L holds X = union {wayabove x : x in X}) implies
L is continuous
proof
assume
A1: for X being Subset of L st X in sigma L holds X = union {wayabove x
where x is Element of L : x in X};
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 y = sup waybelow x, X = (downarrow y)`;
assume
A2: x <> sup waybelow x;
A3: y <= x by Th9;
now
assume x in downarrow y;
then x <= y by WAYBEL_0:17;
hence contradiction by A3,A2,ORDERS_2:2;
end;
then
A4: x in X by XBOOLE_0:def 5;
set Z = {wayabove z where z is Element of L : z in X};
A5: y is_>=_than waybelow x by YELLOW_0:32;
X is open by WAYBEL11:12;
then X in sigma L by Th24;
then X = union Z by A1;
then consider Y being set such that
A6: x in Y and
A7: Y in Z by A4,TARSKI:def 4;
consider z being Element of L such that
A8: Y = wayabove z and
A9: z in X by A7;
z << x by A6,A8,WAYBEL_3:8;
then z in waybelow x;
then z <= y by A5,LATTICE3:def 9;
then z in downarrow y by WAYBEL_0:17;
hence contradiction by A9,XBOOLE_0:def 5;
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 in B holds
X is open filtered
proof
set B = { V where V is Subset of L : ex q being Element of L st V c=
wayabove q & q<<x & x in V & V is open filtered };
B c= bool the carrier of L
proof
let X be object;
assume X in B;
then ex V being Subset of L st X = V & ex q being Element of L st V c=
wayabove q & q<<x & x in V & V is open filtered;
hence thesis;
end;
then reconsider B as Subset-Family of L;
reconsider B as Subset-Family of L;
assume
A1: L is continuous;
then reconsider
A = { wayabove q where q is Element of L: q << x } as Basis of x
by WAYBEL11:44;
A2: B is Basis of x
proof
A3: B is open
proof
let Y be Subset of L;
assume Y in B;
then ex V being Subset of L st Y = V & ex q being Element of L st V c=
wayabove q & q<<x & x in V & V is open filtered;
hence thesis;
end;
B is x-quasi_basis
proof
thus x in Intersect B
proof
per cases;
suppose
B is empty;
then Intersect B = the carrier of L by SETFAM_1:def 9;
hence thesis;
end;
suppose
A4: B is non empty;
A5: now
let Y be set;
assume Y in B;
then ex V being Subset of L st Y = V & ex q being Element of L st V
c= wayabove q & q<<x & x in V& V is open filtered;
hence x in Y;
end;
Intersect B = meet B by A4,SETFAM_1:def 9;
hence thesis by A4,A5,SETFAM_1:def 1;
end;
end;
let S be Subset of L;
assume S is open & x in S;
then consider V being Subset of L such that
A6: V in A and
A7: V c= S by YELLOW_8:def 1;
consider q being Element of L such that
A8: V = wayabove q and
A9: q << x by A6;
consider F being Open Filter of L such that
A10: x in F and
A11: F c= wayabove q by A1,A9,WAYBEL_6:8;
take F;
F is open by WAYBEL11:41;
hence F in B by A9,A10,A11;
thus thesis by A7,A8,A11;
end;
hence thesis by A3;
end;
now
let Y be Subset of L;
assume Y in B;
then ex V being Subset of L st Y = V & ex q being Element of L st V c=
wayabove q & q<<x & x in V & V is open filtered;
hence Y is open filtered;
end;
hence thesis by A2;
end;
theorem :: Theorem 1.14 (1) implies (3 second conjunct) p. 107
L is continuous implies InclPoset sigma L is continuous
proof
assume
A1: L is continuous;
set IPs = InclPoset the topology of L;
A2: the carrier of IPs = the topology of L by YELLOW_1:1;
A3: sigma L = the topology of L by Th23;
IPs is satisfying_axiom_of_approximation
proof
let V be Element of IPs;
set VV = {wayabove x where x is Element of L : x in V};
set wV = waybelow V;
V in sigma L by A3,A2;
then
A4: V = union VV by A1,Th33;
now
let x be object;
hereby
assume x in V;
then consider xU being set such that
A5: x in xU and
A6: xU in VV by A4,TARSKI:def 4;
consider y being Element of L such that
A7: xU = wayabove y and
A8: y in V by A6;
wayabove y is open by A1,WAYBEL11:36;
then reconsider xU as Element of IPs by A2,A7,PRE_TOPC:def 2;
xU << V
proof
let D be non empty directed Subset of IPs;
assume V <= sup D;
then V c= sup D by YELLOW_1:3;
then V c= union D by YELLOW_1:22;
then consider DD being set such that
A9: y in DD and
A10: DD in D by A8,TARSKI:def 4;
DD in sigma L by A3,A2,A10;
then reconsider DD as Subset of L;
DD is open by A2,A10,PRE_TOPC:def 2;
then DD is upper by WAYBEL11:def 4;
then
A11: uparrow y c= DD by A9,WAYBEL11:42;
reconsider d = DD as Element of IPs by A10;
take d;
thus d in D by A10;
wayabove y c= uparrow y by WAYBEL_3:11;
then wayabove y c= DD by A11;
hence thesis by A7,YELLOW_1:3;
end;
then xU in wV;
hence x in union wV by A5,TARSKI:def 4;
end;
assume x in union wV;
then consider X being set such that
A12: x in X and
A13: X in wV by TARSKI:def 4;
reconsider X as Element of IPs by A13;
X << V by A13,WAYBEL_3:7;
then X <= V by WAYBEL_3:1;
then X c= V by YELLOW_1:3;
hence x in V by A12;
end;
then V = union waybelow V by TARSKI:2;
hence thesis by YELLOW_1:22;
end;
hence thesis by Th23;
end;
theorem Th37: :: Theorem 1.14 (3) implies (4) p. 107
(for x ex B being Basis of x st for Y st Y in B holds Y is open
filtered) & InclPoset sigma L is continuous implies x = "\/" ({inf X : x in X &
X in sigma L}, L)
proof
assume that
A1: for x being Element of L ex B being Basis of x st for Y being Subset
of L st Y in B holds Y is open filtered and
A2: InclPoset sigma L is continuous;
A3: sigma L = the topology of L by Th23;
set IU = {inf V where V is Subset of L : x in V & V in sigma L};
set IPs = InclPoset the topology of L;
A4: the carrier of IPs = the topology of L by YELLOW_1:1;
set y = "\/"(IU,L);
set VVl = (downarrow y)`;
now
let b be Element of L;
assume b in IU;
then consider V being Subset of L such that
A5: b = inf V and
A6: x in V and
V in sigma L;
b is_<=_than V by A5,YELLOW_0:33;
hence b <= x by A6,LATTICE3:def 8;
end;
then x is_>=_than IU by LATTICE3:def 9;
then
A7: y <= x by YELLOW_0:32;
assume
A8: x <> y;
now
assume x in downarrow y;
then x <= y by WAYBEL_0:17;
hence contradiction by A7,A8,ORDERS_2:2;
end;
then
A9: x in VVl by XBOOLE_0:def 5;
VVl is open by WAYBEL11:12;
then reconsider VVp = VVl as Element of IPs by A3,A4,Th24;
VVp = sup waybelow VVp by A2,A3,WAYBEL_3:def 5;
then VVp = union waybelow VVp by YELLOW_1:22;
then consider Vp being set such that
A10: x in Vp and
A11: Vp in waybelow VVp by A9,TARSKI:def 4;
reconsider Vp as Element of IPs by A11;
Vp in sigma L by A3,A4;
then reconsider Vl = Vp as Subset of L;
A12: Vp << VVp by A11,WAYBEL_3:7;
consider bas being Basis of x such that
A13: for Y being Subset of L st Y in bas holds Y is open filtered by A1;
A14: y is_>=_than IU by YELLOW_0:32;
Vl is open by A4,PRE_TOPC:def 2;
then consider Ul being Subset of L such that
A15: Ul in bas and
A16: Ul c= Vl by A10,YELLOW_8:def 1;
set F = {downarrow u where u is Element of L : u in Ul};
A17: x in Ul by A15,YELLOW_8:12;
then
A18: downarrow x in F;
F c= bool the carrier of L
proof
let X be object;
assume X in F;
then ex u being Element of L st X = downarrow u & u in Ul;
hence thesis;
end;
then reconsider F as non empty Subset-Family of L by A18;
COMPLEMENT F c= the topology of L
proof
let X be object;
assume
A19: X in COMPLEMENT F;
then reconsider X9 = X as Subset of L;
X9` in F by A19,SETFAM_1:def 7;
then consider u being Element of L such that
A20: X9` = downarrow u and
u in Ul;
X9 = (downarrow u)` by A20;
then X9 is open by WAYBEL11:12;
hence thesis by PRE_TOPC:def 2;
end;
then reconsider CF = COMPLEMENT F as Subset of IPs by YELLOW_1:1;
Ul is filtered by A13,A15;
then
A21: CF is directed by A3,Lm2;
Ul is open by A15,YELLOW_8:12;
then Ul in sigma L by A3,PRE_TOPC:def 2;
then inf Ul in IU by A17;
then inf Ul <= y by A14,LATTICE3:def 9;
then downarrow inf Ul c= downarrow y by WAYBEL_0:21;
then
A22: (downarrow y)` c= (downarrow inf Ul)` by SUBSET_1:12;
downarrow inf Ul = meet F by A17,Th15;
then (downarrow inf Ul)` = union COMPLEMENT F by TOPS_2:7;
then VVp c= sup CF by A22,YELLOW_1:22;
then
A23: VVp <= sup CF by YELLOW_1:3;
(downarrow x)` in COMPLEMENT F by A18,YELLOW_8:5;
then consider d being Element of IPs such that
A24: d in CF and
A25: Vp << d by A2,A3,A12,A21,A23,WAYBEL_4:53;
Vp <= d by A25,WAYBEL_3:1;
then
A26: Vp c= d by YELLOW_1:3;
d in sigma L by A3,A4;
then reconsider d9 = d as Subset of L;
d9` in F by A24,SETFAM_1:def 7;
then consider u being Element of L such that
A27: d9` = downarrow u and
A28: u in Ul;
u <= u;
then u in downarrow u by WAYBEL_0:17;
then not u in Vp by A27,A26,XBOOLE_0:def 5;
hence contradiction by A16,A28;
end;
theorem Th38: :: Theorem 1.14 (4) implies (1) p. 107
(for x holds x = "\/" ({inf X : x in X & X in 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 in V & V in 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 in V & V in sigma L};
A2: sup waybelow x <= x by Th9;
A3: VV c= waybelow x
proof
let d be object;
assume d in VV;
then consider V being Subset of L such that
A4: inf V = d and
A5: x in V and
A6: V in sigma L;
V is open by A6,Th24;
then inf V << x by A5,Th26;
hence thesis by A4;
end;
ex_sup_of VV, L & ex_sup_of waybelow x, L by YELLOW_0:17;
then
A7: "\/" (VV, L) <= sup waybelow x by A3,YELLOW_0:34;
x = "\/" (VV, L) by A1;
hence thesis by A7,A2,ORDERS_2:2;
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 in B holds Y is open
filtered) iff for V ex VV st V = sup VV & for W st W in 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 in X holds Y is open filtered;
let V be Element of InclPoset sigma L;
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 in V & Y in bas & for Yx being Subset of L st Yx in bas
holds Yx is open filtered};
now
let YY be object;
assume YY in X;
then consider Y being Subset of L such that
A4: Y = YY and
Y c= V and
A5: ex x being Element of L, bas being Basis of x st x in V & Y in
bas & for Yx being Subset of L st Yx in bas holds Yx is open filtered;
Y is open by A5;
then Y in sigma L by Th24;
hence YY in the carrier of InclPoset sigma L by A4,YELLOW_1:1;
end;
then reconsider X as Subset of InclPoset sigma L by TARSKI:def 3;
take X;
V in sigma L by A1,A2;
then reconsider Vl = V as Subset of L;
A6: Vl is open by A1,A2,Th24;
now
let x be object;
hereby
assume
A7: x in V;
Vl = V;
then reconsider d = x as Element of L by A7;
consider bas being Basis of d such that
A8: for Y being Subset of L st Y in bas holds Y is open filtered by A3;
consider Y being Subset of L such that
A9: Y in bas and
A10: Y c= V by A6,A7,YELLOW_8:13;
A11: x in Y by A9,YELLOW_8:12;
Y in X by A7,A8,A9,A10;
hence x in union X by A11,TARSKI:def 4;
end;
assume x in union X;
then consider YY being set such that
A12: x in YY and
A13: YY in X by TARSKI:def 4;
ex Y being Subset of L st Y = YY & Y c= V & ex x being Element of L,
bas being Basis of x st x in V & Y in bas & for Yx being Subset of L st Yx in
bas holds Yx is open filtered by A13;
hence x in V by A12;
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 in X;
then consider Y being Subset of L such that
A14: Y = Yp and
Y c= V and
A15: ex x being Element of L, bas being Basis of x st x in V & Y in
bas & for Yx being Subset of L st Yx in bas holds Yx is open filtered;
A16: Y is open filtered by A15;
then Y is upper by WAYBEL11:def 4;
hence Yp is co-prime by A14,A16,Th27;
end;
assume
A17: 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
in X holds x is co-prime;
let x be Element of L;
set bas = {V where V is Element of InclPoset sigma L : x in V & V is
co-prime};
bas c= bool the carrier of L
proof
let VV be object;
assume VV in bas;
then ex V being Element of InclPoset sigma L st VV= V & x in V & V is
co-prime;
then VV in sigma L by A1,A2;
hence thesis;
end;
then reconsider bas as Subset-Family of L;
reconsider bas as Subset-Family of L;
bas is Basis of x
proof
A18: bas is open
proof
let VV be Subset of L;
assume VV in bas;
then ex V being Element of InclPoset sigma L st VV= V & x in V & V is
co-prime;
hence thesis by A1,A2,PRE_TOPC:def 2;
end;
bas is x-quasi_basis
proof
now
per cases;
suppose
bas is empty;
then Intersect bas = the carrier of L by SETFAM_1:def 9;
hence x in Intersect bas;
end;
suppose
A19: bas is non empty;
A20: now
let Y be set;
assume Y in bas;
then ex V being Element of InclPoset sigma L st Y = V & x in V & V
is co-prime;
hence x in Y;
end;
Intersect bas = meet bas by A19,SETFAM_1:def 9;
hence x in Intersect bas by A19,A20,SETFAM_1:def 1;
end;
end;
hence x in Intersect bas;
let S be Subset of L;
assume that
A21: S is open and
A22: x in S;
reconsider S9 = S as Element of IPs by A2,A21,Th24;
consider X being Subset of IPs such that
A23: S9 = sup X and
A24: for x being Element of IPs st x in X holds x is co-prime by A1,A17;
S9 = union X by A23,YELLOW_1:22;
then consider V being set such that
A25: x in V and
A26: V in X by A22,TARSKI:def 4;
V in sigma L by A2,A26;
then reconsider V as Subset of L;
reconsider Vp = V as Element of IPs by A26;
take V;
Vp is co-prime by A24,A26;
hence V in bas by A1,A25;
sup X is_>=_than X by YELLOW_0:32;
then Vp <= sup X by A26,LATTICE3:def 9;
hence thesis by A23,YELLOW_1:3;
end;
hence thesis by A18;
end;
then reconsider bas as Basis of x;
take bas;
let V be Subset of L;
assume V in bas;
then ex Vp being Element of InclPoset sigma L st V = Vp & x in Vp & Vp is
co-prime;
hence thesis by A1,A2,Th24,Th27;
end;
theorem :: Theorem 1.14 (5) iff (6) p. 107
(for V ex VV st V = sup VV & for W st W in 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 in
the carrier of CompactSublatt L}
proof
set P = {uparrow k where k is Element of L : k in the carrier of
CompactSublatt L};
P c= bool the carrier of L
proof
let x be object;
assume x in P;
then ex k being Element of L st x = uparrow k & k in the carrier of
CompactSublatt L;
hence thesis;
end;
then reconsider P as Subset-Family of L;
reconsider P as Subset-Family of L;
A1: P c= the topology of L
proof
let x be object;
assume x in P;
then consider k being Element of L such that
A2: x = uparrow k and
A3: k in the carrier of CompactSublatt L;
k is compact by A3,WAYBEL_8:def 1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
hence thesis by A2,PRE_TOPC:def 2;
end;
assume
A4: L is algebraic;
now
let x be Point of L;
set B = {uparrow k where k is Element of L : uparrow k in P & x in uparrow
k};
B c= bool the carrier of L
proof
let y be object;
assume y in B;
then ex k being Element of L st y = uparrow k & uparrow k in P & x in
uparrow k;
hence thesis;
end;
then reconsider B as Subset-Family of L;
reconsider B as Subset-Family of L;
B is Basis of x
proof
A5: B is open
proof
let y be Subset of L;
assume y in B;
then ex k being Element of L st y = uparrow k & uparrow k in P & x in
uparrow k;
hence thesis by A1,PRE_TOPC:def 2;
end;
B is x-quasi_basis
proof
now
per cases;
suppose
B is empty;
then Intersect B = the carrier of L by SETFAM_1:def 9;
hence x in Intersect B;
end;
suppose
A6: B is non empty;
A7: now
let Y be set;
assume Y in B;
then
ex k being Element of L st Y = uparrow k & uparrow k in P & x
in uparrow k;
hence x in Y;
end;
Intersect B = meet B by A6,SETFAM_1:def 9;
hence x in Intersect B by A6,A7,SETFAM_1:def 1;
end;
end;
hence x in Intersect B;
reconsider x9 = x as Element of L;
let S be Subset of L such that
A8: S is open and
A9: x in S;
A10: x = sup compactbelow x9 by A4,WAYBEL_8:def 3;
S is inaccessible by A8,WAYBEL11:def 4;
then (compactbelow x9) meets S by A9,A10,WAYBEL11:def 1;
then consider k being object such that
A11: k in compactbelow x9 and
A12: k in S by XBOOLE_0:3;
reconsider k as Element of L by A11;
A13: compactbelow x9 = downarrow x9 /\ the carrier of CompactSublatt L
by WAYBEL_8:5;
then k in downarrow x9 by A11,XBOOLE_0:def 4;
then k <= x9 by WAYBEL_0:17;
then
A14: x in uparrow k by WAYBEL_0:18;
take V = uparrow k;
k in the carrier of CompactSublatt L by A11,A13,XBOOLE_0:def 4;
then uparrow k in P;
hence V in B by A14;
S is upper by A8,WAYBEL11:def 4;
hence thesis by A12,WAYBEL11:42;
end;
hence thesis by A5;
end;
then reconsider B as Basis of x;
take B;
thus B c= P
proof
let y be object;
assume y in B;
then ex k being Element of L st y = uparrow k & uparrow k in P & x in
uparrow k;
hence thesis;
end;
end;
then P is Basis of L by A1,YELLOW_8:14;
hence thesis;
end;
theorem :: Corollary 1.15 (2) implies (3) p. 108
(ex B being Basis of L st B = {uparrow x :x in the carrier of
CompactSublatt L}) implies InclPoset sigma L is algebraic & for V ex VV st V =
sup VV & for W st W in 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 in the carrier of
CompactSublatt L};
set IPs = InclPoset sigma L;
set IPt = InclPoset the topology of L;
A2: the carrier of IPs = sigma L by YELLOW_1:1;
A3: sigma L = the topology of L by Th23;
A4: IPs = IPt by Th23;
thus InclPoset sigma L is algebraic
proof
thus for X being Element of IPs holds compactbelow X is non empty directed
by A3;
thus IPs is up-complete by A4;
let X be Element of IPs;
set cX = compactbelow X;
set GB = { G where G is Subset of L: G in B & G c= X };
X in sigma L by A2;
then reconsider X9 = X as Subset of L;
X9 is open by A2,Th24;
then
A5: X = union GB by YELLOW_8:9;
A6: now
let x be object;
hereby
assume x in X;
then consider GG being set such that
A7: x in GG and
A8: GG in GB by A5,TARSKI:def 4;
consider G being Subset of L such that
A9: G = GG and
A10: G in B and
A11: G c= X by A8;
consider k being Element of L such that
A12: G = uparrow k and
A13: k in the carrier of CompactSublatt L by A1,A10;
k is compact by A13,WAYBEL_8:def 1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
then reconsider G as Element of IPs by A3,A2,A12,PRE_TOPC:def 2;
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
A14: G is compact by A3,A12,WAYBEL_3:36;
G <= X by A11,YELLOW_1:3;
then G in cX by A14;
hence x in union cX by A7,A9,TARSKI:def 4;
end;
assume x in union cX;
then consider G being set such that
A15: x in G and
A16: G in cX by TARSKI:def 4;
reconsider G as Element of IPs by A16;
G <= X by A16,WAYBEL_8:4;
then G c= X by YELLOW_1:3;
hence x in X by A15;
end;
sup cX = union cX by A3,YELLOW_1:22;
hence thesis by A6,TARSKI:2;
end;
let V be Element of InclPoset sigma L;
V in sigma L by A2;
then reconsider V9 = V as Subset of L;
set GB = { G where G is Subset of L: G in B & G c= V };
GB c= the carrier of IPs
proof
let x be object;
assume x in GB;
then consider G being Subset of L such that
A17: G = x and
A18: G in B and
G c= V;
G is open by A18,YELLOW_8:10;
hence thesis by A2,A17,Th24;
end;
then reconsider GB as Subset of InclPoset sigma L;
take GB;
V9 is open by A2,Th24;
then V = union GB by YELLOW_8:9;
hence V = sup GB by A3,YELLOW_1:22;
let x be Element of InclPoset sigma L;
assume x in GB;
then consider G being Subset of L such that
A19: G = x and
A20: G in B and
G c= V;
ex k being Element of L st G = uparrow k & k in the carrier of
CompactSublatt L by A1,A20;
hence thesis by A19,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 in VV holds W is co-prime) implies ex B being Basis of L st B = {uparrow x :
x in the carrier of CompactSublatt L}
proof
set IPt = InclPoset the topology of L;
set IPs = InclPoset sigma L;
A1: the carrier of IPs = sigma L by YELLOW_1:1;
set B = {uparrow k where k is Element of L : k in the carrier of
CompactSublatt L};
B c= bool the carrier of L
proof
let x be object;
assume x in B;
then ex k being Element of L st x = uparrow k & k in the carrier of
CompactSublatt L;
hence thesis;
end;
then reconsider B as Subset-Family of L;
assume that
A2: InclPoset sigma L is algebraic and
A3: 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
in X holds x is co-prime;
IPs = IPt by Th23;
then reconsider ips = InclPoset sigma L as algebraic LATTICE by A2;
reconsider B as Subset-Family of L;
A4: B c= the topology of L
proof
let x be object;
assume x in B;
then consider k being Element of L such that
A5: x = uparrow k and
A6: k in the carrier of CompactSublatt L;
k is compact by A6,WAYBEL_8:def 1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
hence thesis by A5,PRE_TOPC:def 2;
end;
A7: sigma L = the topology of L by Th23;
ips is continuous & for x being Element of L ex X being Basis of x st
for Y being Subset of L st Y in X holds Y is open filtered by A3,Th39;
then
for x being Element of L holds x = "\/" ({inf V where V is Subset of L :
x in V & V in sigma L}, L) by Th37;
then
A8: L is continuous by Th38;
now
let x be Point of L;
set Bx = {uparrow k where k is Element of L : uparrow k in B & x in
uparrow k};
Bx c= bool the carrier of L
proof
let y be object;
assume y in Bx;
then ex k being Element of L st y = uparrow k & uparrow k in B & x in
uparrow k;
hence thesis;
end;
then reconsider Bx as Subset-Family of L;
reconsider Bx as Subset-Family of L;
Bx is Basis of x
proof
A9: Bx is open
proof
let y be Subset of L;
assume y in Bx;
then ex k being Element of L st y = uparrow k & uparrow k in B & x in
uparrow k;
hence thesis by A4,PRE_TOPC:def 2;
end;
Bx is x-quasi_basis
proof
now
per cases;
suppose
Bx is empty;
then Intersect Bx = the carrier of L by SETFAM_1:def 9;
hence x in Intersect Bx;
end;
suppose
A10: Bx is non empty;
A11: now
let Y be set;
assume Y in Bx;
then
ex k being Element of L st Y = uparrow k & uparrow k in B & x
in uparrow k;
hence x in Y;
end;
Intersect Bx = meet Bx by A10,SETFAM_1:def 9;
hence x in Intersect Bx by A10,A11,SETFAM_1:def 1;
end;
end;
hence x in Intersect Bx;
let S be Subset of L such that
A12: S is open and
A13: x in S;
reconsider S9 = S as Element of IPt by A7,A1,A12,PRE_TOPC:def 2;
S9 = sup compactbelow S9 by A2,A7,WAYBEL_8:def 3;
then S9 = union compactbelow S9 by YELLOW_1:22;
then consider UA being set such that
A14: x in UA and
A15: UA in compactbelow S9 by A13,TARSKI:def 4;
reconsider UA as Element of IPt by A15;
UA is compact by A15,WAYBEL_8:4;
then
A16: UA << UA;
UA in the topology of L by A7,A1;
then reconsider UA9 = UA as Subset of L;
UA <= S9 by A15,WAYBEL_8:4;
then
A17: UA c= S by YELLOW_1:3;
consider F being Subset of InclPoset sigma L such that
A18: UA = sup F and
A19: for x being Element of InclPoset sigma L st x in F holds x is
co-prime by A3,A7;
reconsider F9 = F as Subset-Family of L by A1,XBOOLE_1:1;
A20: UA = union F by A7,A18,YELLOW_1:22;
F9 is open
by A7,A1,PRE_TOPC:def 2;
then consider G being finite Subset of F9 such that
A21: UA c= union G by A20,A16,WAYBEL_3:34;
union G c= union F by ZFMISC_1:77;
then
A22: UA = union G by A20,A21;
reconsider G as finite Subset-Family of L by XBOOLE_1:1;
consider Gg being finite Subset-Family of L such that
A23: Gg c= G and
A24: union Gg = union G and
A25: for g being Subset of L st g in Gg holds not g c= union (Gg\{g} ) by Th1;
consider U1 being set such that
A26: x in U1 and
A27: U1 in Gg by A14,A21,A24,TARSKI:def 4;
A28: Gg c= F by A23,XBOOLE_1:1;
then U1 in F by A27;
then reconsider U1 as Element of IPs;
U1 in the topology of L by A7,A1;
then reconsider U19 = U1 as Subset of L;
set k = inf U19;
A29: U19 c= uparrow k
proof
let x be object;
assume
A30: x in U19;
then reconsider x9 = x as Element of L;
k is_<=_than U19 by YELLOW_0:33;
then k <= x9 by A30,LATTICE3:def 8;
hence thesis by WAYBEL_0:18;
end;
U1 is co-prime by A19,A27,A28;
then
A31: U19 is filtered upper by Th27;
now
set D = {(downarrow u)` where u is Element of L : u in U19};
A32: D c= the topology of L
proof
let d be object;
assume d in D;
then consider u being Element of L such that
A33: d = (downarrow u)` and
u in U19;
(downarrow u)` is open by WAYBEL11:12;
hence thesis by A33,PRE_TOPC:def 2;
end;
consider u being set such that
A34: u in U19 by A26;
reconsider u as Element of L by A34;
(downarrow u)` in D by A34;
then reconsider D as non empty Subset of IPt by A32,YELLOW_1:1;
assume
A35: not k in U19;
now
assume not UA c= union D;
then consider l being object such that
A36: l in UA9 and
A37: not l in union D;
reconsider l as Element of L by A36;
consider Uk being set such that
A38: l in Uk and
A39: Uk in Gg by A21,A24,A36,TARSKI:def 4;
A40: Gg c= F by A23,XBOOLE_1:1;
then Uk in F by A39;
then reconsider Uk as Element of IPs;
Uk in the topology of L by A7,A1;
then reconsider Uk9 = Uk as Subset of L;
Uk is co-prime by A19,A39,A40;
then
A41: Uk9 is filtered upper by Th27;
now
assume not l is_<=_than U19;
then consider m being Element of L such that
A42: m in U19 and
A43: not l <= m by LATTICE3:def 8;
(downarrow m)` in D by A42;
then not l in (downarrow m)` by A37,TARSKI:def 4;
then l in downarrow m by XBOOLE_0:def 5;
hence contradiction by A43,WAYBEL_0:17;
end;
then l <= k by YELLOW_0:33;
then
A44: k in Uk9 by A38,A41;
A45: k is_<=_than U19 by YELLOW_0:33;
A46: U19 c= Uk
proof
let u be object;
assume
A47: u in U19;
then reconsider d = u as Element of L;
k <= d by A45,A47,LATTICE3:def 8;
hence thesis by A41,A44;
end;
U19 c= union (Gg\{U19})
proof
let u be object;
assume
A48: u in U19;
Uk in Gg\{U19} by A35,A39,A44,ZFMISC_1:56;
hence thesis by A46,A48,TARSKI:def 4;
end;
hence contradiction by A25,A27;
end;
then UA c= sup D by YELLOW_1:22;
then
A49: UA <= sup D by YELLOW_1:3;
D is directed by A7,A31,Th25;
then consider d being Element of IPt such that
A50: d in D and
A51: UA <= d by A16,A49;
consider u being Element of L such that
A52: d = (downarrow u)` and
A53: u in U19 by A50;
U1 c= UA by A20,A27,A28,ZFMISC_1:74;
then
A54: u in UA by A53;
A55: u <= u;
UA c= d by A51,YELLOW_1:3;
then not u in downarrow u by A52,A54,XBOOLE_0:def 5;
hence contradiction by A55,WAYBEL_0:17;
end;
then uparrow k c= U19 by A31,WAYBEL11:42;
then
A56: U19 = uparrow k by A29;
take V = uparrow k;
U19 is open by A7,A1,PRE_TOPC:def 2;
then U19 is Open by A8,A31,WAYBEL11:46;
then k is compact by A56,WAYBEL_8:2;
then k in the carrier of CompactSublatt L by WAYBEL_8:def 1;
then uparrow k in B;
hence V in Bx by A26,A29;
U1 c= UA by A22,A24,A27,ZFMISC_1:74;
hence thesis by A56,A17;
end;
hence thesis by A9;
end;
then reconsider Bx as Basis of x;
take Bx;
thus Bx c= B
proof
let y be object;
assume y in Bx;
then ex k being Element of L st y = uparrow k & uparrow k in B & x in
uparrow k;
hence thesis;
end;
end;
then reconsider B as Basis of L by A4,YELLOW_8:14;
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 in 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 in 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
for z be Element of L st z in dx holds z <= x by WAYBEL_0:17;
then x is_>=_than dx by LATTICE3:def 9;
then
A2: sup dx <= x by YELLOW_0:32;
set GB = { G where G is Subset of L: G in B & G c= dy`};
A3: cx = dx /\ the carrier of CompactSublatt L by WAYBEL_8:5;
A4: y is_>=_than cx by YELLOW_0:32;
ex_sup_of cx, L & ex_sup_of dx, L by YELLOW_0:17;
then sup compactbelow x <= sup dx by A3,XBOOLE_1:17,YELLOW_0:34;
then
A5: y <= x by A2,ORDERS_2:3;
assume
A6: y <> x;
now
assume x in dy;
then x <= y by WAYBEL_0:17;
hence contradiction by A6,A5,ORDERS_2:2;
end;
then
A7: x in dy` by XBOOLE_0:def 5;
dy` = union GB by WAYBEL11:12,YELLOW_8:9;
then consider X being set such that
A8: x in X and
A9: X in GB by A7,TARSKI:def 4;
consider G being Subset of L such that
A10: G = X and
A11: G in B and
A12: G c= dy` by A9;
consider k being Element of L such that
A13: G = uparrow k and
A14: k in the carrier of CompactSublatt L by A1,A11;
A15: k is compact by A14,WAYBEL_8:def 1;
k <= x by A8,A10,A13,WAYBEL_0:18;
then k in cx by A15;
then k <= y by A4,LATTICE3:def 9;
then y in uparrow k by WAYBEL_0:18;
then y <= y & not y in dy by A12,A13,XBOOLE_0:def 5;
hence contradiction by WAYBEL_0:17;
end;
hence thesis;
end;