let M be non empty MetrSpace; :: thesis: for S being non empty compact TopSpace
for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st G = F holds
( Cl F is compact iff ( G is equibounded & G is equicontinuous ) )
let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st G = F holds
( Cl F is compact iff ( G is equibounded & G is equicontinuous ) )
let T be NormedLinearTopSpace; :: thesis: ( S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 implies for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st G = F holds
( Cl F is compact iff ( G is equibounded & G is equicontinuous ) ) )
assume that
A1: S = TopSpaceMetr M and
A2: T is complete and
A3: ( T is finite-dimensional & dim T <> 0 ) ; :: thesis: for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st G = F holds
( Cl F is compact iff ( G is equibounded & G is equicontinuous ) )
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); :: thesis: for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st G = F holds
( Cl F is compact iff ( G is equibounded & G is equicontinuous ) )
let F be non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: ( G = F implies ( Cl F is compact iff ( G is equibounded & G is equicontinuous ) ) )
assume A4: G = F ; :: thesis: ( Cl F is compact iff ( G is equibounded & G is equicontinuous ) )
reconsider H = F as non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) ;
A5: Cl H = Cl F by ASCOLI:1;
( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) ) by Th27, A1, A2, A3, A4;
hence ( Cl F is compact iff ( G is equibounded & G is equicontinuous ) ) by TOPMETR4:18, A5; :: thesis: verum