let T be non empty TopSpace; :: thesis: ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_discrete )
assume A1:
T is metrizable
; :: thesis: ex Un being FamilySequence of T st Un is Basis_sigma_discrete
consider metr being Function of [:the carrier of T,the carrier of T:], REAL such that
A2:
( metr is_metric_of the carrier of T & Family_open_set (SpaceMetr the carrier of T,metr) = the topology of T )
by A1, PCOMPS_1:def 9;
set PM = SpaceMetr the carrier of T,metr;
set TPM = TopSpaceMetr (SpaceMetr the carrier of T,metr);
A3:
TopSpaceMetr (SpaceMetr the carrier of T,metr) = TopStruct(# the carrier of (SpaceMetr the carrier of T,metr),(Family_open_set (SpaceMetr the carrier of T,metr)) #)
by PCOMPS_1:def 6;
then A4:
[#] T = [#] (TopSpaceMetr (SpaceMetr the carrier of T,metr))
by A2, PCOMPS_2:8;
deffunc H1( set ) -> set = { (Ball x,(1 / (2 |^ (In $1,NAT )))) where x is Point of (SpaceMetr the carrier of T,metr) : x is Point of (SpaceMetr the carrier of T,metr) } ;
A5:
for k being set st k in NAT holds
H1(k) in bool (bool the carrier of T)
consider FB being FamilySequence of T such that
A8:
for k being set st k in NAT holds
FB . k = H1(k)
from FUNCT_2:sch 2(A5);
set bbcT = bool (bool the carrier of T);
defpred S1[ set , set ] means ex FS being FamilySequence of T st
( $2 = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . $1 & FS is sigma_discrete );
A9:
for n being Element of NAT ex Un being Element of Funcs NAT ,(bool (bool the carrier of T)) st S1[n,Un]
proof
let n be
Element of
NAT ;
:: thesis: ex Un being Element of Funcs NAT ,(bool (bool the carrier of T)) st S1[n,Un]
A10:
n = In n,
NAT
by FUNCT_7:def 1;
[#] (TopSpaceMetr (SpaceMetr the carrier of T,metr)) = union (FB . n)
then A14:
FB . n is
Cover of
T
by A4, SETFAM_1:60;
then
FB . n is
open
by TOPS_2:def 1;
then consider Un being
FamilySequence of
T such that A15:
(
Union Un is
open &
Union Un is
Cover of
T &
Union Un is_finer_than FB . n &
Un is
sigma_discrete )
by A1, A14, Th20;
Un in Funcs NAT ,
(bool (bool the carrier of T))
by FUNCT_2:11;
hence
ex
Un being
Element of
Funcs NAT ,
(bool (bool the carrier of T)) st
S1[
n,
Un]
by A15;
:: thesis: verum
end;
consider Un being Function of NAT , Funcs NAT ,(bool (bool the carrier of T)) such that
A16:
for n being Element of NAT holds S1[n,Un . n]
from FUNCT_2:sch 3(A9);
defpred S2[ set , set ] means for n, m being Element of NAT st PairFunc . [n,m] = $1 holds
for Unn being FamilySequence of T st Unn = Un . n holds
$2 = Unn . m;
A17:
for k being set st k in NAT holds
ex Ux being set st
( Ux in bool (bool the carrier of T) & S2[k,Ux] )
consider UX being Function of NAT , bool (bool the carrier of T) such that
A23:
for k being set st k in NAT holds
S2[k,UX . k]
from FUNCT_2:sch 1(A17);
A24:
UX is sigma_discrete
A28:
Union UX c= the topology of T
proof
let UXk be
set ;
:: according to TARSKI:def 3 :: thesis: ( not UXk in Union UX or UXk in the topology of T )
assume
UXk in Union UX
;
:: thesis: UXk in the topology of T
then consider k being
Element of
NAT such that A29:
UXk in UX . k
by PROB_1:25;
reconsider UXk' =
UXk as
Subset of
T by A29;
PairFunc is
onto
by Th2;
then
NAT = rng PairFunc
by FUNCT_2:def 3;
then consider nm being
set such that A30:
(
nm in dom PairFunc &
k = PairFunc . nm )
by FUNCT_1:def 5;
consider n,
m being
set such that A31:
(
n in NAT &
m in NAT &
nm = [n,m] )
by A30, ZFMISC_1:def 2;
reconsider Unn =
Un . n as
FamilySequence of
T by A31, FUNCT_2:7, FUNCT_2:121;
consider FS being
FamilySequence of
T such that A32:
(
Un . n = FS &
Union FS is
open &
Union FS is
Cover of
T &
Union FS is_finer_than FB . n &
FS is
sigma_discrete )
by A16, A31;
UXk in Unn . m
by A23, A29, A30, A31;
then
(
UXk in Union Unn &
Union Unn is
open )
by A31, A32, PROB_1:25;
then
UXk' is
open
by TOPS_2:def 1;
hence
UXk in the
topology of
T
by PRE_TOPC:def 5;
:: thesis: verum
end;
for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex B being Subset of T st
( B in Union UX & p in B & B c= A )
proof
let A be
Subset of
T;
:: thesis: ( A is open implies for p being Point of T st p in A holds
ex B being Subset of T st
( B in Union UX & p in B & B c= A ) )
assume A33:
A is
open
;
:: thesis: for p being Point of T st p in A holds
ex B being Subset of T st
( B in Union UX & p in B & B c= A )
let p be
Point of
T;
:: thesis: ( p in A implies ex B being Subset of T st
( B in Union UX & p in B & B c= A ) )
assume A34:
p in A
;
:: thesis: ex B being Subset of T st
( B in Union UX & p in B & B c= A )
A35:
A in Family_open_set (SpaceMetr the carrier of T,metr)
by A2, A33, PRE_TOPC:def 5;
then reconsider p =
p as
Element of
(SpaceMetr the carrier of T,metr) by A34;
consider r being
Real such that A36:
(
r > 0 &
Ball p,
r c= A )
by A34, A35, PCOMPS_1:def 5;
consider n being
Element of
NAT such that A37:
1
/ (2 |^ n) <= r
by A36, PREPOWER:106;
consider Unn1 being
FamilySequence of
T such that A38:
(
Un . (n + 1) = Unn1 &
Union Unn1 is
open &
Union Unn1 is
Cover of
T &
Union Unn1 is_finer_than FB . (n + 1) &
Unn1 is
sigma_discrete )
by A16;
union (Union Unn1) = [#] T
by A38, SETFAM_1:60;
then consider B being
set such that A39:
(
p in B &
B in Union Unn1 )
by TARSKI:def 4;
reconsider B =
B as
Subset of
(SpaceMetr the carrier of T,metr) by A2, A39, PCOMPS_2:8;
consider B1 being
set such that A40:
(
B1 in FB . (n + 1) &
B c= B1 )
by A38, A39, SETFAM_1:def 2;
A41:
n + 1
= In (n + 1),
NAT
by FUNCT_7:def 1;
B1 in H1(
n + 1)
by A8, A40;
then consider q being
Point of
(SpaceMetr the carrier of T,metr) such that A42:
(
B1 = Ball q,
(1 / (2 |^ (n + 1))) &
q is
Element of
(SpaceMetr the carrier of T,metr) )
by A41;
consider k being
Element of
NAT such that A43:
B in Unn1 . k
by A39, PROB_1:25;
A44:
UX . (PairFunc . [(n + 1),k]) = Unn1 . k
by A23, A38;
B c= Ball p,
r
proof
now let s be
Element of
(SpaceMetr the carrier of T,metr);
:: thesis: ( s in B implies s in Ball p,r )assume
s in B
;
:: thesis: s in Ball p,rthen A45:
dist q,
s < 1
/ (2 |^ (n + 1))
by A40, A42, METRIC_1:12;
A46:
dist p,
s <= (dist q,p) + (dist q,s)
by METRIC_1:4;
dist q,
p < 1
/ (2 |^ (n + 1))
by A39, A40, A42, METRIC_1:12;
then
(dist q,p) + (dist q,s) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1)))
by A45, XREAL_1:10;
then
dist p,
s < 2
* (1 / (2 |^ (n + 1)))
by A46, XXREAL_0:2;
then
dist p,
s < (1 / ((2 |^ n) * 2)) * 2
by NEWTON:11;
then
dist p,
s < 1
/ (2 |^ n)
by XCMPLX_1:93;
then
dist p,
s < r
by A37, XXREAL_0:2;
hence
s in Ball p,
r
by METRIC_1:12;
:: thesis: verum end;
hence
B c= Ball p,
r
by SUBSET_1:7;
:: thesis: verum
end;
then
(
B in Union UX &
p in B &
B c= A )
by A36, A39, A43, A44, PROB_1:25, XBOOLE_1:1;
hence
ex
B being
Subset of
T st
(
B in Union UX &
p in B &
B c= A )
;
:: thesis: verum
end;
then
Union UX is Basis of T
by A28, YELLOW_9:32;
then
UX is Basis_sigma_discrete
by A24, NAGATA_1:def 5;
hence
ex Un being FamilySequence of T st Un is Basis_sigma_discrete
; :: thesis: verum