:: The Scott Topology, Part II
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received August 27, 1997
:: Copyright (c) 1997-2016 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, NAT_1;
requirements NUMERALS, BOOLE, SUBSET;
begin :: Preliminaries
theorem :: WAYBEL14:1
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});
theorem :: WAYBEL14:2
for S being 1-sorted, X being Subset of S holds X` = the carrier
of S iff X is empty;
theorem :: WAYBEL14:3
for R being antisymmetric with_infima transitive non empty RelStr
, x, y being Element of R holds downarrow (x"/\"y) = (downarrow x) /\ downarrow
y;
theorem :: WAYBEL14:4
for R being antisymmetric with_suprema transitive non empty RelStr, x,
y being Element of R holds uparrow (x"\/"y) = (uparrow x) /\ uparrow y;
theorem :: WAYBEL14:5
for L being complete antisymmetric non empty RelStr, X being
lower Subset of L st sup X in X holds X = downarrow sup X;
theorem :: WAYBEL14:6
for L being complete antisymmetric non empty RelStr, X being upper
Subset of L st inf X in X holds X = uparrow inf X;
theorem :: WAYBEL14:7
for R being non empty reflexive transitive RelStr, x, y being
Element of R holds x << y iff uparrow y c= wayabove x;
theorem :: WAYBEL14:8
for R being non empty reflexive transitive RelStr, x, y being Element
of R holds x << y iff downarrow x c= waybelow y;
theorem :: WAYBEL14:9
for R being complete reflexive antisymmetric non empty RelStr,
x being Element of R holds sup waybelow x <= x & x <= inf wayabove x;
theorem :: WAYBEL14:10
for L being lower-bounded antisymmetric non empty RelStr holds
uparrow Bottom L = the carrier of L;
theorem :: WAYBEL14:11
for L being upper-bounded antisymmetric non empty RelStr holds
downarrow Top L = the carrier of L;
theorem :: WAYBEL14:12
for P being with_suprema Poset, x, y being Element of P holds (
wayabove x)"\/"(wayabove y) c= uparrow (x"\/"y);
theorem :: WAYBEL14:13
for P being with_infima Poset, x, y being Element of P holds (waybelow
x)"/\"(waybelow y) c= downarrow (x"/\"y);
theorem :: WAYBEL14:14
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;
theorem :: WAYBEL14:15
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
};
theorem :: WAYBEL14:16
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};
registration
let L be sup-Semilattice, x be Element of L;
cluster compactbelow x -> directed;
end;
theorem :: WAYBEL14:17
:: 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;
theorem :: WAYBEL14:18
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;
theorem :: WAYBEL14:19
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;
theorem :: WAYBEL14:20
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;
registration
let T be non empty TopSpace;
cluster InclPoset the topology of T -> distributive;
end;
theorem :: WAYBEL14:21
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;
theorem :: WAYBEL14:22
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;
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;
end;
theorem :: WAYBEL14:23
sigma L = the topology of L;
theorem :: WAYBEL14:24
X in sigma L iff X is open;
theorem :: WAYBEL14:25
for X being filtered Subset of L st VV = {(downarrow x)` : x in
X} holds VV is directed;
theorem :: WAYBEL14:26
X is open & x in X implies inf X << x;
:: p. 105
definition
let R be non empty reflexive RelStr, f be Function of [:R, R:], R;
attr f is jointly_Scott-continuous means
:: WAYBEL14:def 1
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 :: WAYBEL14:27 :: Proposition 1.11 (i) p. 105
V = X implies (V is co-prime iff X is filtered upper);
theorem :: WAYBEL14:28 :: Proposition 1.11 (ii) p. 105
(V = X & ex x st X = (downarrow x)`) implies V is prime & V <> the
carrier of L;
theorem :: WAYBEL14:29 :: 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)`;
theorem :: WAYBEL14:30 :: Proposition 1.11 (iv) p. 105
L is continuous implies sup_op L is jointly_Scott-continuous;
theorem :: WAYBEL14:31 :: Corollary 1.12 p. 106
sup_op L is jointly_Scott-continuous implies L is sober;
theorem :: WAYBEL14:32 :: Corollary 1.13 p. 106
L is continuous implies L is compact locally-compact sober Baire;
theorem :: WAYBEL14:33 :: Theorem 1.14 (1) implies (2) p. 107
L is continuous & X in sigma L implies X = union {wayabove x : x in X};
theorem :: WAYBEL14:34 :: 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;
theorem :: WAYBEL14:35 :: 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;
theorem :: WAYBEL14:36 :: Theorem 1.14 (1) implies (3 second conjunct) p. 107
L is continuous implies InclPoset sigma L is continuous;
theorem :: WAYBEL14:37 :: 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);
theorem :: WAYBEL14:38 :: 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;
theorem :: WAYBEL14:39 :: 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;
theorem :: WAYBEL14:40 :: 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;
theorem :: WAYBEL14:41 :: 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;
theorem :: WAYBEL14:42 :: 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};
theorem :: WAYBEL14:43 :: 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;
theorem :: WAYBEL14:44 :: 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};
theorem :: WAYBEL14:45 :: 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;