let M be non empty MetrSpace; ( M is totally_bounded implies TopSpaceMetr M is second-countable )
assume A1:
M is totally_bounded
; TopSpaceMetr M is second-countable
set T = TopSpaceMetr M;
defpred S1[ object , object ] means for i being Nat 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 object st x in NAT holds
ex y being object st
( y in bool (bool the carrier of (TopSpaceMetr M)) & S1[x,y] )
consider f being sequence of (bool (bool the carrier of (TopSpaceMetr M))) such that
A6:
for x being object st x in NAT holds
S1[x,f . x]
from FUNCT_2:sch 1(A2);
set U = Union f;
A7:
dom f = NAT
by FUNCT_2:def 1;
A8:
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);
( 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 A9:
A is
open
;
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);
( p in A implies ex a being Subset of (TopSpaceMetr M) st
( a in Union f & p in a & a c= A ) )
assume A10:
p in A
;
ex a being Subset of (TopSpaceMetr M) st
( a in Union f & p in a & a c= A )
reconsider p9 =
p as
Point of
M ;
consider r being
Real such that A11:
r > 0
and A12:
Ball (
p9,
r)
c= A
by A9, A10, TOPMETR:15;
reconsider r =
r as
Real ;
consider n being
Nat such that A13:
n > 0
and A14:
1
/ n < r / 2
by A11, UNIFORM1:1, XREAL_1:215;
A15:
(1 / n) + (1 / n) < (r / 2) + (r / 2)
by A14, XREAL_1:8;
reconsider n1 =
n - 1 as
Element of
NAT by A13, NAT_1:20;
reconsider fn =
f . n1 as
Subset-Family of
(TopSpaceMetr M) ;
the
carrier of
M = union fn
by A6;
then consider x being
set such that A16:
p in x
and A17:
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 A6, A17;
reconsider B =
Ball (
w,
(1 / n)) as
Subset of
(TopSpaceMetr M) ;
take
B
;
( B in Union f & p in B & B c= A )
f . n1 in rng f
by A7, FUNCT_1:def 3;
then
B in union (rng f)
by A17, A18, TARSKI:def 4;
hence
(
B in Union f &
p in B )
by A16, A18, CARD_3:def 4;
B c= A
let q be
object ;
TARSKI:def 3 ( not q in B or q in A )
assume A19:
q in B
;
q in A
reconsider q9 =
q as
Point of
M by A19;
A20:
dist (
q9,
w)
< 1
/ n
by A19, METRIC_1:11;
dist (
w,
p9)
< 1
/ (n1 + 1)
by A16, A18, METRIC_1:11;
then A21:
(dist (q9,w)) + (dist (w,p9)) < (1 / n) + (1 / n)
by A20, XREAL_1:8;
dist (
q9,
p9)
<= (dist (q9,w)) + (dist (w,p9))
by METRIC_1:4;
then
dist (
q9,
p9)
< (1 / n) + (1 / n)
by A21, XXREAL_0:2;
then
dist (
q9,
p9)
< (r / 2) + (r / 2)
by A15, XXREAL_0:2;
then
q in Ball (
p9,
r)
by METRIC_1:11;
hence
q in A
by A12;
verum
end;
set CB = { (card B) where B is Basis of (TopSpaceMetr M) : verum } ;
Union f c= the topology of (TopSpaceMetr M)
then
Union f is Basis of (TopSpaceMetr M)
by A8, YELLOW_9:32;
then A26:
card (Union f) in { (card B) where B is Basis of (TopSpaceMetr M) : verum }
;
then
Union f is countable
by A7, CARD_4:2, CARD_4:11;
then A27:
card (Union f) c= omega
by CARD_3:def 14;
weight (TopSpaceMetr M) = meet { (card B) where B is Basis of (TopSpaceMetr M) : verum }
by WAYBEL23:def 5;
then
weight (TopSpaceMetr M) c= card (Union f)
by A26, SETFAM_1:3;
then
weight (TopSpaceMetr M) c= omega
by A27;
hence
TopSpaceMetr M is second-countable
by WAYBEL23:def 6; verum