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
( ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded ) & 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
( ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded ) & 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
( ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded ) & 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
( ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded ) & 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
( ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded ) & 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 ( ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded ) & G is equicontinuous ) )
assume A2:
G = H
; ( not (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded or ( ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded ) & 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
; ( ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded ) & G is equicontinuous )
thus
for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded
G is equicontinuous proof
let x be
Point of
S;
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | Hx is totally_bounded let Hx be non
empty Subset of
(MetricSpaceNorm T);
( Hx = { (f . x) where f is Function of S,T : f in H } implies (MetricSpaceNorm T) | Hx is totally_bounded )
assume A5:
Hx = { (f . x) where f is Function of S,T : f in H }
;
(MetricSpaceNorm T) | Hx is totally_bounded
set MTHx =
(MetricSpaceNorm T) | Hx;
let e be
Real;
TBSP_1:def 1 ( e <= 0 or ex b1 being Element of bool (bool the carrier of ((MetricSpaceNorm T) | Hx)) st
( b1 is finite & the carrier of ((MetricSpaceNorm T) | Hx) = union b1 & ( for b2 being Element of bool the carrier of ((MetricSpaceNorm T) | Hx) holds
( not b2 in b1 or ex b3 being Element of the carrier of ((MetricSpaceNorm T) | Hx) st b2 = Ball (b3,e) ) ) ) )
assume
0 < e
;
ex b1 being Element of bool (bool the carrier of ((MetricSpaceNorm T) | Hx)) st
( b1 is finite & the carrier of ((MetricSpaceNorm T) | Hx) = union b1 & ( for b2 being Element of bool the carrier of ((MetricSpaceNorm T) | Hx) holds
( not b2 in b1 or ex b3 being Element of the carrier of ((MetricSpaceNorm T) | Hx) st b2 = Ball (b3,e) ) ) )
then consider L being
Subset-Family of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that A6:
(
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) ) )
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,
e) );
A7:
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 A8:
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 A9:
D0 = Ball (
w,
e)
by A6, A8;
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 A9;
verum
end;
consider U being
Function of
L, the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that A10:
for
D being
object st
D in L holds
S1[
D,
U . D]
from FUNCT_2:sch 1(A7);
A11:
for
D being
object st
D in L holds
D = Ball (
(U /. D),
e)
defpred S2[
object ,
object ]
means ex
w being
Function of
S,
T ex
p being
Point of
((MetricSpaceNorm T) | Hx) st
( $1
= w &
p = w . x & $2
= Ball (
p,
e) );
A14:
for
f being
object st
f in the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) holds
ex
B being
object st
(
B in bool the
carrier of
((MetricSpaceNorm T) | Hx) &
S2[
f,
B] )
proof
let f be
object ;
( f in the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) implies ex B being object st
( B in bool the carrier of ((MetricSpaceNorm T) | Hx) & S2[f,B] ) )
assume A15:
f in the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H)
;
ex B being object st
( B in bool the carrier of ((MetricSpaceNorm T) | Hx) & S2[f,B] )
then
f in R_NormSpace_of_ContinuousFunctions (
S,
T)
by A3;
then
ex
g being
Function of the
carrier of
S, the
carrier of
T st
(
f = g &
g is
continuous )
;
then reconsider g =
f as
Function of
S,
T ;
g . x in Hx
by A15, A5, A3;
then reconsider p =
g . x as
Point of
((MetricSpaceNorm T) | Hx) by TOPMETR:def 2;
take B =
Ball (
p,
e);
( B in bool the carrier of ((MetricSpaceNorm T) | Hx) & S2[f,B] )
thus
(
B in bool the
carrier of
((MetricSpaceNorm T) | Hx) &
S2[
f,
B] )
;
verum
end;
consider NF being
Function of the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H),
(bool the carrier of ((MetricSpaceNorm T) | Hx)) such that A16:
for
D being
object st
D in the
carrier of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) holds
S2[
D,
NF . D]
from FUNCT_2:sch 1(A14);
A17:
dom U = L
by FUNCT_2:def 1;
set Le =
NF .: (rng U);
reconsider Le =
NF .: (rng U) as
Subset-Family of
((MetricSpaceNorm T) | Hx) ;
take
Le
;
( Le is finite & the carrier of ((MetricSpaceNorm T) | Hx) = union Le & ( for b1 being Element of bool the carrier of ((MetricSpaceNorm T) | Hx) holds
( not b1 in Le or ex b2 being Element of the carrier of ((MetricSpaceNorm T) | Hx) st b1 = Ball (b2,e) ) ) )
thus
Le is
finite
by A6;
( the carrier of ((MetricSpaceNorm T) | Hx) = union Le & ( for b1 being Element of bool the carrier of ((MetricSpaceNorm T) | Hx) holds
( not b1 in Le or ex b2 being Element of the carrier of ((MetricSpaceNorm T) | Hx) st b1 = Ball (b2,e) ) ) )
for
t being
object holds
(
t in the
carrier of
((MetricSpaceNorm T) | Hx) iff
t in union Le )
proof
let t0 be
object ;
( t0 in the carrier of ((MetricSpaceNorm T) | Hx) iff t0 in union Le )
hereby ( t0 in union Le implies t0 in the carrier of ((MetricSpaceNorm T) | Hx) )
assume A18:
t0 in the
carrier of
((MetricSpaceNorm T) | Hx)
;
t0 in union Lethen A19:
t0 in Hx
by TOPMETR:def 2;
reconsider t =
t0 as
Point of
((MetricSpaceNorm T) | Hx) by A18;
consider f being
Function of
S,
T such that A20:
(
t = f . x &
f in H )
by A5, A19;
consider K being
set such that A21:
(
f in K &
K in L )
by TARSKI:def 4, A6, A3, A20;
U /. K = U . K
by PARTFUN1:def 6, A21, A17;
then A22:
U /. K in rng U
by FUNCT_1:def 3, A17, A21;
consider g being
Function of
S,
T,
p being
Point of
((MetricSpaceNorm T) | Hx) such that A23:
(
U /. K = g &
p = g . x &
NF . (U /. K) = Ball (
p,
e) )
by A16;
A24:
f in Ball (
(U /. K),
e)
by A21, A11;
reconsider f0 =
f as
Point of
((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A21;
A25:
dist (
f0,
(U /. K))
< e
by A24, METRIC_1:11;
reconsider f1 =
f0 as
Point of
(MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) by TOPMETR:def 1, TARSKI:def 3;
reconsider g1 =
U /. K as
Point of
(MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) by TOPMETR:def 1, TARSKI:def 3;
A26:
dist (
f1,
g1)
< e
by A25, TOPMETR:def 1;
reconsider f2 =
f1,
g2 =
g1 as
Point of
(R_NormSpace_of_ContinuousFunctions (S,T)) ;
A27:
||.(f2 - g2).|| < e
by NORMSP_2:def 1, A26;
g2 - f2 in ContinuousFunctions (
S,
T)
;
then
ex
f being
Function of the
carrier of
S, the
carrier of
T st
(
g2 - f2 = f &
f is
continuous )
;
then reconsider fg =
g2 - f2 as
Function of
S,
T ;
||.(fg . x).|| <= ||.(g2 - f2).||
by C0SP3:37;
then
||.(fg . x).|| <= ||.(f2 - g2).||
by NORMSP_1:7;
then
||.((g . x) - (f . x)).|| <= ||.(f2 - g2).||
by A23, C0SP3:48;
then A30:
||.((g /. x) - (f /. x)).|| < e
by A27, XXREAL_0:2;
A31:
NF . (U /. K) in Le
by A22, FUNCT_2:35;
reconsider tt =
t as
Point of
(MetricSpaceNorm T) by A20;
reconsider pp =
p as
Point of
(MetricSpaceNorm T) by TOPMETR:def 1, TARSKI:def 3;
reconsider p1 =
pp as
Point of
T ;
dist (
pp,
tt)
< e
by NORMSP_2:def 1, A23, A20, A30;
then
dist (
p,
t)
< e
by TOPMETR:def 1;
then
f . x in { y where y is Point of ((MetricSpaceNorm T) | Hx) : dist (p,y) < e }
by A20;
then
f . x in NF . (U /. K)
by A23, METRIC_1:def 14;
hence
t0 in union Le
by TARSKI:def 4, A31, A20;
verum
end;
assume
t0 in union Le
;
t0 in the carrier of ((MetricSpaceNorm T) | Hx)
hence
t0 in the
carrier of
((MetricSpaceNorm T) | Hx)
;
verum
end;
hence
the
carrier of
((MetricSpaceNorm T) | Hx) = union Le
by TARSKI:2;
for b1 being Element of bool the carrier of ((MetricSpaceNorm T) | Hx) holds
( not b1 in Le or ex b2 being Element of the carrier of ((MetricSpaceNorm T) | Hx) st b1 = Ball (b2,e) )
thus
for
C being
Subset of
((MetricSpaceNorm T) | Hx) st
C in Le holds
ex
p being
Element of
((MetricSpaceNorm T) | Hx) st
C = Ball (
p,
e)
verum
end;
thus
G is equicontinuous
by Th13, A1, A2, A4; verum