let T be non empty TopSpace; ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_discrete )
assume A1:
T is metrizable
; 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
and
A3:
Family_open_set (SpaceMetr the carrier of T,metr) = the topology of T
by A1, PCOMPS_1:def 9;
set bbcT = bool (bool the carrier of T);
reconsider PM = SpaceMetr the carrier of T,metr as non empty MetrSpace by A2, PCOMPS_1:40;
deffunc H1( set ) -> set = { (Ball x,(1 / (2 |^ (In $1,NAT )))) where x is Point of PM : x is Point of PM } ;
A4:
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
A6:
for k being set st k in NAT holds
FB . k = H1(k)
from FUNCT_2:sch 2(A4);
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 );
set TPM = TopSpaceMetr PM;
A7:
TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #)
by PCOMPS_1:def 6;
then A8:
[#] T = [#] (TopSpaceMetr PM)
by A2, PCOMPS_2:8;
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 ;
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;
then A11:
FB . n is
open
by TOPS_2:def 1;
A12:
[#] (TopSpaceMetr PM) c= union (FB . n)
union (FB . n) c= [#] (TopSpaceMetr PM)
then
[#] (TopSpaceMetr PM) = union (FB . n)
by A12, XBOOLE_0:def 10;
then
FB . n is
Cover of
T
by A8, SETFAM_1:60;
then consider Un being
FamilySequence of
T such that A18:
(
Union Un is
open &
Union Un is
Cover of
T &
Union Un is_finer_than FB . n &
Un is
sigma_discrete )
by A1, A11, 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 A18;
verum
end;
consider Un being Function of NAT ,(Funcs NAT ,(bool (bool the carrier of T))) such that
A19:
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;
A20:
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] )
proof
let k be
set ;
( k in NAT implies ex Ux being set st
( Ux in bool (bool the carrier of T) & S2[k,Ux] ) )
assume
k in NAT
;
ex Ux being set st
( Ux in bool (bool the carrier of T) & S2[k,Ux] )
then reconsider k9 =
k as
Element of
NAT ;
NAT = rng PairFunc
by Th2, FUNCT_2:def 3;
then consider nm being
set such that A21:
nm in dom PairFunc
and A22:
k9 = PairFunc . nm
by FUNCT_1:def 5;
consider n,
m being
set such that A23:
n in NAT
and
m in NAT
and A24:
nm = [n,m]
by A21, ZFMISC_1:def 2;
reconsider Unn =
Un . n as
FamilySequence of
T by A23, FUNCT_2:7, FUNCT_2:121;
take Ux =
Unn . m;
( Ux in bool (bool the carrier of T) & S2[k,Ux] )
hence
(
Ux in bool (bool the carrier of T) &
S2[
k,
Ux] )
;
verum
end;
consider UX being Function of NAT ,(bool (bool the carrier of T)) such that
A28:
for k being set st k in NAT holds
S2[k,UX . k]
from FUNCT_2:sch 1(A20);
A29:
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;
( 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
A is
open
;
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 )
then A30:
A in Family_open_set PM
by A3, PRE_TOPC:def 5;
let p be
Point of
T;
( p in A implies ex B being Subset of T st
( B in Union UX & p in B & B c= A ) )
assume A31:
p in A
;
ex B being Subset of T st
( B in Union UX & p in B & B c= A )
reconsider p =
p as
Element of
PM by A31, A30;
consider r being
Real such that A32:
r > 0
and A33:
Ball p,
r c= A
by A31, A30, PCOMPS_1:def 5;
consider n being
Element of
NAT such that A34:
1
/ (2 |^ n) <= r
by A32, PREPOWER:106;
consider Unn1 being
FamilySequence of
T such that A35:
Un . (n + 1) = Unn1
and
Union Unn1 is
open
and A36:
Union Unn1 is
Cover of
T
and A37:
Union Unn1 is_finer_than FB . (n + 1)
and
Unn1 is
sigma_discrete
by A19;
union (Union Unn1) = [#] T
by A36, SETFAM_1:60;
then consider B being
set such that A38:
p in B
and A39:
B in Union Unn1
by TARSKI:def 4;
reconsider B =
B as
Subset of
PM by A2, A39, PCOMPS_2:8;
consider B1 being
set such that A40:
B1 in FB . (n + 1)
and A41:
B c= B1
by A37, A39, SETFAM_1:def 2;
consider k being
Element of
NAT such that A42:
B in Unn1 . k
by A39, PROB_1:25;
(
n + 1
= In (n + 1),
NAT &
B1 in H1(
n + 1) )
by A6, A40, FUNCT_7:def 1;
then consider q being
Point of
PM such that A43:
B1 = Ball q,
(1 / (2 |^ (n + 1)))
and
q is
Element of
PM
;
now let s be
Element of
PM;
( s in B implies s in Ball p,r )assume
s in B
;
s in Ball p,rthen A44:
dist q,
s < 1
/ (2 |^ (n + 1))
by A41, A43, METRIC_1:12;
dist q,
p < 1
/ (2 |^ (n + 1))
by A38, A41, A43, METRIC_1:12;
then
(
dist p,
s <= (dist q,p) + (dist q,s) &
(dist q,p) + (dist q,s) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) )
by A44, METRIC_1:4, XREAL_1:10;
then
dist p,
s < 2
* (1 / (2 |^ (n + 1)))
by 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 A34, XXREAL_0:2;
hence
s in Ball p,
r
by METRIC_1:12;
verum end;
then A45:
B c= Ball p,
r
by SUBSET_1:7;
UX . (PairFunc . [(n + 1),k]) = Unn1 . k
by A28, A35;
then
B in Union UX
by A42, PROB_1:25;
hence
ex
B being
Subset of
T st
(
B in Union UX &
p in B &
B c= A )
by A33, A38, A45, XBOOLE_1:1;
verum
end;
for k being Element of NAT holds UX . k is discrete
proof
let k be
Element of
NAT ;
UX . k is discrete
NAT = rng PairFunc
by Th2, FUNCT_2:def 3;
then consider nm being
set such that A46:
nm in dom PairFunc
and A47:
k = PairFunc . nm
by FUNCT_1:def 5;
consider n,
m being
set such that A48:
n in NAT
and A49:
m in NAT
and A50:
nm = [n,m]
by A46, ZFMISC_1:def 2;
consider FS being
FamilySequence of
T such that A51:
Un . n = FS
and
Union FS is
open
and
Union FS is
Cover of
T
and
Union FS is_finer_than FB . n
and A52:
FS is
sigma_discrete
by A19, A48;
FS . m is
discrete
by A49, A52, NAGATA_1:def 2;
hence
UX . k is
discrete
by A28, A47, A48, A49, A50, A51;
verum
end;
then A53:
UX is sigma_discrete
by NAGATA_1:def 2;
Union UX c= the topology of T
proof
let UXk be
set ;
TARSKI:def 3 ( not UXk in Union UX or UXk in the topology of T )
assume
UXk in Union UX
;
UXk in the topology of T
then consider k being
Element of
NAT such that A54:
UXk in UX . k
by PROB_1:25;
reconsider UXk9 =
UXk as
Subset of
T by A54;
NAT = rng PairFunc
by Th2, FUNCT_2:def 3;
then consider nm being
set such that A55:
nm in dom PairFunc
and A56:
k = PairFunc . nm
by FUNCT_1:def 5;
consider n,
m being
set such that A57:
n in NAT
and A58:
m in NAT
and A59:
nm = [n,m]
by A55, ZFMISC_1:def 2;
reconsider Unn =
Un . n as
FamilySequence of
T by A57, FUNCT_2:7, FUNCT_2:121;
UXk in Unn . m
by A28, A54, A56, A57, A58, A59;
then A60:
UXk in Union Unn
by A58, PROB_1:25;
ex
FS being
FamilySequence of
T st
(
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 A19, A57;
then
UXk9 is
open
by A60, TOPS_2:def 1;
hence
UXk in the
topology of
T
by PRE_TOPC:def 5;
verum
end;
then
Union UX is Basis of T
by A29, YELLOW_9:32;
then
UX is Basis_sigma_discrete
by A53, NAGATA_1:def 5;
hence
ex Un being FamilySequence of T st Un is Basis_sigma_discrete
; verum