let n be Nat; :: thesis: for X being Subset of (REAL-NS n) st X is closed & ex r being Real st
for y being Point of (REAL-NS n) st y in X holds
||.y.|| < r holds
X is compact
let X be Subset of (REAL-NS n); :: thesis: ( X is closed & ex r being Real st
for y being Point of (REAL-NS n) st y in X holds
||.y.|| < r implies X is compact )
assume that
A1: X is closed and
A2: ex r being Real st
for y being Point of (REAL-NS n) st y in X holds
||.y.|| < r ; :: thesis: X is compact
for s1 being sequence of (REAL-NS n) st rng s1 c= X holds
ex s2 being sequence of (REAL-NS n) st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X )
proof
let s1 be sequence of (REAL-NS n); :: thesis: ( rng s1 c= X implies ex s2 being sequence of (REAL-NS n) st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) )
assume A3: rng s1 c= X ; :: thesis: ex s2 being sequence of (REAL-NS n) st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X )
consider r being Real such that
A4: for y being Point of (REAL-NS n) st y in X holds
||.y.|| < r by A2;
for i being Nat holds ||.(s1 . i).|| < r
proof
let i be Nat; :: thesis: ||.(s1 . i).|| < r
i in NAT by ORDINAL1:def 12;
then i in dom s1 by FUNCT_2:def 1;
then s1 . i in rng s1 by FUNCT_1:3;
hence ||.(s1 . i).|| < r by A3, A4; :: thesis: verum
end;
then consider s2 being subsequence of s1 such that
A5: s2 is convergent by Th5;
take s2 ; :: thesis: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X )
ex N being increasing sequence of NAT st s2 = s1 * N by VALUED_0:def 17;
then rng s2 c= rng s1 by RELAT_1:26;
hence ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A5, A1, A3, XBOOLE_1:1; :: thesis: verum
end;
hence X is compact ; :: thesis: verum