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 8;
reconsider M =
SpaceMetr ( the
carrier of
TM,
metr) as non
empty MetrSpace by A3, A4, PCOMPS_1:36;
defpred S1[
object ,
object ]
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:4;
A7:
for
x being
object st
x in NAT holds
ex
y being
object st
(
y in bool the
carrier of
TM &
S1[
x,
y] )
proof
let x be
object ;
( x in NAT implies ex y being object st
( y in bool the carrier of TM & S1[x,y] ) )
assume
x in NAT
;
ex y being object 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 ;
A8:
2
|^ n > 0
by PREPOWER:6;
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
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:11, XBOOLE_1:1;
defpred S2[
object ,
object ]
means for
p being
Point of
M st
Ball (
p,
(r / 2))
= $1 &
p in A holds
p = $2;
A12:
for
x being
object st
x in BALL holds
ex
y being
object st
(
y in A &
S2[
x,
y] )
proof
let x be
object ;
( x in BALL implies ex y being object st
( y in A & S2[x,y] ) )
assume
x in BALL
;
ex y being object 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:216;
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:11;
then
dist (
q,
p)
< r / 2
by A13, A16, METRIC_1:11;
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
object 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:12;
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
object 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:11;
dist (
b,
x)
< r / 2
by A25, A30, METRIC_1:11;
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:8;
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 for p being Element of M ex q being Point of M st
( q in RNG & dist (p,q) < 1 / (2 |^ m) )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 3, METRIC_1:11;
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
sequence of
(bool the carrier of TM) such that A39:
for
x being
object 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:4;
assume that A40:
U <> {}
and A41:
U is
open
;
Up meets U
consider q being
object 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:4;
U9 in Family_open_set M
by A5, A41;
then consider r being
Real such that A43:
r > 0
and A44:
Ball (
q,
r)
c= U9
by A42, PCOMPS_1:def 4;
consider n being
Nat such that A45:
1
/ (2 |^ n) <= r
by A43, PREPOWER:92;
A46:
n in NAT
by ORDINAL1:def 12;
consider G being
Subset of
TM such that A47:
G = p . n
and
card G c= iC
and A48:
for
p being
Element of
M ex
q being
Element of
M st
(
q in G &
dist (
p,
q)
< 1
/ (2 |^ n) )
by A39, A46;
consider qq being
Element of
M such that A49:
qq in G
and A50:
dist (
q,
qq)
< 1
/ (2 |^ n)
by A48;
dist (
q,
qq)
< r
by A45, A50, XXREAL_0:2;
then A51:
qq in Ball (
q,
r)
by METRIC_1:11;
qq in Up
by A47, A49, PROB_1:12;
hence
Up meets U
by A44, A51, XBOOLE_0:3;
verum
end; then
Up is
dense
by TOPS_1:45;
then A52:
density TM c= card Up
by TOPGEN_1:def 12;
A53:
for
x being
object st
x in dom p holds
card (p . x) c= iC
card (dom p) = omega
by CARD_1:47, FUNCT_2:def 1;
then A54:
card Up c= omega *` iC
by A53, CARD_2:86;
omega *` iC = iC
by Lm5;
hence
density TM c= iC
by A52, A54;
verum end;