let T be non empty TopSpace; ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite )
assume A1:
T is metrizable
; ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite
then 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
;
set PM = SpaceMetr ( the carrier of T,metr);
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36;
deffunc H1( Element of NAT ) -> set = { (Ball (x,(1 / (2 |^ $1)))) where x is Element of PM : x is Element of PM } ;
defpred S1[ Element of NAT , set ] means $2 = H1($1);
A4:
for k being Element of NAT ex y being Subset-Family of T st S1[k,y]
consider FB being sequence of (bool (bool the carrier of T)) such that
A5:
for k being Element of NAT holds S1[k,FB . k]
from FUNCT_2:sch 3(A4);
defpred S2[ object , object ] means ex W being Subset-Family of T st
( W = $2 & W is open & W is Cover of T & W is_finer_than FB . $1 & W is locally_finite );
set TPM = TopSpaceMetr PM;
A6:
[#] T = [#] (TopSpaceMetr PM)
by A2, PCOMPS_2:4;
A7:
for n being Element of NAT ex PP being Subset-Family of T st
( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite )
A10:
for k being object st k in NAT holds
ex y being object st
( y in bool (bool the carrier of T) & S2[k,y] )
consider UC being FamilySequence of T such that
A11:
for x being object st x in NAT holds
S2[x,UC . x]
from FUNCT_2:sch 1(A10);
A12:
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 UC & 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 UC & 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 UC & p in B & B c= A )
then A13:
A in Family_open_set PM
by A3, PRE_TOPC:def 2;
let p be
Point of
T;
( p in A implies ex B being Subset of T st
( B in Union UC & p in B & B c= A ) )
assume A14:
p in A
;
ex B being Subset of T st
( B in Union UC & p in B & B c= A )
then reconsider p =
p as
Element of
PM by A13;
consider r1 being
Real such that A15:
r1 > 0
and A16:
Ball (
p,
r1)
c= A
by A14, A13, PCOMPS_1:def 4;
consider n being
Nat such that A17:
1
/ (2 |^ n) <= r1
by A15, PREPOWER:92;
A18:
S2[
n + 1,
UC . (n + 1)]
by A11;
then
union (UC . (n + 1)) = the
carrier of
T
by SETFAM_1:45;
then consider B being
set such that A19:
p in B
and A20:
B in UC . (n + 1)
by TARSKI:def 4;
reconsider B =
B as
Subset of
PM by A2, A20, PCOMPS_2:4;
consider B1 being
set such that A21:
B1 in FB . (n + 1)
and A22:
B c= B1
by A18, A20, SETFAM_1:def 2;
B1 in H1(
n + 1)
by A5, A21;
then consider q being
Element of
PM such that A23:
B1 = Ball (
q,
(1 / (2 |^ (n + 1))))
and
q is
Element of
PM
;
A24:
dist (
q,
p)
< 1
/ (2 |^ (n + 1))
by A19, A22, A23, METRIC_1:11;
now for r being Element of PM st r in B holds
r in Ball (p,r1)let r be
Element of
PM;
( r in B implies r in Ball (p,r1) )assume
r in B
;
r in Ball (p,r1)then
dist (
q,
r)
< 1
/ (2 |^ (n + 1))
by A22, A23, METRIC_1:11;
then
(
dist (
p,
r)
<= (dist (q,p)) + (dist (q,r)) &
(dist (q,p)) + (dist (q,r)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) )
by A24, METRIC_1:4, XREAL_1:8;
then
dist (
p,
r)
< 2
* (1 / (2 |^ (n + 1)))
by XXREAL_0:2;
then
dist (
p,
r)
< (1 / ((2 |^ n) * 2)) * 2
by NEWTON:6;
then
dist (
p,
r)
< 1
/ (2 |^ n)
by XCMPLX_1:92;
then
dist (
p,
r)
< r1
by A17, XXREAL_0:2;
hence
r in Ball (
p,
r1)
by METRIC_1:11;
verum end;
then A25:
B c= Ball (
p,
r1)
;
B in Union UC
by A20, PROB_1:12;
hence
ex
B being
Subset of
T st
(
B in Union UC &
p in B &
B c= A )
by A16, A19, A25, XBOOLE_1:1;
verum
end;
for n being Element of NAT holds UC . n is locally_finite
then A26:
UC is sigma_locally_finite
;
Union UC c= the topology of T
then
Union UC is Basis of T
by A12, YELLOW_9:32;
then
UC is Basis_sigma_locally_finite
by A26;
hence
ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite
; verum