let L be complete Scott TopLattice; :: thesis: ( 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 ) ) ) implies ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } )
assume that
A1:
InclPoset (sigma L) is algebraic
and
A2:
for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for x being Element of (InclPoset (sigma L)) st x in X holds
x is co-prime ) )
; :: thesis: ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
set IPt = InclPoset the topology of L;
set IPs = InclPoset (sigma L);
A3:
sigma L = the topology of L
by Th23;
A4:
the carrier of (InclPoset (sigma L)) = sigma L
by YELLOW_1:1;
A5:
InclPoset (sigma L) = InclPoset the topology of L
by Th23;
reconsider ips = InclPoset (sigma L) as algebraic LATTICE by A1, A5;
A7:
ips is continuous
;
for x being Element of L ex X being Basis of x st
for Y being Subset of L st Y in X holds
( Y is open & Y is filtered )
by A2, Th39;
then
for x being Element of L holds x = "\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L
by A7, Th37;
then A8:
L is continuous
by Th38;
set B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ;
{ (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } c= bool the carrier of L
then reconsider B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } as Subset-Family of L ;
reconsider B = B as Subset-Family of L ;
A9:
B c= the topology of L
now let x be
Point of
L;
:: thesis: ex Bx being Basis of x st Bx c= Bset Bx =
{ (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } ;
{ (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } c= bool the
carrier of
L
then reconsider Bx =
{ (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } as
Subset-Family of
L ;
reconsider Bx =
Bx as
Subset-Family of
L ;
Bx is
Basis of
x
proof
thus
Bx c= the
topology of
L
:: according to YELLOW_8:def 2 :: thesis: ( x in Intersect Bx & ( for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in Bx & b2 c= b1 ) ) ) )
hence
x in Intersect Bx
;
:: thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in Bx & b2 c= b1 ) )
let S be
Subset of
L;
:: thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in Bx & b1 c= S ) )
assume that A13:
S is
open
and A14:
x in S
;
:: thesis: ex b1 being Element of bool the carrier of L st
( b1 in Bx & b1 c= S )
reconsider S' =
S as
Element of
(InclPoset the topology of L) by A3, A4, A13, PRE_TOPC:def 5;
S' = sup (compactbelow S')
by A3, A1, WAYBEL_8:def 3;
then
S' = union (compactbelow S')
by YELLOW_1:22;
then consider UA being
set such that A15:
(
x in UA &
UA in compactbelow S' )
by A14, TARSKI:def 4;
reconsider UA =
UA as
Element of
(InclPoset the topology of L) by A15;
A16:
(
UA <= S' &
UA is
compact )
by A15, WAYBEL_8:4;
consider F being
Subset of
(InclPoset (sigma L)) such that A17:
UA = sup F
and A18:
for
x being
Element of
(InclPoset (sigma L)) st
x in F holds
x is
co-prime
by A2, A3;
A19:
UA = union F
by A3, A17, YELLOW_1:22;
UA in the
topology of
L
by A3, A4;
then reconsider UA' =
UA as
Subset of
L ;
A20:
UA << UA
by A16, WAYBEL_3:def 2;
reconsider F' =
F as
Subset-Family of
L by A4, XBOOLE_1:1;
F' is
open
then consider G being
finite Subset of
F' such that A21:
UA c= union G
by A19, A20, WAYBEL_3:34;
union G c= union F
by ZFMISC_1:95;
then A22:
UA = union G
by A19, A21, XBOOLE_0:def 10;
reconsider G =
G as
finite Subset-Family of
L by XBOOLE_1:1;
consider Gg being
finite Subset-Family of
L such that A23:
Gg c= G
and A24:
union Gg = union G
and A25:
for
g being
Subset of
L st
g in Gg holds
not
g c= union (Gg \ {g})
by Th1;
consider U1 being
set such that A26:
(
x in U1 &
U1 in Gg )
by A15, A21, A24, TARSKI:def 4;
A27:
Gg c= F
by A23, XBOOLE_1:1;
then
U1 in F
by A26;
then reconsider U1 =
U1 as
Element of
(InclPoset (sigma L)) ;
U1 in the
topology of
L
by A3, A4;
then reconsider U1' =
U1 as
Subset of
L ;
U1 is
co-prime
by A18, A26, A27;
then A28:
(
U1' is
filtered &
U1' is
upper )
by Th27;
set k =
inf U1';
now assume A29:
not
inf U1' in U1'
;
:: thesis: contradictionset D =
{ ((downarrow u) ` ) where u is Element of L : u in U1' } ;
consider u being
set such that A30:
u in U1'
by A26;
reconsider u =
u as
Element of
L by A30;
A31:
(downarrow u) ` in { ((downarrow u) ` ) where u is Element of L : u in U1' }
by A30;
{ ((downarrow u) ` ) where u is Element of L : u in U1' } c= the
topology of
L
then reconsider D =
{ ((downarrow u) ` ) where u is Element of L : u in U1' } as non
empty Subset of
(InclPoset the topology of L) by A31, YELLOW_1:1;
A33:
D is
directed
by A3, A28, Th25;
now assume
not
UA c= union D
;
:: thesis: contradictionthen consider l being
set such that A34:
(
l in UA' & not
l in union D )
by TARSKI:def 3;
reconsider l =
l as
Element of
L by A34;
consider Uk being
set such that A35:
(
l in Uk &
Uk in Gg )
by A21, A24, A34, TARSKI:def 4;
A36:
Gg c= F
by A23, XBOOLE_1:1;
then
Uk in F
by A35;
then reconsider Uk =
Uk as
Element of
(InclPoset (sigma L)) ;
Uk in the
topology of
L
by A3, A4;
then reconsider Uk' =
Uk as
Subset of
L ;
Uk is
co-prime
by A18, A35, A36;
then A37:
(
Uk' is
filtered &
Uk' is
upper )
by Th27;
A38:
inf U1' is_<=_than U1'
by YELLOW_0:33;
then
l <= inf U1'
by YELLOW_0:33;
then A40:
inf U1' in Uk'
by A35, A37, WAYBEL_0:def 20;
A41:
U1' c= Uk
U1' c= union (Gg \ {U1'})
hence
contradiction
by A25, A26;
:: thesis: verum end; then
UA c= sup D
by YELLOW_1:22;
then
UA <= sup D
by YELLOW_1:3;
then consider d being
Element of
(InclPoset the topology of L) such that A44:
d in D
and A45:
UA <= d
by A20, A33, WAYBEL_3:def 1;
consider u being
Element of
L such that A46:
(
d = (downarrow u) ` &
u in U1' )
by A44;
U1 c= UA
by A19, A26, A27, ZFMISC_1:92;
then A47:
u in UA
by A46;
UA c= d
by A45, YELLOW_1:3;
then A48:
not
u in downarrow u
by A46, A47, XBOOLE_0:def 5;
u <= u
;
hence
contradiction
by A48, WAYBEL_0:17;
:: thesis: verum end;
then A49:
uparrow (inf U1') c= U1'
by A28, WAYBEL11:42;
A50:
U1' c= uparrow (inf U1')
then A52:
U1' = uparrow (inf U1')
by A49, XBOOLE_0:def 10;
U1' is
open
by A3, A4, PRE_TOPC:def 5;
then
U1' is
Open
by A8, A28, WAYBEL11:46;
then A53:
inf U1' is
compact
by A52, WAYBEL_8:2;
take V =
uparrow (inf U1');
:: thesis: ( V in Bx & V c= S )
inf U1' in the
carrier of
(CompactSublatt L)
by A53, WAYBEL_8:def 1;
then
uparrow (inf U1') in B
;
hence
V in Bx
by A26, A50;
:: thesis: V c= S
A54:
UA c= S
by A16, YELLOW_1:3;
U1 c= UA
by A22, A24, A26, ZFMISC_1:92;
hence
V c= S
by A52, A54, XBOOLE_1:1;
:: thesis: verum
end; then reconsider Bx =
Bx as
Basis of
x ;
take Bx =
Bx;
:: thesis: Bx c= Bthus
Bx c= B
:: thesis: verum end;
then reconsider B = B as Basis of L by A9, YELLOW_8:23;
take
B
; :: thesis: B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
thus
B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
; :: thesis: verum