let M be non empty MetrSpace; :: thesis: for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for U being compact Subset of T
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F & ( for f being Function st f in F holds
rng f c= U ) holds
( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) )
let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for U being compact Subset of T
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F & ( for f being Function st f in F holds
rng f c= U ) holds
( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) )
let T be NormedLinearTopSpace; :: thesis: for U being compact Subset of T
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F & ( for f being Function st f in F holds
rng f c= U ) holds
( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) )
let U be compact Subset of T; :: thesis: for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F & ( for f being Function st f in F holds
rng f c= U ) holds
( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) )
let F be non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F & ( for f being Function st f in F holds
rng f c= U ) holds
( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) )
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); :: thesis: ( S = TopSpaceMetr M & T is complete & G = F & ( for f being Function st f in F holds
rng f c= U ) implies ( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) ) )
assume that
A1: S = TopSpaceMetr M and
A2: T is complete ; :: thesis: ( not G = F or ex f being Function st
( f in F & not rng f c= U ) or ( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) ) )
assume A3: ( G = F & ( for f being Function st f in F holds
rng f c= U ) ) ; :: thesis: ( ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) & ( G is equicontinuous implies Cl F is compact ) )
reconsider H = F as non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) ;
set Z = R_NormSpace_of_ContinuousFunctions (S,T);
( (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded iff Cl F is compact ) by A2, Th12;
hence ( Cl F is compact implies ( G is equibounded & G is equicontinuous ) ) by A2, A1, Th13, A3; :: thesis: ( G is equicontinuous implies Cl F is compact )
assume A5: G is equicontinuous ; :: thesis: Cl F is compact
for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact
proof
let x be Point of S; :: thesis: for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact
let Fx be non empty Subset of (MetricSpaceNorm T); :: thesis: ( Fx = { (f . x) where f is Function of S,T : f in F } implies (MetricSpaceNorm T) | (Cl Fx) is compact )
assume A6: Fx = { (f . x) where f is Function of S,T : f in F } ; :: thesis: (MetricSpaceNorm T) | (Cl Fx) is compact
reconsider V = U as Subset of (TopSpaceNorm T) ;
A7: V is compact by Th21;
A10: Fx c= V
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Fx or y in V )
assume y in Fx ; :: thesis: y in V
then consider f being Function of S,T such that
A8: ( y = f . x & f in F ) by A6;
A9: f . x in rng f by FUNCT_2:4;
rng f c= V by A3, A8;
hence y in V by A8, A9; :: thesis: verum
end;
consider Gx being Subset of (TopSpaceMetr (MetricSpaceNorm T)) such that
A11: ( Fx = Gx & Cl Fx = Cl Gx ) by Def1;
reconsider HClx = Cl Gx as non empty Subset of (MetricSpaceNorm T) by A11;
A12: TopSpaceNorm T is T_2 by PCOMPS_1:34;
Cl Gx c= Cl V by A10, A11, PRE_TOPC:19;
then Cl Gx c= V by A12, A7, PRE_TOPC:22;
then Cl Gx is compact by Th21, COMPTS_1:9;
then HClx is sequentially_compact by TOPMETR4:15;
hence (MetricSpaceNorm T) | (Cl Fx) is compact by A11, TOPMETR4:14; :: thesis: verum
end;
hence Cl F is compact by Th18, A1, A2, A3, A5; :: thesis: verum