:: The Scott Topology, Part II :: by Czes{\l}aw Byli\'nski and Piotr Rudnicki :: :: Received August 27, 1997 :: Copyright (c) 1997-2021 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; 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;