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

proof end;

Lm1: for S being 1-sorted
for X, Y being Subset of S holds
( X c= Y ` iff Y c= X ` )

proof end;

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 )

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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 )

proof end;

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 )

proof end;

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) )

proof end;

theorem Th10: :: WAYBEL14:10

for L being non empty antisymmetric lower-bounded RelStr holds uparrow (Bottom L) = the carrier of L

proof end;

theorem :: WAYBEL14:11

for L being non empty antisymmetric upper-bounded RelStr holds downarrow (Top L) = the carrier of L

proof end;

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)

proof end;

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)

proof end;

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 ) )

proof end;

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 }

proof end;

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 }

proof end;

registration

let L be sup-Semilattice;
let x be Element of L;
cluster compactbelow x -> directed ;
coherence
compactbelow x is directed

proof end;

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

proof end;

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 )

proof end;

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 ) )

proof end;

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 ) )

proof end;

registration

let T be non empty TopSpace;
cluster InclPoset the topology of T -> distributive ;
coherence
InclPoset the topology of T is distributive

proof end;

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

proof end;

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

proof end;

begin

registration

let L be complete LATTICE;
cluster sigma L -> non empty ;
coherence
not sigma L is empty

proof end;

end;

theorem Th23: :: WAYBEL14:23

for L being complete Scott TopLattice holds sigma L = the topology of L

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

definition

let R be non empty reflexive RelStr ;
let f be Function of [:R,R:],R;
attr f 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 ) )

proof end;

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 )

proof end;

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) `

proof end;

theorem Th30: :: WAYBEL14:30

for L being complete Scott TopLattice st L is continuous holds
sup_op L is jointly_Scott-continuous

proof end;

theorem Th31: :: WAYBEL14:31

for L being complete Scott TopLattice st sup_op L is jointly_Scott-continuous holds
L is sober

proof end;

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 )

proof end;

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 }

proof end;

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

proof end;

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 )

proof end;

theorem :: WAYBEL14:36

for L being complete Scott TopLattice st L is continuous holds
InclPoset (sigma L) is continuous

proof end;

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)

proof end;

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

proof end;

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 ) ) )

proof end;

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 )

proof end;

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 ) )

proof end;

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) }

proof end;

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 ) ) ) )

proof end;

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) }

proof end;

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

proof end;