let T be NormedLinearTopSpace; :: thesis: for X being set holds
( X is compact Subset of T iff X is compact Subset of (TopSpaceNorm T) )
let X be set ; :: thesis: ( X is compact Subset of T iff X is compact Subset of (TopSpaceNorm T) )
consider RNS being RealNormSpace such that
A1: ( RNS = NORMSTR(# the carrier of T, the ZeroF of T, the U5 of T, the U7 of T, the normF of T #) & the topology of T = the topology of (TopSpaceNorm RNS) ) by C0SP3:def 6;
A2: TopSpaceMetr (MetricSpaceNorm T) = TopStruct(# the carrier of T, the topology of T #) by A1, Th15;
hence ( X is compact Subset of T implies X is compact Subset of (TopSpaceNorm T) ) by COMPTS_1:23; :: thesis: ( X is compact Subset of (TopSpaceNorm T) implies X is compact Subset of T )
assume X is compact Subset of (TopSpaceNorm T) ; :: thesis: X is compact Subset of T
then reconsider X0 = X as compact Subset of (TopSpaceNorm T) ;
X0 is compact Subset of TopStruct(# the carrier of T, the topology of T #) by A2;
hence X is compact Subset of T by COMPTS_1:23; :: thesis: verum