:: The Scott Topology, Part II :: by Czes{\l}aw Byli\'nski and Piotr Rudnicki :: :: Received August 27, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users begin theorem Th1: :: WAYBEL14:1 for X being set for 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}) ) ) proofend; Lm1: for S being 1-sorted for X, Y being Subset of S holds ( X c= Y ` iff Y c= X ` ) proofend; theorem Th2: :: WAYBEL14:2 for S being 1-sorted for X being Subset of S holds ( X ` = the carrier of S iff X is empty ) proofend; theorem Th3: :: WAYBEL14:3 for R being non empty transitive antisymmetric with_infima RelStr for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y) proofend; theorem :: WAYBEL14:4 for R being non empty transitive antisymmetric with_suprema RelStr for x, y being Element of R holds uparrow (x "\/" y) = (uparrow x) /\ (uparrow y) proofend; theorem Th5: :: WAYBEL14:5 for L being non empty antisymmetric complete RelStr for X being lower Subset of L st sup X in X holds X = downarrow (sup X) proofend; theorem :: WAYBEL14:6 for L being non empty antisymmetric complete RelStr for X being upper Subset of L st inf X in X holds X = uparrow (inf X) proofend; theorem Th7: :: WAYBEL14:7 for R being non empty reflexive transitive RelStr for x, y being Element of R holds ( x << y iff uparrow y c= wayabove x ) proofend; theorem :: WAYBEL14:8 for R being non empty reflexive transitive RelStr for x, y being Element of R holds ( x << y iff downarrow x c= waybelow y ) proofend; theorem Th9: :: WAYBEL14:9 for R being non empty reflexive antisymmetric complete RelStr for x being Element of R holds ( sup (waybelow x) <= x & x <= inf (wayabove x) ) proofend; theorem Th10: :: WAYBEL14:10 for L being non empty antisymmetric lower-bounded RelStr holds uparrow (Bottom L) = the carrier of L proofend; theorem :: WAYBEL14:11 for L being non empty antisymmetric upper-bounded RelStr holds downarrow (Top L) = the carrier of L proofend; theorem Th12: :: WAYBEL14:12 for P being with_suprema Poset for x, y being Element of P holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y) proofend; theorem :: WAYBEL14:13 for P being with_infima Poset for x, y being Element of P holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y) proofend; theorem Th14: :: WAYBEL14:14 for R being non empty with_suprema Poset for l being Element of R holds ( l is co-prime iff for x, y being Element of R holds ( not l <= x "\/" y or l <= x or l <= y ) ) proofend; theorem Th15: :: WAYBEL14:15 for P being non empty complete Poset for V being non empty Subset of P holds downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V } proofend; theorem :: WAYBEL14:16 for P being non empty complete Poset for V being non empty Subset of P holds uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V } proofend; registration let L be sup-Semilattice; let x be Element of L; cluster compactbelow x -> directed ; coherence compactbelow x is directed proofend; end; theorem Th17: :: WAYBEL14:17 for T being non empty TopSpace for S being irreducible Subset of T for V being Element of (InclPoset the topology of T) st V = S ` holds V is prime proofend; theorem Th18: :: WAYBEL14:18 for T being non empty TopSpace for x, y being Element of (InclPoset the topology of T) holds ( x "\/" y = x \/ y & x "/\" y = x /\ y ) proofend; theorem Th19: :: WAYBEL14:19 for T being non empty TopSpace for 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) holds ( not X /\ Y c= V or X c= V or Y c= V ) ) proofend; theorem :: WAYBEL14:20 for T being non empty TopSpace for 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) holds ( not V c= X \/ Y or V c= X or V c= Y ) ) proofend; registration let T be non empty TopSpace; cluster InclPoset the topology of T -> distributive ; coherence InclPoset the topology of T is distributive proofend; end; theorem Th21: :: WAYBEL14:21 for T being non empty TopSpace for L being TopLattice for t being Point of T for l being Point of L for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds X is Basis of t proofend; theorem Th22: :: WAYBEL14:22 for L being TopLattice for 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 proofend; begin registration let L be complete LATTICE; cluster sigma L -> non empty ; coherence not sigma L is empty proofend; end; theorem Th23: :: WAYBEL14:23 for L being complete Scott TopLattice holds sigma L = the topology of L proofend; theorem Th24: :: WAYBEL14:24 for L being complete Scott TopLattice for X being Subset of L holds ( X in sigma L iff X is open ) proofend; Lm2: for L being complete Scott TopLattice for V being filtered Subset of L for F being Subset-Family of L for 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 proofend; theorem Th25: :: WAYBEL14:25 for L being complete Scott TopLattice for VV being Subset of (InclPoset (sigma L)) for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds VV is directed proofend; theorem Th26: :: WAYBEL14:26 for L being complete Scott TopLattice for x being Element of L for X being Subset of L st X is open & x in X holds inf X << x proofend; :: p. 105 definition let R be non empty reflexive RelStr ; let f be Function of [:R,R:],R; attrf is jointly_Scott-continuous means :Def1: :: WAYBEL14:def 1 for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds ex ft being Function of [:T,T:],T st ( ft = f & ft is continuous ); end; :: deftheorem Def1 defines jointly_Scott-continuous WAYBEL14:def_1_:_ for R being non empty reflexive RelStr for f being Function of [:R,R:],R holds ( f is jointly_Scott-continuous iff for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds ex ft being Function of [:T,T:],T st ( ft = f & ft is continuous ) ); theorem Th27: :: WAYBEL14:27 for L being complete Scott TopLattice for X being Subset of L for V being Element of (InclPoset (sigma L)) st V = X holds ( V is co-prime iff ( X is filtered & X is upper ) ) proofend; theorem :: WAYBEL14:28 for L being complete Scott TopLattice for X being Subset of L for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds ( V is prime & V <> the carrier of L ) proofend; theorem Th29: :: WAYBEL14:29 for L being complete Scott TopLattice for X being Subset of L for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds ex x being Element of L st X = (downarrow x) ` proofend; theorem Th30: :: WAYBEL14:30 for L being complete Scott TopLattice st L is continuous holds sup_op L is jointly_Scott-continuous proofend; theorem Th31: :: WAYBEL14:31 for L being complete Scott TopLattice st sup_op L is jointly_Scott-continuous holds L is sober proofend; theorem :: WAYBEL14:32 for L being complete Scott TopLattice st L is continuous holds ( L is compact & L is locally-compact & L is sober & L is Baire ) proofend; theorem Th33: :: WAYBEL14:33 for L being complete Scott TopLattice for X being Subset of L st L is continuous & X in sigma L holds X = union { (wayabove x) where x is Element of L : x in X } proofend; theorem :: WAYBEL14:34 for L being complete Scott TopLattice st ( 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 } ) holds L is continuous proofend; theorem :: WAYBEL14:35 for L being complete Scott TopLattice for x being Element of L st L is continuous holds ex B being Basis of x st for X being Subset of L st X in B holds ( X is open & X is filtered ) proofend; theorem :: WAYBEL14:36 for L being complete Scott TopLattice st L is continuous holds InclPoset (sigma L) is continuous proofend; theorem Th37: :: WAYBEL14:37 for L being complete Scott TopLattice for x being Element of L st ( 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 & Y is filtered ) ) & InclPoset (sigma L) is continuous holds x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L) proofend; theorem Th38: :: WAYBEL14:38 for L being complete Scott TopLattice st ( for x being Element of L holds x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L) ) holds L is continuous proofend; theorem Th39: :: WAYBEL14:39 for L being complete Scott TopLattice holds ( ( 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 & Y is filtered ) ) iff for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st ( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds W is co-prime ) ) ) proofend; theorem :: WAYBEL14:40 for L being complete Scott TopLattice holds ( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st ( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive ) proofend; theorem :: WAYBEL14:41 for L being complete Scott TopLattice holds ( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) ) proofend; theorem :: WAYBEL14:42 for L being complete Scott TopLattice st L is algebraic holds ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } proofend; theorem :: WAYBEL14:43 for L being complete Scott TopLattice st ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } holds ( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st ( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds W is co-prime ) ) ) ) proofend; theorem :: WAYBEL14:44 for L being complete Scott TopLattice st InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st ( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds W is co-prime ) ) ) holds ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } proofend; theorem :: WAYBEL14:45 for L being complete Scott TopLattice st ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } holds L is algebraic proofend;