let T be NormedLinearTopSpace; :: thesis: ( T is compact iff TopSpaceNorm T is compact )
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;
A3: [#] T = [#] (TopSpaceMetr (MetricSpaceNorm T)) ;
hereby :: thesis: ( TopSpaceNorm T is compact implies T is compact )
assume T is compact ; :: thesis: TopSpaceNorm T is compact
then [#] T is compact Subset of (TopSpaceMetr (MetricSpaceNorm T)) by A2, COMPTS_1:23, COMPTS_1:1;
hence TopSpaceNorm T is compact by A3, COMPTS_1:1; :: thesis: verum
end;
assume TopSpaceNorm T is compact ; :: thesis: T is compact
then [#] T is compact Subset of (TopSpaceMetr (MetricSpaceNorm T)) by A3, COMPTS_1:1;
hence T is compact by A2, COMPTS_1:1, COMPTS_1:23; :: thesis: verum