let L be complete Scott TopLattice; :: thesis: ( L is continuous implies ( L is compact & L is locally-compact & L is sober & L is Baire ) )
assume A1:
L is continuous
; :: thesis: ( L is compact & L is locally-compact & L is sober & L is Baire )
A2:
uparrow (Bottom L) = the carrier of L
by Th10;
A3:
for X being Subset of L st X is open holds
X is upper
by WAYBEL11:def 4;
then A4:
uparrow (Bottom L) is compact
by Th22;
[#] L = the carrier of L
;
hence
L is compact
by A2, A4, COMPTS_1:10; :: thesis: ( L is locally-compact & L is sober & L is Baire )
thus A5:
L is locally-compact
:: thesis: ( L is sober & L is Baire )proof
let x be
Point of
L;
:: according to WAYBEL_3:def 9 :: thesis: for b1 being Element of bool the carrier of L holds
( not x in b1 or not b1 is open or ex b2 being Element of bool the carrier of L st
( x in Int b2 & b2 c= b1 & b2 is compact ) )let X be
Subset of
L;
:: thesis: ( not x in X or not X is open or ex b1 being Element of bool the carrier of L st
( x in Int b1 & b1 c= X & b1 is compact ) )
assume that A6:
x in X
and A7:
X is
open
;
:: thesis: ex b1 being Element of bool the carrier of L st
( x in Int b1 & b1 c= X & b1 is compact )
reconsider x' =
x as
Element of
L ;
set bas =
{ (wayabove q) where q is Element of L : q << x' } ;
A8:
{ (wayabove q) where q is Element of L : q << x' } is
Basis of
x
by A1, WAYBEL11:44;
consider y being
Element of
L such that A9:
(
y << x' &
y in X )
by A1, A6, A7, WAYBEL11:43;
A10:
X is
upper
by A7, WAYBEL11:def 4;
set Y =
uparrow y;
take
uparrow y
;
:: thesis: ( x in Int (uparrow y) & uparrow y c= X & uparrow y is compact )
wayabove y in { (wayabove q) where q is Element of L : q << x' }
by A9;
then A11:
(
wayabove y is
open &
x in wayabove y )
by A8, YELLOW_8:21;
wayabove y c= Int (uparrow y)
by A11, TOPS_1:56, WAYBEL_3:11;
hence
x in Int (uparrow y)
by A11;
:: thesis: ( uparrow y c= X & uparrow y is compact )
thus
uparrow y c= X
by A9, A10, WAYBEL11:42;
:: thesis: uparrow y is compact
thus
uparrow y is
compact
by A3, Th22;
:: thesis: verum
end;
sup_op L is jointly_Scott-continuous
by A1, Th30;
hence
L is sober
by Th31; :: thesis: L is Baire
hence
L is Baire
by A5, WAYBEL12:48; :: thesis: verum