let TM be metrizable TopSpace; for iC being infinite Cardinal st ( for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds
Am misses Bm ) holds
card Fm c= iC ) holds
density TM c= iC
let iC be infinite Cardinal; ( ( for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds
Am misses Bm ) holds
card Fm c= iC ) implies density TM c= iC )
assume A1:
for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds
Am misses Bm ) holds
card Fm c= iC
; density TM c= iC
per cases
( TM is empty or not TM is empty )
;
suppose A3:
not
TM is
empty
;
density TM c= iCconsider metr being
Function of
[:the carrier of TM,the carrier of TM:],
REAL such that A4:
metr is_metric_of the
carrier of
TM
and A5:
Family_open_set (SpaceMetr the carrier of TM,metr) = the
topology of
TM
by PCOMPS_1:def 9;
reconsider M =
SpaceMetr the
carrier of
TM,
metr as non
empty MetrSpace by A3, A4, PCOMPS_1:40;
defpred S1[
set ,
set ]
means for
n being
Nat st $1
= n holds
ex
G being
Subset of
TM st
(
G = $2 &
card G c= iC & ( for
p being
Element of
M ex
q being
Element of
M st
(
q in G &
dist p,
q < 1
/ (2 |^ n) ) ) );
A6:
the
carrier of
TM = the
carrier of
M
by A3, A4, PCOMPS_2:8;
A7:
for
x being
set st
x in NAT holds
ex
y being
set st
(
y in bool the
carrier of
TM &
S1[
x,
y] )
proof
let x be
set ;
( x in NAT implies ex y being set st
( y in bool the carrier of TM & S1[x,y] ) )
assume
x in NAT
;
ex y being set st
( y in bool the carrier of TM & S1[x,y] )
then reconsider n =
x as
Element of
NAT ;
reconsider r = 1
/ (2 |^ n) as
Real by XREAL_0:def 1;
A8:
2
|^ n > 0
by PREPOWER:13;
then consider A being
Subset of
M such that A9:
for
p,
q being
Point of
M st
p <> q &
p in A &
q in A holds
dist p,
q >= r
and A10:
for
p being
Point of
M ex
q being
Point of
M st
(
q in A &
p in Ball q,
r )
by COMPL_SP:30;
set BALL =
{ (Ball p,(r / 2)) where p is Element of M : p in A } ;
A11:
{ (Ball p,(r / 2)) where p is Element of M : p in A } c= the
topology of
TM
the
topology of
TM is
open
by CANTOR_1:3;
then reconsider BALL =
{ (Ball p,(r / 2)) where p is Element of M : p in A } as
open Subset-Family of
TM by A11, TOPS_2:18, XBOOLE_1:1;
defpred S2[
set ,
set ]
means for
p being
Point of
M st
Ball p,
(r / 2) = $1 &
p in A holds
p = $2;
A12:
for
x being
set st
x in BALL holds
ex
y being
set st
(
y in A &
S2[
x,
y] )
proof
let x be
set ;
( x in BALL implies ex y being set st
( y in A & S2[x,y] ) )
assume
x in BALL
;
ex y being set st
( y in A & S2[x,y] )
then consider p being
Point of
M such that A13:
x = Ball p,
(r / 2)
and A14:
p in A
;
A15:
r / 2
< r
by A8, XREAL_1:218;
take
p
;
( p in A & S2[x,p] )
thus
p in A
by A14;
S2[x,p]
let q be
Point of
M;
( Ball q,(r / 2) = x & q in A implies q = p )
assume that A16:
Ball q,
(r / 2) = x
and A17:
q in A
;
q = p
dist p,
p = 0
by METRIC_1:1;
then
p in Ball p,
(r / 2)
by A8, METRIC_1:12;
then
dist q,
p < r / 2
by A13, A16, METRIC_1:12;
then
dist q,
p < r
by A15, XXREAL_0:2;
hence
q = p
by A9, A14, A17;
verum
end;
consider f being
Function of
BALL,
A such that A18:
for
x being
set st
x in BALL holds
S2[
x,
f . x]
from FUNCT_2:sch 1(A12);
reconsider RNG =
rng f as
Subset of
TM by A6, XBOOLE_1:1;
ex
q being
Point of
M st
(
q in A & the
Point of
M in Ball q,
r )
by A10;
then A19:
dom f = BALL
by FUNCT_2:def 1;
then A20:
card RNG c= card BALL
by CARD_1:28;
A21:
for
A9,
B9 being
Subset of
TM st
A9 in BALL &
B9 in BALL &
A9 <> B9 holds
A9 misses B9
proof
let A9,
B9 be
Subset of
TM;
( A9 in BALL & B9 in BALL & A9 <> B9 implies A9 misses B9 )
assume that A22:
A9 in BALL
and A23:
B9 in BALL
and A24:
A9 <> B9
;
A9 misses B9
consider b being
Element of
M such that A25:
Ball b,
(r / 2) = B9
and A26:
b in A
by A23;
consider a being
Element of
M such that A27:
Ball a,
(r / 2) = A9
and A28:
a in A
by A22;
assume
A9 meets B9
;
contradiction
then consider x being
set such that A29:
x in A9
and A30:
x in B9
by XBOOLE_0:3;
reconsider x =
x as
Element of
M by A27, A29;
A31:
dist a,
x < r / 2
by A27, A29, METRIC_1:12;
dist b,
x < r / 2
by A25, A30, METRIC_1:12;
then A32:
(
dist a,
b <= (dist a,x) + (dist x,b) &
(dist a,x) + (dist x,b) < (r / 2) + (r / 2) )
by A31, METRIC_1:4, XREAL_1:10;
dist a,
b >= r
by A9, A24, A25, A26, A27, A28;
hence
contradiction
by A32, XXREAL_0:2;
verum
end;
take
RNG
;
( RNG in bool the carrier of TM & S1[x,RNG] )
thus
RNG in bool the
carrier of
TM
;
S1[x,RNG]
let m be
Nat;
( x = m implies ex G being Subset of TM st
( G = RNG & card G c= iC & ( for p being Element of M ex q being Element of M st
( q in G & dist p,q < 1 / (2 |^ m) ) ) ) )
assume A33:
x = m
;
ex G being Subset of TM st
( G = RNG & card G c= iC & ( for p being Element of M ex q being Element of M st
( q in G & dist p,q < 1 / (2 |^ m) ) ) )
A34:
now let p be
Element of
M;
ex q being Point of M st
( q in RNG & dist p,q < 1 / (2 |^ m) )consider q being
Point of
M such that A35:
q in A
and A36:
p in Ball q,
r
by A10;
take q =
q;
( q in RNG & dist p,q < 1 / (2 |^ m) )A37:
Ball q,
(r / 2) in BALL
by A35;
then
f . (Ball q,(r / 2)) = q
by A18, A35;
hence
(
q in RNG &
dist p,
q < 1
/ (2 |^ m) )
by A19, A33, A36, A37, FUNCT_1:def 5, METRIC_1:12;
verum end;
not
{} in BALL
then
card BALL c= iC
by A1, A21;
hence
ex
G being
Subset of
TM st
(
G = RNG &
card G c= iC & ( for
p being
Element of
M ex
q being
Element of
M st
(
q in G &
dist p,
q < 1
/ (2 |^ m) ) ) )
by A20, A34, XBOOLE_1:1;
verum
end; consider p being
Function of
NAT ,
(bool the carrier of TM) such that A39:
for
x being
set st
x in NAT holds
S1[
x,
p . x]
from FUNCT_2:sch 1(A7);
reconsider Up =
Union p as
Subset of
TM ;
for
U being
Subset of
TM st
U <> {} &
U is
open holds
Up meets U
proof
let U be
Subset of
TM;
( U <> {} & U is open implies Up meets U )
reconsider U9 =
U as
Subset of
M by A3, A4, PCOMPS_2:8;
assume that A40:
U <> {}
and A41:
U is
open
;
Up meets U
consider q being
set such that A42:
q in U
by A40, XBOOLE_0:def 1;
reconsider q =
q as
Element of
M by A3, A4, A42, PCOMPS_2:8;
U9 in Family_open_set M
by A5, A41, PRE_TOPC:def 5;
then consider r being
Real such that A43:
r > 0
and A44:
Ball q,
r c= U9
by A42, PCOMPS_1:def 5;
consider n being
Element of
NAT such that A45:
1
/ (2 |^ n) <= r
by A43, PREPOWER:106;
consider G being
Subset of
TM such that A46:
G = p . n
and
card G c= iC
and A47:
for
p being
Element of
M ex
q being
Element of
M st
(
q in G &
dist p,
q < 1
/ (2 |^ n) )
by A39;
consider qq being
Element of
M such that A48:
qq in G
and A49:
dist q,
qq < 1
/ (2 |^ n)
by A47;
dist q,
qq < r
by A45, A49, XXREAL_0:2;
then A50:
qq in Ball q,
r
by METRIC_1:12;
qq in Up
by A46, A48, PROB_1:25;
hence
Up meets U
by A44, A50, XBOOLE_0:3;
verum
end; then
Up is
dense
by TOPS_1:80;
then A51:
density TM c= card Up
by TOPGEN_1:def 12;
A52:
for
x being
set st
x in dom p holds
card (p . x) c= iC
card (dom p) = omega
by CARD_1:84, FUNCT_2:def 1;
then A53:
card Up c= omega *` iC
by A52, CARD_3:132;
omega *` iC = iC
by Lm5;
hence
density TM c= iC
by A51, A53, XBOOLE_1:1;
verum end;