let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for T being correct Lawson TopAugmentation of L1
for B1 being with_bottom CLbasis of L1 holds { (Way_Up a,A) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
let T be correct Lawson TopAugmentation of L1; :: thesis: for B1 being with_bottom CLbasis of L1 holds { (Way_Up a,A) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
let B1 be with_bottom CLbasis of L1; :: thesis: { (Way_Up a,A) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
A1:
RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of T,the InternalRel of T #)
by YELLOW_9:def 4;
{ (Way_Up a,A) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= bool the carrier of T
then reconsider WU = { (Way_Up a,A) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } as Subset-Family of T ;
reconsider WU = WU as Subset-Family of T ;
A3:
WU c= the topology of T
now let A be
Subset of
T;
:: thesis: ( A is open implies for pT being Point of T st pT in A holds
ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A ) )assume A7:
A is
open
;
:: thesis: for pT being Point of T st pT in A holds
ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A )let pT be
Point of
T;
:: thesis: ( pT in A implies ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A ) )assume A8:
pT in A
;
:: thesis: ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A )consider S being
Scott TopAugmentation of
T;
A9:
RelStr(# the
carrier of
S,the
InternalRel of
S #)
= RelStr(# the
carrier of
T,the
InternalRel of
T #)
by YELLOW_9:def 4;
reconsider BL =
{ (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } as
Basis of
T by WAYBEL19:32;
consider a being
Subset of
T such that A10:
a in BL
and A11:
pT in a
and A12:
a c= A
by A7, A8, YELLOW_9:31;
consider W,
FT being
Subset of
T such that A13:
a = W \ (uparrow FT)
and A14:
W in sigma T
and A15:
FT is
finite
by A10;
reconsider W1 =
W as
Subset of
S by A9;
sigma S = sigma T
by A9, YELLOW_9:52;
then A16:
W = union { (wayabove x) where x is Element of S : x in W1 }
by A14, WAYBEL14:33;
A17:
(
pT in W & not
pT in uparrow FT )
by A11, A13, XBOOLE_0:def 5;
then consider k being
set such that A18:
pT in k
and A19:
k in { (wayabove x) where x is Element of S : x in W1 }
by A16, TARSKI:def 4;
consider xS being
Element of
S such that A20:
k = wayabove xS
and A21:
xS in W1
by A19;
reconsider pS =
pT as
Element of
S by A9;
reconsider pL =
pS as
Element of
L1 by A1;
reconsider xL =
xS as
Element of
L1 by A1, A9;
reconsider FL =
FT as
Subset of
L1 by A1;
xS << pS
by A18, A20, WAYBEL_3:8;
then A22:
xL << pL
by A1, A9, WAYBEL_8:8;
Bottom L1 in B1
by WAYBEL23:def 8;
then consider bL being
Element of
L1 such that A23:
bL in B1
and A24:
xL <= bL
and A25:
bL << pL
by A22, WAYBEL23:47;
A26:
pL in wayabove bL
by A25, WAYBEL_3:8;
A27:
uparrow FT = uparrow FL
by A1, WAYBEL_0:13;
defpred S1[
set ,
set ]
means ex
b1,
y1 being
Element of
L1 st
(
y1 = $1 &
b1 = $2 &
b1 in B1 & not
b1 <= pL &
b1 << y1 );
A28:
for
y being
set st
y in FL holds
ex
b being
set st
S1[
y,
b]
consider f being
Function such that A33:
dom f = FL
and A34:
for
y being
set st
y in FL holds
S1[
y,
f . y]
from CLASSES1:sch 1(A28);
rng f c= the
carrier of
L1
then reconsider FFL =
rng f as
Subset of
L1 ;
reconsider cT =
(wayabove bL) \ (uparrow FFL) as
Subset of
T by A1;
take cT =
cT;
:: thesis: ( cT in WU & pT in cT & cT c= A )A38:
cT = Way_Up bL,
FFL
;
A39:
FFL is
finite
by A15, A33, FINSET_1:26;
FFL c= B1
hence
cT in WU
by A23, A38, A39;
:: thesis: ( pT in cT & cT c= A )
for
z being
Element of
L1 holds
( not
z in FFL or not
z <= pL )
then
for
z being
Element of
L1 holds
( not
z <= pL or not
z in FFL )
;
then
not
pL in uparrow FFL
by WAYBEL_0:def 16;
hence
pT in cT
by A26, XBOOLE_0:def 5;
:: thesis: cT c= AA48:
wayabove bL c= wayabove xL
by A24, WAYBEL_3:12;
uparrow FL c= uparrow FFL
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in uparrow FL or z in uparrow FFL )
assume A49:
z in uparrow FL
;
:: thesis: z in uparrow FFL
then reconsider z1 =
z as
Element of
L1 ;
consider v1 being
Element of
L1 such that A50:
v1 <= z1
and A51:
v1 in FL
by A49, WAYBEL_0:def 16;
consider b1,
y1 being
Element of
L1 such that A52:
y1 = v1
and A53:
b1 = f . v1
and
b1 in B1
and
not
b1 <= pL
and A54:
b1 << y1
by A34, A51;
A55:
b1 in FFL
by A33, A51, A53, FUNCT_1:def 5;
b1 << z1
by A50, A52, A54, WAYBEL_3:2;
then
b1 <= z1
by WAYBEL_3:1;
hence
z in uparrow FFL
by A55, WAYBEL_0:def 16;
:: thesis: verum
end; then A56:
(wayabove bL) \ (uparrow FFL) c= (wayabove xL) \ (uparrow FL)
by A48, XBOOLE_1:35;
wayabove xL c= W
then
(wayabove xL) \ (uparrow FL) c= a
by A13, A27, XBOOLE_1:33;
then
(wayabove bL) \ (uparrow FFL) c= a
by A56, XBOOLE_1:1;
hence
cT c= A
by A12, XBOOLE_1:1;
:: thesis: verum end;
hence
{ (Way_Up a,A) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
by A3, YELLOW_9:32; :: thesis: verum