let TM be metrizable TopSpace; :: thesis: for iC being infinite Cardinal
for B being Basis of TM st ( for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds
ex Gm being Subset-Family of TM st
( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) ) holds
ex underB being Basis of TM st
( underB c= B & card underB c= iC )
let iC be infinite Cardinal; :: thesis: for B being Basis of TM st ( for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds
ex Gm being Subset-Family of TM st
( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) ) holds
ex underB being Basis of TM st
( underB c= B & card underB c= iC )
let B be Basis of TM; :: thesis: ( ( for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds
ex Gm being Subset-Family of TM st
( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) ) implies ex underB being Basis of TM st
( underB c= B & card underB c= iC ) )
assume A1:
for F being Subset-Family of TM st F is open & F is Cover of TM holds
ex G being Subset-Family of TM st
( G c= F & G is Cover of TM & card G c= iC )
; :: thesis: ex underB being Basis of TM st
( underB c= B & card underB c= iC )
per cases
( TM is empty or not TM is empty )
;
suppose A3:
not
TM is
empty
;
:: thesis: ex underB being Basis of TM st
( underB c= B & card underB c= iC )set TOP = the
topology of
TM;
set cT = the
carrier of
TM;
consider 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 Tm =
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
open Subset-Family of
TM st
(
G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball p,(1 / (2 |^ n)) ) } &
G is
Cover of
TM &
card G c= iC & $2
= G );
A6:
B c= the
topology of
TM
by CANTOR_1:def 2;
A7:
for
x being
set st
x in NAT holds
ex
y being
set st
S1[
x,
y]
proof
let x be
set ;
:: thesis: ( x in NAT implies ex y being set st S1[x,y] )
assume
x in NAT
;
:: thesis: ex y being set st S1[x,y]
then reconsider n =
x as
Nat ;
set F =
{ U where U is Subset of TM : ( U in B & ex p being Element of Tm st U c= Ball p,(1 / (2 |^ n)) ) } ;
A8:
{ U where U is Subset of TM : ( U in B & ex p being Element of Tm st U c= Ball p,(1 / (2 |^ n)) ) } c= the
topology of
TM
then reconsider F =
{ U where U is Subset of TM : ( U in B & ex p being Element of Tm st U c= Ball p,(1 / (2 |^ n)) ) } as
Subset-Family of
TM by XBOOLE_1:1;
reconsider F =
F as
open Subset-Family of
TM by A8, CANTOR_1:3, TOPS_2:18;
the
carrier of
TM c= union F
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in the carrier of TM or y in union F )
assume A9:
y in the
carrier of
TM
;
:: thesis: y in union F
then reconsider p =
y as
Point of
TM ;
reconsider q =
y as
Element of
Tm by A3, A4, A9, PCOMPS_2:8;
( 2
|^ n > 0 &
dist q,
q = 0 )
by METRIC_1:1, NEWTON:102;
then A10:
q in Ball q,
(1 / (2 |^ n))
by METRIC_1:12;
reconsider BALL =
Ball q,
(1 / (2 |^ n)) as
Subset of
TM by A3, A4, PCOMPS_2:8;
BALL in Family_open_set Tm
by PCOMPS_1:33;
then
BALL is
open
by A5, PRE_TOPC:def 5;
then consider U being
Subset of
TM such that A11:
U in B
and A12:
p in U
and A13:
U c= BALL
by A10, YELLOW_9:31;
U in F
by A11, A13;
hence
y in union F
by A12, TARSKI:def 4;
:: thesis: verum
end;
then
F is
Cover of
TM
by SETFAM_1:def 12;
then consider G being
Subset-Family of
TM such that A14:
G c= F
and A15:
(
G is
Cover of
TM &
card G c= iC )
by A1;
take
G
;
:: thesis: S1[x,G]
let m be
Nat;
:: thesis: ( x = m implies ex G being open Subset-Family of TM st
( G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball p,(1 / (2 |^ m)) ) } & G is Cover of TM & card G c= iC & G = G ) )
assume A16:
x = m
;
:: thesis: ex G being open Subset-Family of TM st
( G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball p,(1 / (2 |^ m)) ) } & G is Cover of TM & card G c= iC & G = G )
G is
open
by A14, TOPS_2:18;
hence
ex
G being
open Subset-Family of
TM st
(
G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball p,(1 / (2 |^ m)) ) } &
G is
Cover of
TM &
card G c= iC &
G = G )
by A14, A15, A16;
:: thesis: verum
end; consider f being
Function such that A17:
(
dom f = NAT & ( for
e being
set st
e in NAT holds
S1[
e,
f . e] ) )
from CLASSES1:sch 1(A7);
A18:
union (rng f) c= B
then reconsider Urngf =
union (rng f) as
Subset-Family of
TM by XBOOLE_1:1;
for
A being
Subset of
TM st
A is
open holds
for
p being
Point of
TM st
p in A holds
ex
a being
Subset of
TM st
(
a in Urngf &
p in a &
a c= A )
proof
let A be
Subset of
TM;
:: thesis: ( A is open implies for p being Point of TM st p in A holds
ex a being Subset of TM st
( a in Urngf & p in a & a c= A ) )
assume A23:
A is
open
;
:: thesis: for p being Point of TM st p in A holds
ex a being Subset of TM st
( a in Urngf & p in a & a c= A )
A24:
A in Family_open_set Tm
by A5, A23, PRE_TOPC:def 5;
let p be
Point of
TM;
:: thesis: ( p in A implies ex a being Subset of TM st
( a in Urngf & p in a & a c= A ) )
assume A25:
p in A
;
:: thesis: ex a being Subset of TM st
( a in Urngf & p in a & a c= A )
reconsider p' =
p as
Element of
Tm by A3, A4, PCOMPS_2:8;
consider r being
Real such that A26:
r > 0
and A27:
Ball p',
r c= A
by A24, A25, PCOMPS_1:def 5;
consider n being
Element of
NAT such that A28:
1
/ (2 |^ n) <= r / 2
by A26, PREPOWER:106;
consider G being
open Subset-Family of
TM such that A29:
G c= { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball p,(1 / (2 |^ n)) ) }
and A30:
G is
Cover of
TM
and
card G c= iC
and A31:
f . n = G
by A17;
[#] TM = union G
by A30, SETFAM_1:60;
then consider a being
set such that A32:
p in a
and A33:
a in G
by A3, TARSKI:def 4;
a in { U where U is Subset of TM : ( U in B & ex p being Point of Tm st U c= Ball p,(1 / (2 |^ n)) ) }
by A29, A33;
then consider U being
Subset of
TM such that A34:
a = U
and
U in B
and A35:
ex
p being
Point of
Tm st
U c= Ball p,
(1 / (2 |^ n))
;
take
U
;
:: thesis: ( U in Urngf & p in U & U c= A )
f . n in rng f
by A17, FUNCT_1:def 5;
hence
(
U in Urngf &
p in U )
by A31, A32, A33, A34, TARSKI:def 4;
:: thesis: U c= A
thus
U c= A
:: thesis: verumproof
let u' be
set ;
:: according to TARSKI:def 3 :: thesis: ( not u' in U or u' in A )
consider pp being
Element of
Tm such that A36:
U c= Ball pp,
(1 / (2 |^ n))
by A35;
assume A37:
u' in U
;
:: thesis: u' in A
then reconsider u =
u' as
Element of
Tm by A3, A4, PCOMPS_2:8;
dist pp,
u < 1
/ (2 |^ n)
by A36, A37, METRIC_1:12;
then A38:
dist pp,
u < r / 2
by A28, XXREAL_0:2;
dist pp,
p' < 1
/ (2 |^ n)
by A32, A34, A36, METRIC_1:12;
then
dist p',
pp < r / 2
by A28, XXREAL_0:2;
then
(
dist p',
u <= (dist p',pp) + (dist pp,u) &
(dist p',pp) + (dist pp,u) < (r / 2) + (r / 2) )
by A38, METRIC_1:4, XREAL_1:10;
then
dist p',
u < (r / 2) + (r / 2)
by XXREAL_0:2;
then
u in Ball p',
r
by METRIC_1:12;
hence
u' in A
by A27;
:: thesis: verum
end;
end; then reconsider Urngf =
Urngf as
Basis of
TM by A6, A18, XBOOLE_1:1, YELLOW_9:32;
take
Urngf
;
:: thesis: ( Urngf c= B & card Urngf c= iC )
for
x being
set st
x in dom f holds
card (f . x) c= iC
then
card (Union f) c= omega *` iC
by A17, CARD_1:84, CARD_3:132;
hence
(
Urngf c= B &
card Urngf c= iC )
by A18, Lm6;
:: thesis: verum end;