let TM be metrizable TopSpace; for Am being Subset of TM st Am is dense holds
weight TM c= omega *` (card Am)
let Am be Subset of TM; ( Am is dense implies weight TM c= omega *` (card Am) )
assume A1:
Am is dense
; weight TM c= omega *` (card Am)
per cases
( TM is empty or not TM is empty )
;
suppose A2:
not
TM is
empty
;
weight TM c= omega *` (card Am)set TOP = the
topology of
TM;
set cTM = the
carrier of
TM;
consider metr being
Function of
[:the carrier of TM,the carrier of TM:],
REAL such that A3:
metr is_metric_of the
carrier of
TM
and A4:
Family_open_set (SpaceMetr the carrier of TM,metr) = the
topology of
TM
by PCOMPS_1:def 9;
reconsider Tm =
SpaceMetr the
carrier of
TM,
metr as non
empty MetrSpace by A2, A3, PCOMPS_1:40;
defpred S1[
set ,
set ]
means for
n being
Nat st
n = $1 holds
( $2
= { (Ball p,(1 / (2 |^ n))) where p is Point of Tm : p in Am } &
card $2
c= card Am );
A5:
for
x being
set st
x in NAT holds
ex
y being
set st
(
y in bool the
topology of
TM &
S1[
x,
y] )
consider P being
Function of
NAT ,
(bool the topology of TM) such that A9:
for
x being
set st
x in NAT holds
S1[
x,
P . x]
from FUNCT_2:sch 1(A5);
reconsider Up =
Union P as
Subset-Family of
TM by XBOOLE_1:1;
for
B being
Subset of
TM st
B is
open holds
for
p being
Point of
TM st
p in B holds
ex
a being
Subset of
TM st
(
a in Up &
p in a &
a c= B )
proof
let B be
Subset of
TM;
( B is open implies for p being Point of TM st p in B holds
ex a being Subset of TM st
( a in Up & p in a & a c= B ) )
assume
B is
open
;
for p being Point of TM st p in B holds
ex a being Subset of TM st
( a in Up & p in a & a c= B )
then A10:
B in the
topology of
TM
by PRE_TOPC:def 5;
let p be
Point of
TM;
( p in B implies ex a being Subset of TM st
( a in Up & p in a & a c= B ) )
assume A11:
p in B
;
ex a being Subset of TM st
( a in Up & p in a & a c= B )
reconsider p9 =
p as
Point of
Tm by A2, A3, PCOMPS_2:8;
consider r being
Real such that A12:
r > 0
and A13:
Ball p9,
r c= B
by A4, A10, A11, PCOMPS_1:def 5;
consider n being
Element of
NAT such that A14:
1
/ (2 |^ n) <= r / 2
by A12, PREPOWER:106;
reconsider B2 =
Ball p9,
(1 / (2 |^ n)) as
Subset of
TM by A2, A3, PCOMPS_2:8;
( 2
|^ n > 0 &
dist p9,
p9 = 0 )
by METRIC_1:1, PREPOWER:13;
then A15:
p9 in B2
by METRIC_1:12;
B2 in the
topology of
TM
by A4, PCOMPS_1:33;
then
B2 is
open
by PRE_TOPC:def 5;
then
B2 meets Am
by A1, A15, TOPS_1:80;
then consider q being
set such that A16:
q in B2
and A17:
q in Am
by XBOOLE_0:3;
reconsider q =
q as
Point of
Tm by A16;
reconsider B3 =
Ball q,
(1 / (2 |^ n)) as
Subset of
TM by A2, A3, PCOMPS_2:8;
take
B3
;
( B3 in Up & p in B3 & B3 c= B )
P . n = { (Ball t,(1 / (2 |^ n))) where t is Point of Tm : t in Am }
by A9;
then
B3 in P . n
by A17;
hence
B3 in Up
by PROB_1:25;
( p in B3 & B3 c= B )
A18:
dist p9,
q < 1
/ (2 |^ n)
by A16, METRIC_1:12;
hence
p in B3
by METRIC_1:12;
B3 c= B
let y be
set ;
TARSKI:def 3 ( not y in B3 or y in B )
assume A19:
y in B3
;
y in B
then reconsider t =
y as
Point of
Tm ;
dist q,
t < 1
/ (2 |^ n)
by A19, METRIC_1:12;
then A20:
dist q,
t < r / 2
by A14, XXREAL_0:2;
dist p9,
q < r / 2
by A14, A18, XXREAL_0:2;
then
(
dist p9,
t <= (dist p9,q) + (dist q,t) &
(dist p9,q) + (dist q,t) < (r / 2) + (r / 2) )
by A20, METRIC_1:4, XREAL_1:10;
then
dist p9,
t < r
by XXREAL_0:2;
then
t in Ball p9,
r
by METRIC_1:12;
hence
y in B
by A13;
verum
end; then
Up is
Basis of
TM
by YELLOW_9:32;
then A21:
weight TM c= card Up
by WAYBEL23:74;
A22:
card (dom P) = omega
by CARD_1:84, FUNCT_2:def 1;
for
x being
set st
x in dom P holds
card (P . x) c= card Am
by A9;
then
card (Union P) c= omega *` (card Am)
by A22, CARD_3:132;
hence
weight TM c= omega *` (card Am)
by A21, XBOOLE_1:1;
verum end;