let M be non empty MetrSpace; for S being non empty compact TopSpace
for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous )
let S be non empty compact TopSpace; for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous )
let T be NormedLinearTopSpace; ( S = TopSpaceMetr M & T is complete implies for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous ) )
assume A1:
( S = TopSpaceMetr M & T is complete )
; for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous )
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded holds
( G is equibounded & G is equicontinuous )
let H be non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))); ( G = H & (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded implies ( G is equibounded & G is equicontinuous ) )
assume A2:
G = H
; ( not (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded or ( G is equibounded & G is equicontinuous ) )
set Z = R_NormSpace_of_ContinuousFunctions (S,T);
set MZH = (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H;
A3:
the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) = H
by TOPMETR:def 2;
assume A4:
(MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded
; ( G is equibounded & G is equicontinuous )
consider L being Subset-Family of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A5:
( L is finite & the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) = union L & ( for C being Subset of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st C in L holds
ex w being Element of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st C = Ball (w,1) ) )
by A4;
defpred S1[ object , object ] means ex w being Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( $2 = w & $1 = Ball (w,1) );
A6:
for D being object st D in L holds
ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S1[D,w] )
proof
let D be
object ;
( D in L implies ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S1[D,w] ) )
assume A7:
D in L
;
ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S1[D,w] )
then reconsider D0 =
D as
Subset of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
consider w being
Element of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that A8:
D0 = Ball (
w,1)
by A5, A7;
take
w
;
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S1[D,w] )
thus
(
w in the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) &
S1[
D,
w] )
by A8;
verum
end;
consider U being Function of L, the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A9:
for D being object st D in L holds
S1[D,U . D]
from FUNCT_2:sch 1(A6);
A10:
for D being object st D in L holds
D = Ball ((U /. D),1)
set NF = the normF of (R_NormSpace_of_ContinuousFunctions (S,T));
A13:
dom U = L
by FUNCT_2:def 1;
reconsider NFU = the normF of (R_NormSpace_of_ContinuousFunctions (S,T)) .: (rng U) as finite Subset of REAL by A5;
consider xx being object such that
A14:
xx in L
by XBOOLE_0:def 1, A5, ZFMISC_1:2;
rng U <> {}
by A13, A14, FUNCT_1:3;
then consider xx being object such that
A15:
xx in rng U
by XBOOLE_0:def 1;
reconsider xx = xx as Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A15;
set d0 = upper_bound NFU;
A16:
for r being Real st r in NFU holds
r <= upper_bound NFU
by SEQ_4:def 1;
set K = (upper_bound NFU) + 1;
for f being Function of the carrier of M, the carrier of T st f in G holds
for x being Element of M holds ||.(f . x).|| <= (upper_bound NFU) + 1
proof
let f be
Function of the
carrier of
M, the
carrier of
T;
( f in G implies for x being Element of M holds ||.(f . x).|| <= (upper_bound NFU) + 1 )
assume
f in G
;
for x being Element of M holds ||.(f . x).|| <= (upper_bound NFU) + 1
then consider C being
set such that A17:
(
f in C &
C in L )
by A5, TARSKI:def 4, A3, A2;
reconsider C =
C as
Subset of the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A17;
reconsider pf =
f as
Element of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A17;
A18:
pf in H
by A3;
set pg =
U /. C;
reconsider pg =
U /. C as
Element of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
A19:
C = Ball (
pg,1)
by A10, A17;
A20:
pg in H
by A3;
then
pg in R_NormSpace_of_ContinuousFunctions (
S,
T)
;
then
ex
f being
Function of the
carrier of
S, the
carrier of
T st
(
pg = f &
f is
continuous )
;
then reconsider g =
pg as
Function of
S,
T ;
pf in { y where y is Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) : dist (pg,y) < 1 }
by METRIC_1:def 14, A17, A19;
then A21:
ex
y being
Point of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
(
pf = y &
dist (
pg,
y)
< 1 )
;
reconsider ppf =
pf,
ppg =
pg as
Element of
(MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) by A18, A20;
A22:
dist (
ppg,
ppf)
< 1
by A21, TOPMETR:def 1;
reconsider pppf =
ppf,
pppg =
ppg as
Point of
(R_NormSpace_of_ContinuousFunctions (S,T)) ;
A23:
||.(pppg - pppf).|| < 1
by A22, NORMSP_2:def 1;
pppf = (pppf - pppg) + pppg
by RLVECT_4:1;
then
||.pppf.|| <= ||.(pppf - pppg).|| + ||.pppg.||
by NORMSP_1:def 1;
then A24:
||.pppf.|| <= ||.(pppg - pppf).|| + ||.pppg.||
by NORMSP_1:7;
A25:
C in dom U
by FUNCT_2:def 1, A17;
U . C in rng U
by FUNCT_1:3, A13, A17;
then
pg in rng U
by A25, PARTFUN1:def 6;
then
||.pppg.|| <= upper_bound NFU
by A16, FUNCT_2:35;
then
||.(pppg - pppf).|| + ||.pppg.|| <= 1
+ (upper_bound NFU)
by XREAL_1:8, A23;
then A26:
||.pppf.|| <= (upper_bound NFU) + 1
by A24, XXREAL_0:2;
let x be
Element of
M;
||.(f . x).|| <= (upper_bound NFU) + 1
reconsider x0 =
x as
Point of
S by A1;
reconsider f0 =
f as
Function of the
carrier of
S, the
carrier of
T by A1;
||.(f0 . x0).|| <= ||.pppf.||
by C0SP3:37;
hence
||.(f . x).|| <= (upper_bound NFU) + 1
by A26, XXREAL_0:2;
verum
end;
hence
G is equibounded
; G is equicontinuous
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) )
proof
let e be
Real;
( 0 < e implies ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) ) )
assume A27:
0 < e
;
ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) )
then consider L being
Subset-Family of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that A28:
(
L is
finite & the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) = union L & ( for
C being
Subset of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
C in L holds
ex
w being
Element of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
C = Ball (
w,
(e / 3)) ) )
by A4;
defpred S2[
object ,
object ]
means ex
w being
Point of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( $2
= w & $1
= Ball (
w,
(e / 3)) );
A29:
for
D being
object st
D in L holds
ex
w being
object st
(
w in the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) &
S2[
D,
w] )
proof
let D be
object ;
( D in L implies ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S2[D,w] ) )
assume A30:
D in L
;
ex w being object st
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S2[D,w] )
then reconsider D0 =
D as
Subset of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
consider w being
Element of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that A31:
D0 = Ball (
w,
(e / 3))
by A28, A30;
take
w
;
( w in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) & S2[D,w] )
thus
(
w in the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) &
S2[
D,
w] )
by A31;
verum
end;
consider U being
Function of
L, the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that A32:
for
D being
object st
D in L holds
S2[
D,
U . D]
from FUNCT_2:sch 1(A29);
A33:
for
D being
object st
D in L holds
D = Ball (
(U /. D),
(e / 3))
defpred S3[
Element of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H),
Real]
means ex
f being
Function of the
carrier of
S, the
carrier of
T st
( $1
= f &
0 < $2 & ( for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< $2 holds
||.((f /. x1) - (f /. x2)).|| < e / 3 ) );
A36:
for
x0 being
Element of the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ex
d being
Element of
REAL st
S3[
x0,
d]
proof
let x0 be
Element of the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H);
ex d being Element of REAL st S3[x0,d]
x0 in H
by A3;
then
x0 in R_NormSpace_of_ContinuousFunctions (
S,
T)
;
then A37:
ex
f being
Function of the
carrier of
S, the
carrier of
T st
(
x0 = f &
f is
continuous )
;
then reconsider f =
x0 as
Function of the
carrier of
S, the
carrier of
T ;
consider d being
Real such that A38:
(
0 < d & ( for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< d holds
||.((f /. x1) - (f /. x2)).|| < e / 3 ) )
by A27, Th4, A1, A37;
reconsider d0 =
d as
Element of
REAL by XREAL_0:def 1;
take
d0
;
S3[x0,d0]
thus
S3[
x0,
d0]
by A38;
verum
end;
consider NF being
Function of the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H),
REAL such that A39:
for
f being
Element of the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) holds
S3[
f,
NF . f]
from FUNCT_2:sch 3(A36);
A40:
dom U = L
by FUNCT_2:def 1;
reconsider NFU =
NF .: (rng U) as
finite Subset of
REAL by A28;
consider xx being
object such that A41:
xx in L
by XBOOLE_0:def 1, A28, ZFMISC_1:2;
rng U <> {}
by A40, A41, FUNCT_1:3;
then consider xx being
object such that A42:
xx in rng U
by XBOOLE_0:def 1;
reconsider xx =
xx as
Point of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A42;
A43:
(
NFU is
bounded_below &
lower_bound NFU in NFU )
by SEQ_4:133, A42;
set d =
lower_bound NFU;
consider xx being
object such that A44:
(
xx in dom NF &
xx in rng U &
lower_bound NFU = NF . xx )
by FUNCT_1:def 6, A43;
reconsider xx =
xx as
Point of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A44;
A45:
ex
f being
Function of the
carrier of
S, the
carrier of
T st
(
xx = f &
0 < NF . xx & ( for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< NF . xx holds
||.((f /. x1) - (f /. x2)).|| < e / 3 ) )
by A39;
take
lower_bound NFU
;
( 0 < lower_bound NFU & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f . x1) - (f . x2)).|| < e ) )
thus
0 < lower_bound NFU
by A45, A44;
for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f . x1) - (f . x2)).|| < e
thus
for
f being
Function of the
carrier of
M, the
carrier of
T st
f in G holds
for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< lower_bound NFU holds
||.((f . x1) - (f . x2)).|| < e
verumproof
let f0 be
Function of the
carrier of
M, the
carrier of
T;
( f0 in G implies for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f0 . x1) - (f0 . x2)).|| < e )
assume
f0 in G
;
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
||.((f0 . x1) - (f0 . x2)).|| < e
then consider C being
set such that A46:
(
f0 in C &
C in L )
by A28, TARSKI:def 4, A3, A2;
reconsider f =
f0 as
Function of the
carrier of
S, the
carrier of
T by A1;
reconsider C =
C as
Subset of the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A46;
reconsider pf =
f0 as
Element of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A46;
A47:
pf in H
by A3;
reconsider pg =
U /. C as
Element of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
A48:
C = Ball (
pg,
(e / 3))
by A33, A46;
A49:
pg in H
by A3;
then
pg in ContinuousFunctions (
S,
T)
;
then
ex
f being
Function of the
carrier of
S, the
carrier of
T st
(
pg = f &
f is
continuous )
;
then reconsider g =
pg as
Function of
S,
T ;
pf in { y where y is Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) : dist (pg,y) < e / 3 }
by METRIC_1:def 14, A46, A48;
then A50:
ex
y being
Point of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
(
pf = y &
dist (
pg,
y)
< e / 3 )
;
reconsider ppf =
pf,
ppg =
pg as
Element of
(MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) by A47, A49;
A51:
dist (
ppg,
ppf)
< e / 3
by A50, TOPMETR:def 1;
reconsider pppf =
ppf,
pppg =
ppg as
Point of
(R_NormSpace_of_ContinuousFunctions (S,T)) ;
A52:
||.(pppg - pppf).|| < e / 3
by A51, NORMSP_2:def 1;
A53:
C in dom U
by FUNCT_2:def 1, A46;
U . C in rng U
by FUNCT_1:3, A40, A46;
then
pg in rng U
by A53, PARTFUN1:def 6;
then A54:
NF . pppg in NF .: (rng U)
by FUNCT_2:35;
let x1,
x2 be
Element of
M;
( dist (x1,x2) < lower_bound NFU implies ||.((f0 . x1) - (f0 . x2)).|| < e )
reconsider x10 =
x1,
x20 =
x2 as
Point of
S by A1;
assume A55:
dist (
x1,
x2)
< lower_bound NFU
;
||.((f0 . x1) - (f0 . x2)).|| < e
lower_bound NFU <= NF . pg
by A54, SEQ_4:def 2;
then A56:
dist (
x1,
x2)
< NF . pg
by A55, XXREAL_0:2;
ex
f being
Function of the
carrier of
S, the
carrier of
T st
(
pg = f &
0 < NF . pg & ( for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< NF . pg holds
||.((f /. x1) - (f /. x2)).|| < e / 3 ) )
by A39;
then A57:
||.((g /. x1) - (g /. x2)).|| < e / 3
by A56;
pppg - pppf in ContinuousFunctions (
S,
T)
;
then
ex
f being
Function of the
carrier of
S, the
carrier of
T st
(
pppg - pppf = f &
f is
continuous )
;
then reconsider gf =
pppg - pppf as
Function of
S,
T ;
pppf - pppg in ContinuousFunctions (
S,
T)
;
then
ex
f being
Function of the
carrier of
S, the
carrier of
T st
(
pppf - pppg = f &
f is
continuous )
;
then reconsider fg =
pppf - pppg as
Function of
S,
T ;
||.(gf . x20).|| <= ||.(pppg - pppf).||
by C0SP3:37;
then A59:
||.((g . x20) - (f . x20)).|| <= ||.(pppg - pppf).||
by C0SP3:48;
(
f /. x20 = f . x20 &
g /. x20 = g . x20 )
;
then A60:
||.((g /. x2) - (f /. x2)).|| < e / 3
by A59, XXREAL_0:2, A52;
||.(fg . x10).|| <= ||.(pppf - pppg).||
by C0SP3:37;
then
||.((f . x10) - (g . x10)).|| <= ||.(pppf - pppg).||
by C0SP3:48;
then A62:
||.((f . x10) - (g . x10)).|| <= ||.(pppg - pppf).||
by NORMSP_1:7;
(
f /. x10 = f . x10 &
g /. x10 = g . x10 )
;
then A63:
||.((f /. x1) - (g /. x1)).|| < e / 3
by A62, XXREAL_0:2, A52;
(f /. x1) - (f /. x2) =
(((f /. x1) - (g /. x1)) + (g /. x1)) - (f /. x2)
by RLVECT_4:1
.=
((f /. x1) - (g /. x1)) + ((g /. x1) - (f /. x2))
by RLVECT_1:28
.=
((f /. x1) - (g /. x1)) + ((((g /. x1) - (g /. x2)) + (g /. x2)) - (f /. x2))
by RLVECT_4:1
.=
((f /. x1) - (g /. x1)) + (((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2)))
by RLVECT_1:28
;
then A64:
||.((f /. x1) - (f /. x2)).|| <= ||.((f /. x1) - (g /. x1)).|| + ||.(((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))).||
by NORMSP_1:def 1;
A65:
||.(((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))).|| <= ||.((g /. x1) - (g /. x2)).|| + ||.((g /. x2) - (f /. x2)).||
by NORMSP_1:def 1;
||.((g /. x1) - (g /. x2)).|| + ||.((g /. x2) - (f /. x2)).|| < (e / 3) + (e / 3)
by A57, A60, XREAL_1:8;
then
||.(((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))).|| < (e / 3) + (e / 3)
by XXREAL_0:2, A65;
then A66:
||.((f /. x1) - (g /. x1)).|| + ||.(((g /. x1) - (g /. x2)) + ((g /. x2) - (f /. x2))).|| < (e / 3) + ((e / 3) + (e / 3))
by A63, XREAL_1:8;
(
f /. x10 = f . x10 &
f /. x20 = f . x20 )
;
hence
||.((f0 . x1) - (f0 . x2)).|| < e
by A66, A64, XXREAL_0:2;
verum
end;
end;
hence
G is equicontinuous
; verum