let TM be metrizable TopSpace; :: thesis: for Am being Subset of TM st Am is dense holds
weight TM c= omega *` (card Am)
let Am be Subset of TM; :: thesis: ( Am is dense implies weight TM c= omega *` (card Am) )
assume A1:
Am is dense
; :: thesis: weight TM c= omega *` (card Am)
per cases
( TM is empty or not TM is empty )
;
suppose A2:
not
TM is
empty
;
:: thesis: 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;
:: thesis: ( 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 A10:
B is
open
;
:: thesis: 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 )
A11:
B in the
topology of
TM
by A10, PRE_TOPC:def 5;
let p be
Point of
TM;
:: thesis: ( 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
;
:: thesis: ex a being Subset of TM st
( a in Up & p in a & a c= B )
reconsider p' =
p as
Point of
Tm by A2, A3, PCOMPS_2:8;
consider r being
Real such that A13:
r > 0
and A14:
Ball p',
r c= B
by A4, A11, A12, PCOMPS_1:def 5;
consider n being
Element of
NAT such that A15:
1
/ (2 |^ n) <= r / 2
by A13, PREPOWER:106;
reconsider B2 =
Ball p',
(1 / (2 |^ n)) as
Subset of
TM by A2, A3, PCOMPS_2:8;
( 2
|^ n > 0 &
dist p',
p' = 0 )
by METRIC_1:1, PREPOWER:13;
then A16:
p' 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, A16, TOPS_1:80;
then consider q being
set such that A17:
q in B2
and A18:
q in Am
by XBOOLE_0:3;
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:8;
take
B3
;
:: thesis: ( 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 A18;
hence
B3 in Up
by PROB_1:25;
:: thesis: ( p in B3 & B3 c= B )
A19:
dist p',
q < 1
/ (2 |^ n)
by A17, METRIC_1:12;
hence
p in B3
by METRIC_1:12;
:: thesis: B3 c= B
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in B3 or y in B )
assume A20:
y in B3
;
:: thesis: y in B
then reconsider t =
y as
Point of
Tm ;
dist q,
t < 1
/ (2 |^ n)
by A20, METRIC_1:12;
then A21:
dist q,
t < r / 2
by A15, XXREAL_0:2;
dist p',
q < r / 2
by A15, A19, XXREAL_0:2;
then
(
dist p',
t <= (dist p',q) + (dist q,t) &
(dist p',q) + (dist q,t) < (r / 2) + (r / 2) )
by A21, METRIC_1:4, XREAL_1:10;
then
dist p',
t < r
by XXREAL_0:2;
then
t in Ball p',
r
by METRIC_1:12;
hence
y in B
by A14;
:: thesis: verum
end; then
Up is
Basis of
TM
by YELLOW_9:32;
then A22:
weight TM c= card Up
by WAYBEL23:74;
A23:
for
x being
set st
x in dom P holds
card (P . x) c= card Am
by A9;
card (dom P) = omega
by CARD_1:84, FUNCT_2:def 1;
then
card (Union P) c= omega *` (card Am)
by A23, CARD_3:132;
hence
weight TM c= omega *` (card Am)
by A22, XBOOLE_1:1;
:: thesis: verum end;