let T be non empty finite-weight TopSpace; :: thesis: ex B0 being Basis of T ex f being Function of the carrier of T, the topology of T st
( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:74;
deffunc H1( object ) -> set = meet { U where U is Subset of T : ( $1 in U & U in B ) } ;
A2: B is finite by A1, Def4;
A3: now :: thesis: for a being object st a in the carrier of T holds
H1(a) in the topology of T
B c= the topology of T by TOPS_2:64;
then FinMeetCl B c= FinMeetCl the topology of T by CANTOR_1:14;
then A4: FinMeetCl B c= the topology of T by CANTOR_1:5;
let a be object ; :: thesis: ( a in the carrier of T implies H1(a) in the topology of T )
assume a in the carrier of T ; :: thesis: H1(a) in the topology of T
then reconsider x = a as Point of T ;
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
consider U being Subset of T such that
A5: U in B and
A6: x in U and
U c= [#] T by YELLOW_9:31;
A7: { U where U is Subset of T : ( x in U & U in B ) } c= B
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { U where U is Subset of T : ( x in U & U in B ) } or a in B )
assume a in { U where U is Subset of T : ( x in U & U in B ) } ; :: thesis: a in B
then ex U being Subset of T st
( a = U & x in U & U in B ) ;
hence a in B ; :: thesis: verum
end;
then reconsider S = { U where U is Subset of T : ( x in U & U in B ) } as Subset-Family of T by XBOOLE_1:1;
Intersect S in FinMeetCl B by A2, A7, CANTOR_1:def 3;
then A8: Intersect S in the topology of T by A4;
U in S by A5, A6;
hence H1(a) in the topology of T by A8, SETFAM_1:def 9; :: thesis: verum
end;
consider f being Function of the carrier of T, the topology of T such that
A9: for a being object st a in the carrier of T holds
f . a = H1(a) from FUNCT_2:sch 2(A3);
 set B0 = rng f;
reconsider B0 = rng f as Subset-Family of T by XBOOLE_1:1;
A10: now :: thesis: for a being set st a in the carrier of T holds
a in f . a
let a be set ; :: thesis: ( a in the carrier of T implies a in f . a )
assume a in the carrier of T ; :: thesis: a in f . a
then reconsider x = a as Point of T ;
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
consider U being Subset of T such that
A11: U in B and
A12: x in U and
U c= [#] T by YELLOW_9:31;
A13: now :: thesis: for b being set st b in { U where U is Subset of T : ( x in U & U in B ) } holds
a in b
let b be set ; :: thesis: ( b in { U where U is Subset of T : ( x in U & U in B ) } implies a in b )
assume b in { U where U is Subset of T : ( x in U & U in B ) } ; :: thesis: a in b
then ex U being Subset of T st
( b = U & a in U & U in B ) ;
hence a in b ; :: thesis: verum
end;
A14: f . a = meet { U where U is Subset of T : ( x in U & U in B ) } by A9;
U in { U where U is Subset of T : ( x in U & U in B ) } by A11, A12;
hence a in f . a by A14, A13, SETFAM_1:def 1; :: thesis: verum
end;
A15: now :: thesis: for x being Point of T
for V being Subset of T st x in V & V is open holds
f . x c= V
let x be Point of T; :: thesis: for V being Subset of T st x in V & V is open holds
f . x c= V
let V be Subset of T; :: thesis: ( x in V & V is open implies f . x c= V )
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
assume that
A16: x in V and
A17: V is open ; :: thesis: f . x c= V
consider U being Subset of T such that
A18: U in B and
A19: x in U and
A20: U c= V by A16, A17, YELLOW_9:31;
A21: f . x = meet { U where U is Subset of T : ( x in U & U in B ) } by A9;
U in { U where U is Subset of T : ( x in U & U in B ) } by A18, A19;
then f . x c= U by A21, SETFAM_1:3;
hence f . x c= V by A20; :: thesis: verum
end;
now :: thesis: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B0 & p in a & a c= A )
let A be Subset of T; :: thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in B0 & p in a & a c= A ) )
assume A22: A is open ; :: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in B0 & p in a & a c= A )
let p be Point of T; :: thesis: ( p in A implies ex a being Subset of T st
( a in B0 & p in a & a c= A ) )
assume A23: p in A ; :: thesis: ex a being Subset of T st
( a in B0 & p in a & a c= A )
f . p in the topology of T ;
then reconsider a = f . p as Subset of T ;
take a = a; :: thesis: ( a in B0 & p in a & a c= A )
thus a in B0 by FUNCT_2:4; :: thesis: ( p in a & a c= A )
thus p in a by A10; :: thesis: a c= A
thus a c= A by A15, A22, A23; :: thesis: verum
end;
then reconsider B0 = B0 as Basis of T by YELLOW_9:32;
take B0 ; :: thesis: ex f being Function of the carrier of T, the topology of T st
( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
take f ; :: thesis: ( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
thus B0 = rng f ; :: thesis: for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) )
let x be Point of T; :: thesis: ( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) )
thus ( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) by A10, A15; :: thesis: verum