let V be finite-dimensional RealNormSpace; :: thesis: for X being Subset of V st dim V <> 0 holds
( X is compact iff ( X is closed & ex r being Real st
for y being Point of V st y in X holds
||.y.|| < r ) )
let X be Subset of V; :: thesis: ( dim V <> 0 implies ( X is compact iff ( X is closed & ex r being Real st
for y being Point of V st y in X holds
||.y.|| < r ) ) )
assume A1: dim V <> 0 ; :: thesis: ( X is compact iff ( X is closed & ex r being Real st
for y being Point of V st y in X holds
||.y.|| < r ) )
thus ( X is compact implies ( X is closed & ex r being Real st
for y being Point of V st y in X holds
||.y.|| < r ) ) by Th6; :: thesis: ( X is closed & ex r being Real st
for y being Point of V st y in X holds
||.y.|| < r implies X is compact )
assume A2: ( X is closed & ex r being Real st
for x being Point of V st x in X holds
||.x.|| < r ) ; :: thesis: X is compact
then consider r being Real such that
A3: for x being Point of V st x in X holds
||.x.|| < r ;
consider S being LinearOperator of V,(REAL-NS (dim V)) such that
A4: ( S is one-to-one & S is onto & S is isometric-like ) by A1, Th28;
consider k1, k2 being Real such that
A5: ( 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(S . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(S . x).|| ) ) ) by A4;
A6: S .: X is closed by A2, A4, Th36;
reconsider r2 = (k1 * r) + 1 as Real ;
for y being Point of (REAL-NS (dim V)) st y in S .: X holds
||.y.|| < r2
proof
let y be Point of (REAL-NS (dim V)); :: thesis: ( y in S .: X implies ||.y.|| < r2 )
assume y in S .: X ; :: thesis: ||.y.|| < r2
then consider x being object such that
A7: ( x in dom S & x in X & y = S . x ) by FUNCT_1:def 6;
reconsider x = x as Point of V by A7;
A8: ||.(S . x).|| <= k1 * ||.x.|| by A5;
||.x.|| < r by A3, A7;
then k1 * ||.x.|| <= k1 * r by XREAL_1:64, A5;
then ||.(S . x).|| <= k1 * r by XXREAL_0:2, A8;
then ||.(S . x).|| + 0 < (k1 * r) + 1 by XREAL_1:8;
hence ||.y.|| < r2 by A7; :: thesis: verum
end;
then S .: X is compact by A6, Lm3;
hence X is compact by A4, Th38; :: thesis: verum