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 8;
reconsider Tm =
SpaceMetr ( the
carrier of
TM,
metr) as non
empty MetrSpace by A2, A3, PCOMPS_1:36;
defpred S1[
object ,
object ]
means ex
D2 being
set st
(
D2 = $2 & ( for
n being
Nat st
n = $1 holds
( $2
= { (Ball (p,(1 / (2 |^ n)))) where p is Point of Tm : p in Am } &
card D2 c= card Am ) ) );
A5:
for
x being
object st
x in NAT holds
ex
y being
object st
(
y in bool the
topology of
TM &
S1[
x,
y] )
consider P being
sequence of
(bool the topology of TM) such that A9:
for
x being
object 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;
A10:
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 A11:
B in the
topology of
TM
;
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 A12:
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:4;
consider r being
Real such that A13:
r > 0
and A14:
Ball (
p9,
r)
c= B
by A4, A11, A12, PCOMPS_1:def 4;
consider n being
Nat such that A15:
1
/ (2 |^ n) <= r / 2
by A13, PREPOWER:92;
reconsider B2 =
Ball (
p9,
(1 / (2 |^ n))) as
Subset of
TM by A2, A3, PCOMPS_2:4;
( 2
|^ n > 0 &
dist (
p9,
p9)
= 0 )
by METRIC_1:1, PREPOWER:6;
then A16:
p9 in B2
by METRIC_1:11;
B2 in the
topology of
TM
by A4, PCOMPS_1:29;
then
B2 is
open
;
then
B2 meets Am
by A1, A16, TOPS_1:45;
then consider q being
object such that A17:
q in B2
and A18:
q in Am
by XBOOLE_0:3;
A19:
n in NAT
by ORDINAL1:def 12;
reconsider q =
q as
Point of
Tm by A17;
reconsider B3 =
Ball (
q,
(1 / (2 |^ n))) as
Subset of
TM by A2, A3, PCOMPS_2:4;
take
B3
;
( B3 in Up & p in B3 & B3 c= B )
S1[
n,
P . n]
by A9, A19;
then
P . n = { (Ball (t,(1 / (2 |^ n)))) where t is Point of Tm : t in Am }
;
then
B3 in P . n
by A18;
hence
B3 in Up
by PROB_1:12;
( p in B3 & B3 c= B )
A20:
dist (
p9,
q)
< 1
/ (2 |^ n)
by A17, METRIC_1:11;
hence
p in B3
by METRIC_1:11;
B3 c= B
let y be
object ;
TARSKI:def 3 ( not y in B3 or y in B )
assume A21:
y in B3
;
y in B
then reconsider t =
y as
Point of
Tm ;
dist (
q,
t)
< 1
/ (2 |^ n)
by A21, METRIC_1:11;
then A22:
dist (
q,
t)
< r / 2
by A15, XXREAL_0:2;
dist (
p9,
q)
< r / 2
by A15, A20, XXREAL_0:2;
then
(
dist (
p9,
t)
<= (dist (p9,q)) + (dist (q,t)) &
(dist (p9,q)) + (dist (q,t)) < (r / 2) + (r / 2) )
by A22, METRIC_1:4, XREAL_1:8;
then
dist (
p9,
t)
< r
by XXREAL_0:2;
then
t in Ball (
p9,
r)
by METRIC_1:11;
hence
y in B
by A14;
verum
end;
Up is
Basis of
TM
by A10, YELLOW_9:32;
then A23:
weight TM c= card Up
by WAYBEL23:73;
A24:
card (dom P) = omega
by CARD_1:47, FUNCT_2:def 1;
for
x being
object st
x in dom P holds
card (P . x) c= card Am
then
card (Union P) c= omega *` (card Am)
by A24, CARD_2:86;
hence
weight TM c= omega *` (card Am)
by A23;
verum end;