let M be non empty MetrSpace; :: thesis: ( M is totally_bounded implies TopSpaceMetr M is second-countable )
assume A1:
M is totally_bounded
; :: thesis: TopSpaceMetr M is second-countable
set T = TopSpaceMetr M;
defpred S1[ set , set ] means for i being natural number st i = $1 holds
for G being Subset-Family of (TopSpaceMetr M) st $2 = G holds
( G is finite & the carrier of M = union G & ( for C being Subset of M st C in G holds
ex w being Point of M st C = Ball w,(1 / (i + 1)) ) );
A2:
for x being set st x in NAT holds
ex y being set st
( y in bool (bool the carrier of (TopSpaceMetr M)) & S1[x,y] )
consider f being Function of NAT ,(bool (bool the carrier of (TopSpaceMetr M))) such that
A5:
for x being set st x in NAT holds
S1[x,f . x]
from FUNCT_2:sch 1(A2);
A6:
dom f = NAT
by FUNCT_2:def 1;
set U = Union f;
A7:
Union f c= the topology of (TopSpaceMetr M)
for A being Subset of (TopSpaceMetr M) st A is open holds
for p being Point of (TopSpaceMetr M) st p in A holds
ex a being Subset of (TopSpaceMetr M) st
( a in Union f & p in a & a c= A )
proof
let A be
Subset of
(TopSpaceMetr M);
:: thesis: ( A is open implies for p being Point of (TopSpaceMetr M) st p in A holds
ex a being Subset of (TopSpaceMetr M) st
( a in Union f & p in a & a c= A ) )
assume A12:
A is
open
;
:: thesis: for p being Point of (TopSpaceMetr M) st p in A holds
ex a being Subset of (TopSpaceMetr M) st
( a in Union f & p in a & a c= A )
let p be
Point of
(TopSpaceMetr M);
:: thesis: ( p in A implies ex a being Subset of (TopSpaceMetr M) st
( a in Union f & p in a & a c= A ) )
assume A13:
p in A
;
:: thesis: ex a being Subset of (TopSpaceMetr M) st
( a in Union f & p in a & a c= A )
reconsider p' =
p as
Point of
M ;
consider r being
real number such that A14:
(
r > 0 &
Ball p',
r c= A )
by A12, A13, TOPMETR:22;
reconsider r =
r as
Real by XREAL_0:def 1;
consider n being
Element of
NAT such that A15:
(
n > 0 & 1
/ n < r / 2 )
by A14, UNIFORM1:2, XREAL_1:217;
reconsider n1 =
n - 1 as
Element of
NAT by A15, NAT_1:20;
A16:
f . n1 in rng f
by A6, FUNCT_1:def 5;
reconsider fn =
f . n1 as
Subset-Family of
(TopSpaceMetr M) ;
the
carrier of
M = union fn
by A5;
then consider x being
set such that A17:
(
p in x &
x in fn )
by TARSKI:def 4;
reconsider x =
x as
Subset of
M by A17;
consider w being
Point of
M such that A18:
x = Ball w,
(1 / (n1 + 1))
by A5, A17;
reconsider B =
Ball w,
(1 / n) as
Subset of
(TopSpaceMetr M) ;
take
B
;
:: thesis: ( B in Union f & p in B & B c= A )
B in union (rng f)
by A16, A17, A18, TARSKI:def 4;
hence
(
B in Union f &
p in B )
by A17, A18, CARD_3:def 4;
:: thesis: B c= A
let q be
set ;
:: according to TARSKI:def 3 :: thesis: ( not q in B or q in A )
assume A19:
q in B
;
:: thesis: q in A
reconsider q' =
q as
Point of
M by A19;
(
dist q',
w < 1
/ n &
dist w,
p' < 1
/ (n1 + 1) )
by A17, A18, A19, METRIC_1:12;
then
(
dist q',
p' <= (dist q',w) + (dist w,p') &
(dist q',w) + (dist w,p') < (1 / n) + (1 / n) )
by METRIC_1:4, XREAL_1:10;
then
(
dist q',
p' < (1 / n) + (1 / n) &
(1 / n) + (1 / n) < (r / 2) + (r / 2) )
by A15, XREAL_1:10, XXREAL_0:2;
then
dist q',
p' < (r / 2) + (r / 2)
by XXREAL_0:2;
then
q in Ball p',
r
by METRIC_1:12;
hence
q in A
by A14;
:: thesis: verum
end;
then A20:
Union f is Basis of TopSpaceMetr M
by A7, YELLOW_9:32;
then
Union f is countable
by A6, CARD_4:44, CARD_4:61;
then A22:
card (Union f) c= omega
by CARD_3:def 15;
set CB = { (card B) where B is Basis of TopSpaceMetr M : verum } ;
( card (Union f) in { (card B) where B is Basis of TopSpaceMetr M : verum } & weight (TopSpaceMetr M) = meet { (card B) where B is Basis of TopSpaceMetr M : verum } )
by A20, WAYBEL23:def 5;
then
weight (TopSpaceMetr M) c= card (Union f)
by SETFAM_1:4;
then
weight (TopSpaceMetr M) c= omega
by A22, XBOOLE_1:1;
hence
TopSpaceMetr M is second-countable
by WAYBEL23:def 6; :: thesis: verum