let L be complete Scott TopLattice; :: thesis: 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 )
let x be Element of L; :: thesis: ( L is continuous implies ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered ) )
set B = { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } ;
{ V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } c= bool the carrier of L
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } or X in bool the carrier of L )
assume X in { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } ; :: thesis: X in bool the carrier of L
then ex V being Subset of L st
( X = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence X in bool the carrier of L ; :: thesis: verum
end;
then reconsider B = { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } as Subset-Family of L ;
reconsider B = B as Subset-Family of L ;
assume A1: L is continuous ; :: thesis: ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
then reconsider A = { (wayabove q) where q is Element of L : q << x } as Basis of x by WAYBEL11:44;
A2: B is Basis of x
proof
A3: B is open
proof
let Y be Subset of L; :: according to TOPS_2:def 1 :: thesis: ( not Y in B or Y is open )
assume Y in B ; :: thesis: Y is open
then ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence Y is open ; :: thesis: verum
end;
B is x -quasi_basis
proof
thus x in Intersect B :: according to YELLOW_8:def 1 :: 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 B & b2 c= b1 ) )
proof
per cases ( B is empty or not B is empty ) ;
suppose A4: not B is empty ; :: thesis: x in Intersect B
A5: now :: thesis: for Y being set st Y in B holds
x in Y
let Y be set ; :: thesis: ( Y in B implies x in Y )
assume Y in B ; :: thesis: x in Y
then ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence x in Y ; :: thesis: verum
end;
Intersect B = meet B by A4, SETFAM_1:def 9;
hence x in Intersect B by A4, A5, SETFAM_1:def 1; :: thesis: verum
end;
end;
end;
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 B & b1 c= S ) )
assume ( S is open & x in S ) ; :: thesis: ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S )
then consider V being Subset of L such that
A6: V in A and
A7: V c= S by YELLOW_8:def 1;
consider q being Element of L such that
A8: V = wayabove q and
A9: q << x by A6;
consider F being Open Filter of L such that
A10: x in F and
A11: F c= wayabove q by A1, A9, WAYBEL_6:8;
take F ; :: thesis: ( F in B & F c= S )
F is open by WAYBEL11:41;
hence F in B by A9, A10, A11; :: thesis: F c= S
thus F c= S by A7, A8, A11; :: thesis: verum
end;
hence B is Basis of x by A3; :: thesis: verum
end;
now :: thesis: for Y being Subset of L st Y in B holds
( Y is open & Y is filtered )
let Y be Subset of L; :: thesis: ( Y in B implies ( Y is open & Y is filtered ) )
assume Y in B ; :: thesis: ( Y is open & Y is filtered )
then ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence ( Y is open & Y is filtered ) ; :: thesis: verum
end;
hence ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered ) by A2; :: thesis: verum