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[
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;
YY:
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 2;
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:4;
consider r being
Real such that A12:
r > 0
and A13:
Ball (
p9,
r)
c= B
by A4, A10, A11, PCOMPS_1:def 4;
consider n being
Element of
NAT such that A14:
1
/ (2 |^ n) <= r / 2
by A12, 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 A15:
p9 in B2
by METRIC_1:11;
B2 in the
topology of
TM
by A4, PCOMPS_1:29;
then
B2 is
open
by PRE_TOPC:def 2;
then
B2 meets Am
by A1, A15, TOPS_1:45;
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:4;
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:12;
( p in B3 & B3 c= B )
A18:
dist (
p9,
q)
< 1
/ (2 |^ n)
by A16, METRIC_1:11;
hence
p in B3
by METRIC_1:11;
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:11;
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: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 A13;
verum
end;
Up is
Basis of
TM
by YY, YELLOW_9:32;
then A21:
weight TM c= card Up
by WAYBEL23:73;
A22:
card (dom P) = omega
by CARD_1:47, 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_2:86;
hence
weight TM c= omega *` (card Am)
by A21, XBOOLE_1:1;
verum end;