:: 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;