let Z be RealNormSpace; for H being non empty Subset of (MetricSpaceNorm Z) holds
( (MetricSpaceNorm Z) | H is totally_bounded iff (MetricSpaceNorm Z) | (Cl H) is totally_bounded )
let H be non empty Subset of (MetricSpaceNorm Z); ( (MetricSpaceNorm Z) | H is totally_bounded iff (MetricSpaceNorm Z) | (Cl H) is totally_bounded )
reconsider F = H as non empty Subset of Z ;
set K = Cl H;
set M = MetricSpaceNorm Z;
consider D being Subset of (TopSpaceMetr (MetricSpaceNorm Z)) such that
A1:
( D = H & Cl H = Cl D )
by Def1;
A2:
H c= Cl H
by A1, PRE_TOPC:18;
A3:
the carrier of ((MetricSpaceNorm Z) | H) = H
by TOPMETR:def 2;
A4:
the carrier of ((MetricSpaceNorm Z) | (Cl H)) = Cl H
by TOPMETR:def 2;
A5:
Cl F = Cl H
by Th1;
hereby ( (MetricSpaceNorm Z) | (Cl H) is totally_bounded implies (MetricSpaceNorm Z) | H is totally_bounded )
assume A6:
(MetricSpaceNorm Z) | H is
totally_bounded
;
(MetricSpaceNorm Z) | (Cl H) is totally_bounded
for
r being
Real st
r > 0 holds
ex
L being
Subset-Family of
((MetricSpaceNorm Z) | (Cl H)) st
(
L is
finite & the
carrier of
((MetricSpaceNorm Z) | (Cl H)) = union L & ( for
C being
Subset of
((MetricSpaceNorm Z) | (Cl H)) st
C in L holds
ex
w being
Element of
((MetricSpaceNorm Z) | (Cl H)) st
C = Ball (
w,
r) ) )
proof
let r be
Real;
( r > 0 implies ex L being Subset-Family of ((MetricSpaceNorm Z) | (Cl H)) st
( L is finite & the carrier of ((MetricSpaceNorm Z) | (Cl H)) = union L & ( for C being Subset of ((MetricSpaceNorm Z) | (Cl H)) st C in L holds
ex w being Element of ((MetricSpaceNorm Z) | (Cl H)) st C = Ball (w,r) ) ) )
assume A7:
r > 0
;
ex L being Subset-Family of ((MetricSpaceNorm Z) | (Cl H)) st
( L is finite & the carrier of ((MetricSpaceNorm Z) | (Cl H)) = union L & ( for C being Subset of ((MetricSpaceNorm Z) | (Cl H)) st C in L holds
ex w being Element of ((MetricSpaceNorm Z) | (Cl H)) st C = Ball (w,r) ) )
then consider L0 being
Subset-Family of
((MetricSpaceNorm Z) | H) such that A8:
(
L0 is
finite & the
carrier of
((MetricSpaceNorm Z) | H) = union L0 & ( for
C being
Subset of
((MetricSpaceNorm Z) | H) st
C in L0 holds
ex
w being
Element of
((MetricSpaceNorm Z) | H) st
C = Ball (
w,
(r / 2)) ) )
by A6;
defpred S1[
object ,
object ]
means ex
w being
Point of
((MetricSpaceNorm Z) | H) st
( $2
= w & $1
= Ball (
w,
(r / 2)) );
A9:
for
D being
object st
D in L0 holds
ex
w being
object st
(
w in the
carrier of
((MetricSpaceNorm Z) | H) &
S1[
D,
w] )
consider U0 being
Function of
L0, the
carrier of
((MetricSpaceNorm Z) | H) such that A12:
for
D being
object st
D in L0 holds
S1[
D,
U0 . D]
from FUNCT_2:sch 1(A9);
A13:
for
D being
object st
D in L0 holds
D = Ball (
(U0 /. D),
(r / 2))
defpred S2[
object ,
object ]
means ex
x being
Point of
((MetricSpaceNorm Z) | (Cl H)) st
( $1
= x & $2
= Ball (
x,
r) );
A16:
for
w being
object st
w in the
carrier of
((MetricSpaceNorm Z) | H) holds
ex
B being
object st
(
B in bool the
carrier of
((MetricSpaceNorm Z) | (Cl H)) &
S2[
w,
B] )
consider B being
Function of the
carrier of
((MetricSpaceNorm Z) | H),
(bool the carrier of ((MetricSpaceNorm Z) | (Cl H))) such that A17:
for
x being
object st
x in the
carrier of
((MetricSpaceNorm Z) | H) holds
S2[
x,
B . x]
from FUNCT_2:sch 1(A16);
A19:
dom U0 = L0
by FUNCT_2:def 1;
reconsider L =
B .: (rng U0) as
Subset-Family of
((MetricSpaceNorm Z) | (Cl H)) ;
take
L
;
( L is finite & the carrier of ((MetricSpaceNorm Z) | (Cl H)) = union L & ( for C being Subset of ((MetricSpaceNorm Z) | (Cl H)) st C in L holds
ex w being Element of ((MetricSpaceNorm Z) | (Cl H)) st C = Ball (w,r) ) )
thus
L is
finite
by A8;
( the carrier of ((MetricSpaceNorm Z) | (Cl H)) = union L & ( for C being Subset of ((MetricSpaceNorm Z) | (Cl H)) st C in L holds
ex w being Element of ((MetricSpaceNorm Z) | (Cl H)) st C = Ball (w,r) ) )
the
carrier of
((MetricSpaceNorm Z) | (Cl H)) c= union L
proof
let z be
object ;
TARSKI:def 3 ( not z in the carrier of ((MetricSpaceNorm Z) | (Cl H)) or z in union L )
assume A20:
z in the
carrier of
((MetricSpaceNorm Z) | (Cl H))
;
z in union L
then consider seq being
sequence of
Z such that A21:
(
rng seq c= F &
seq is
convergent &
lim seq = z )
by A4, A5, NORMSP_3:6;
consider N being
Nat such that A22:
for
n being
Nat st
N <= n holds
||.((seq . n) - (lim seq)).|| < r / 2
by NORMSP_1:def 7, A21, A7;
A23:
||.((seq . N) - (lim seq)).|| < r / 2
by A22;
A24:
(
dom seq = NAT &
N in NAT )
by FUNCT_2:def 1, ORDINAL1:def 12;
then
seq . N in H
by A21, FUNCT_1:3;
then consider D being
set such that A25:
(
seq . N in D &
D in L0 )
by A8, A3, TARSKI:def 4;
reconsider y0 =
seq . N as
Point of
((MetricSpaceNorm Z) | H) by A24, A21, FUNCT_1:3, A3;
A26:
D = Ball (
(U0 /. D),
(r / 2))
by A13, A25;
y0 in { y where y is Point of ((MetricSpaceNorm Z) | H) : dist ((U0 /. D),y) < r / 2 }
by METRIC_1:def 14, A25, A26;
then A27:
ex
y being
Point of
((MetricSpaceNorm Z) | H) st
(
y0 = y &
dist (
(U0 /. D),
y)
< r / 2 )
;
reconsider y01 =
y0 as
Point of
(MetricSpaceNorm Z) ;
reconsider u0d1 =
U0 /. D as
Point of
(MetricSpaceNorm Z) by TOPMETR:def 1, TARSKI:def 3;
A28:
dist (
u0d1,
y01)
< r / 2
by A27, TOPMETR:def 1;
U0 /. D in H
by A3;
then reconsider u0d =
U0 /. D as
Point of
Z ;
A29:
||.(u0d - (seq . N)).|| < r / 2
by A28, NORMSP_2:def 1;
u0d - (lim seq) =
((u0d - (seq . N)) + (seq . N)) - (lim seq)
by RLVECT_4:1
.=
(u0d - (seq . N)) + ((seq . N) - (lim seq))
by RLVECT_1:28
;
then A30:
||.(u0d - (lim seq)).|| <= ||.(u0d - (seq . N)).|| + ||.((seq . N) - (lim seq)).||
by NORMSP_1:def 1;
||.(u0d - (seq . N)).|| + ||.((seq . N) - (lim seq)).|| < (r / 2) + (r / 2)
by XREAL_1:8, A29, A23;
then A31:
||.(u0d - (lim seq)).|| < r
by A30, XXREAL_0:2;
reconsider w =
U0 /. D as
Point of
((MetricSpaceNorm Z) | (Cl H)) by A2, A3, A4;
reconsider v =
lim seq as
Point of
((MetricSpaceNorm Z) | (Cl H)) by A21, A20;
reconsider v1 =
v as
Point of
(MetricSpaceNorm Z) ;
dist (
u0d1,
v1)
< r
by A31, NORMSP_2:def 1;
then
dist (
w,
v)
< r
by TOPMETR:def 1;
then
v in { y where y is Point of ((MetricSpaceNorm Z) | (Cl H)) : dist (w,y) < r }
;
then A32:
v in Ball (
w,
r)
by METRIC_1:def 14;
A33:
ex
w being
Point of
((MetricSpaceNorm Z) | (Cl H)) st
(
U0 /. D = w &
B . (U0 /. D) = Ball (
w,
r) )
by A17;
U0 /. D in rng U0
by PARTFUN2:2, A25, A19;
then
Ball (
w,
r)
in L
by A33, FUNCT_2:35;
hence
z in union L
by A21, A32, TARSKI:def 4;
verum
end;
hence
the
carrier of
((MetricSpaceNorm Z) | (Cl H)) = union L
;
for C being Subset of ((MetricSpaceNorm Z) | (Cl H)) st C in L holds
ex w being Element of ((MetricSpaceNorm Z) | (Cl H)) st C = Ball (w,r)
thus
for
C being
Subset of
((MetricSpaceNorm Z) | (Cl H)) st
C in L holds
ex
w being
Element of
((MetricSpaceNorm Z) | (Cl H)) st
C = Ball (
w,
r)
verum
end; hence
(MetricSpaceNorm Z) | (Cl H) is
totally_bounded
;
verum
end;
assume A37:
(MetricSpaceNorm Z) | (Cl H) is totally_bounded
; (MetricSpaceNorm Z) | H is totally_bounded
thus
(MetricSpaceNorm Z) | H is totally_bounded
verumproof
let r be
Real;
TBSP_1:def 1 ( r <= 0 or ex b1 being Element of bool (bool the carrier of ((MetricSpaceNorm Z) | H)) st
( b1 is finite & the carrier of ((MetricSpaceNorm Z) | H) = union b1 & ( for b2 being Element of bool the carrier of ((MetricSpaceNorm Z) | H) holds
( not b2 in b1 or ex b3 being Element of the carrier of ((MetricSpaceNorm Z) | H) st b2 = Ball (b3,r) ) ) ) )
assume
r > 0
;
ex b1 being Element of bool (bool the carrier of ((MetricSpaceNorm Z) | H)) st
( b1 is finite & the carrier of ((MetricSpaceNorm Z) | H) = union b1 & ( for b2 being Element of bool the carrier of ((MetricSpaceNorm Z) | H) holds
( not b2 in b1 or ex b3 being Element of the carrier of ((MetricSpaceNorm Z) | H) st b2 = Ball (b3,r) ) ) )
then consider L0 being
Subset-Family of
((MetricSpaceNorm Z) | (Cl H)) such that A38:
(
L0 is
finite & the
carrier of
((MetricSpaceNorm Z) | (Cl H)) = union L0 & ( for
C being
Subset of
((MetricSpaceNorm Z) | (Cl H)) st
C in L0 holds
ex
w being
Element of
((MetricSpaceNorm Z) | (Cl H)) st
C = Ball (
w,
(r / 2)) ) )
by A37;
A39:
for
x being
object st
x in H holds
ex
B being
Subset of
((MetricSpaceNorm Z) | (Cl H)) st
(
x in B &
B in L0 )
set BL =
{ B where B is Subset of ((MetricSpaceNorm Z) | (Cl H)) : ( B in L0 & H /\ B <> {} ) } ;
consider x being
object such that A42:
x in H
by XBOOLE_0:def 1;
consider B being
Subset of
((MetricSpaceNorm Z) | (Cl H)) such that A43:
(
x in B &
B in L0 )
by A39, A42;
B /\ H <> {}
by A42, A43, XBOOLE_0:def 4;
then A44:
B in { B where B is Subset of ((MetricSpaceNorm Z) | (Cl H)) : ( B in L0 & H /\ B <> {} ) }
by A43;
{ B where B is Subset of ((MetricSpaceNorm Z) | (Cl H)) : ( B in L0 & H /\ B <> {} ) } c= L0
then reconsider BL =
{ B where B is Subset of ((MetricSpaceNorm Z) | (Cl H)) : ( B in L0 & H /\ B <> {} ) } as non
empty finite set by A44, A38;
defpred S1[
object ,
object ]
means ex
w being
Point of
((MetricSpaceNorm Z) | H) ex
B being
Subset of
((MetricSpaceNorm Z) | (Cl H)) st
(
B = $1 &
w in B &
B in L0 & $2
= Ball (
w,
r) );
A45:
for
D being
object st
D in BL holds
ex
w being
object st
(
w in bool the
carrier of
((MetricSpaceNorm Z) | H) &
S1[
D,
w] )
proof
let D be
object ;
( D in BL implies ex w being object st
( w in bool the carrier of ((MetricSpaceNorm Z) | H) & S1[D,w] ) )
assume
D in BL
;
ex w being object st
( w in bool the carrier of ((MetricSpaceNorm Z) | H) & S1[D,w] )
then consider B being
Subset of
((MetricSpaceNorm Z) | (Cl H)) such that A46:
(
B = D &
B in L0 &
H /\ B <> {} )
;
consider x being
object such that A47:
x in H /\ B
by XBOOLE_0:def 1, A46;
A48:
(
x in H &
x in B )
by XBOOLE_0:def 4, A47;
reconsider x =
x as
Point of
((MetricSpaceNorm Z) | H) by A3, XBOOLE_0:def 4, A47;
set Z =
Ball (
x,
r);
S1[
D,
Ball (
x,
r)]
by A46, A48;
hence
ex
w being
object st
(
w in bool the
carrier of
((MetricSpaceNorm Z) | H) &
S1[
D,
w] )
;
verum
end;
consider U0 being
Function of
BL,
(bool the carrier of ((MetricSpaceNorm Z) | H)) such that A49:
for
D being
object st
D in BL holds
S1[
D,
U0 . D]
from FUNCT_2:sch 1(A45);
set L =
rng U0;
A50:
dom U0 = BL
by FUNCT_2:def 1;
reconsider L =
rng U0 as
Subset-Family of
((MetricSpaceNorm Z) | H) ;
take
L
;
( L is finite & the carrier of ((MetricSpaceNorm Z) | H) = union L & ( for b1 being Element of bool the carrier of ((MetricSpaceNorm Z) | H) holds
( not b1 in L or ex b2 being Element of the carrier of ((MetricSpaceNorm Z) | H) st b1 = Ball (b2,r) ) ) )
thus
L is
finite
;
( the carrier of ((MetricSpaceNorm Z) | H) = union L & ( for b1 being Element of bool the carrier of ((MetricSpaceNorm Z) | H) holds
( not b1 in L or ex b2 being Element of the carrier of ((MetricSpaceNorm Z) | H) st b1 = Ball (b2,r) ) ) )
the
carrier of
((MetricSpaceNorm Z) | H) c= union L
proof
let z be
object ;
TARSKI:def 3 ( not z in the carrier of ((MetricSpaceNorm Z) | H) or z in union L )
assume A51:
z in the
carrier of
((MetricSpaceNorm Z) | H)
;
z in union L
then consider B being
Subset of
((MetricSpaceNorm Z) | (Cl H)) such that A52:
(
z in B &
B in L0 )
by A39, A3;
z in H /\ B
by A51, A3, A52, XBOOLE_0:def 4;
then A53:
B in BL
by A52;
then consider w being
Point of
((MetricSpaceNorm Z) | H),
D being
Subset of
((MetricSpaceNorm Z) | (Cl H)) such that A54:
(
D = B &
w in D &
D in L0 &
U0 . B = Ball (
w,
r) )
by A49;
consider y being
Element of
((MetricSpaceNorm Z) | (Cl H)) such that A55:
D = Ball (
y,
(r / 2))
by A54, A38;
reconsider x =
z as
Point of
((MetricSpaceNorm Z) | H) by A51;
reconsider x1 =
x,
w1 =
w as
Point of
((MetricSpaceNorm Z) | (Cl H)) by A52, A54;
reconsider x2 =
x1,
w2 =
w1 as
Point of
(MetricSpaceNorm Z) by TOPMETR:def 1, TARSKI:def 3;
x1 in { s where s is Point of ((MetricSpaceNorm Z) | (Cl H)) : dist (y,s) < r / 2 }
by METRIC_1:def 14, A52, A54, A55;
then A56:
ex
s being
Point of
((MetricSpaceNorm Z) | (Cl H)) st
(
x1 = s &
dist (
y,
s)
< r / 2 )
;
w1 in { s where s is Point of ((MetricSpaceNorm Z) | (Cl H)) : dist (y,s) < r / 2 }
by METRIC_1:def 14, A54, A55;
then A57:
ex
s being
Point of
((MetricSpaceNorm Z) | (Cl H)) st
(
w1 = s &
dist (
y,
s)
< r / 2 )
;
A58:
dist (
w1,
x1)
<= (dist (w1,y)) + (dist (y,x1))
by METRIC_1:4;
(dist (w1,y)) + (dist (y,x1)) < (r / 2) + (r / 2)
by A57, A56, XREAL_1:8;
then
dist (
w1,
x1)
< r
by A58, XXREAL_0:2;
then
dist (
w2,
x2)
< r
by TOPMETR:def 1;
then
dist (
w,
x)
< r
by TOPMETR:def 1;
then
x in { s where s is Point of ((MetricSpaceNorm Z) | H) : dist (w,s) < r }
;
then A59:
z in U0 . B
by A54, METRIC_1:def 14;
U0 . B in rng U0
by A53, A50, FUNCT_1:def 3;
hence
z in union L
by A59, TARSKI:def 4;
verum
end;
hence
the
carrier of
((MetricSpaceNorm Z) | H) = union L
;
for b1 being Element of bool the carrier of ((MetricSpaceNorm Z) | H) holds
( not b1 in L or ex b2 being Element of the carrier of ((MetricSpaceNorm Z) | H) st b1 = Ball (b2,r) )
thus
for
C being
Subset of
((MetricSpaceNorm Z) | H) st
C in L holds
ex
w being
Element of
((MetricSpaceNorm Z) | H) st
C = Ball (
w,
r)
verum
end;