let TM be metrizable TopSpace; 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; 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; ( ( 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 )
; 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
;
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 8;
reconsider Tm =
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
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 TOPS_2:64;
A7:
for
x being
object st
x in NAT holds
ex
y being
object st
S1[
x,
y]
proof
let x be
object ;
( x in NAT implies ex y being object st S1[x,y] )
assume
x in NAT
;
ex y being object 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, TOPS_2:11;
the
carrier of
TM c= union F
proof
let y be
object ;
TARSKI:def 3 ( not y in the carrier of TM or y in union F )
assume A9:
y in the
carrier of
TM
;
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:4;
( 2
|^ n > 0 &
dist (
q,
q)
= 0 )
by METRIC_1:1, NEWTON:83;
then A10:
q in Ball (
q,
(1 / (2 |^ n)))
by METRIC_1:11;
reconsider BALL =
Ball (
q,
(1 / (2 |^ n))) as
Subset of
TM by A3, A4, PCOMPS_2:4;
BALL in Family_open_set Tm
by PCOMPS_1:29;
then
BALL is
open
by A5;
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;
verum
end;
then
F is
Cover of
TM
by SETFAM_1:def 11;
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
;
S1[x,G]
let m be
Nat;
( 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
;
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:11;
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;
verum
end; consider f being
Function such that A17:
(
dom f = NAT & ( for
e being
object 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;
( 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
A is
open
;
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 )
then A23:
A in Family_open_set Tm
by A5;
let p be
Point of
TM;
( p in A implies ex a being Subset of TM st
( a in Urngf & p in a & a c= A ) )
assume A24:
p in A
;
ex a being Subset of TM st
( a in Urngf & p in a & a c= A )
reconsider p9 =
p as
Element of
Tm by A3, A4, PCOMPS_2:4;
consider r being
Real such that A25:
r > 0
and A26:
Ball (
p9,
r)
c= A
by A23, A24, PCOMPS_1:def 4;
consider n being
Nat such that A27:
1
/ (2 |^ n) <= r / 2
by A25, PREPOWER:92;
A28:
n in NAT
by ORDINAL1:def 12;
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, A28;
[#] TM = union G
by A30, SETFAM_1:45;
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
;
( U in Urngf & p in U & U c= A )
f . n in rng f
by A17, FUNCT_1:def 3, A28;
hence
(
U in Urngf &
p in U )
by A31, A32, A33, A34, TARSKI:def 4;
U c= A
thus
U c= A
verumproof
let u9 be
object ;
TARSKI:def 3 ( not u9 in U or u9 in A )
consider pp being
Element of
Tm such that A36:
U c= Ball (
pp,
(1 / (2 |^ n)))
by A35;
assume A37:
u9 in U
;
u9 in A
then reconsider u =
u9 as
Element of
Tm by A3, A4, PCOMPS_2:4;
dist (
pp,
u)
< 1
/ (2 |^ n)
by A36, A37, METRIC_1:11;
then A38:
dist (
pp,
u)
< r / 2
by A27, XXREAL_0:2;
dist (
pp,
p9)
< 1
/ (2 |^ n)
by A32, A34, A36, METRIC_1:11;
then
dist (
p9,
pp)
< r / 2
by A27, XXREAL_0:2;
then
(
dist (
p9,
u)
<= (dist (p9,pp)) + (dist (pp,u)) &
(dist (p9,pp)) + (dist (pp,u)) < (r / 2) + (r / 2) )
by A38, METRIC_1:4, XREAL_1:8;
then
dist (
p9,
u)
< (r / 2) + (r / 2)
by XXREAL_0:2;
then
u in Ball (
p9,
r)
by METRIC_1:11;
hence
u9 in A
by A26;
verum
end;
end; then reconsider Urngf =
Urngf as
Basis of
TM by A6, A18, XBOOLE_1:1, YELLOW_9:32;
take
Urngf
;
( Urngf c= B & card Urngf c= iC )
for
x being
object st
x in dom f holds
card (f . x) c= iC
then
card (Union f) c= omega *` iC
by A17, CARD_1:47, CARD_2:86;
hence
(
Urngf c= B &
card Urngf c= iC )
by A18, Lm5;
verum end;