let n be Nat; :: thesis: for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st
( s is convergent & ( for x being Nat holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S
let S be SetSequence of the carrier of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st
( s is convergent & ( for x being Nat holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S
let p be Point of (TOP-REAL n); :: thesis: ( ex s being Real_Sequence of n st
( s is convergent & ( for x being Nat holds s . x in S . x ) & p = lim s ) implies p in Lim_inf S )
reconsider p9 = p as Point of (Euclid n) by TOPREAL3:8;
given s being Real_Sequence of n such that A1: s is convergent and
A2: for x being Nat holds s . x in S . x and
A3: p = lim s ; :: thesis: p in Lim_inf S
for r being Real st r > 0 holds
ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p9,r)

proof

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p9,r) )
reconsider r9 = r as Real ;
assume r > 0 ; :: thesis: ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p9,r)
then consider l being Nat such that
A4: for m being Nat st l <= m holds
|.((s . m) - p).| < r9 by A1, A3, TOPRNS_1:def 9;
reconsider v = max (0,l) as Nat by TARSKI:1;
take v ; :: thesis: for m being Nat st m > v holds
S . m meets Ball (p9,r)
let m be Nat; :: thesis: ( m > v implies S . m meets Ball (p9,r) )
assume v < m ; :: thesis: S . m meets Ball (p9,r)
then l <= m by XXREAL_0:30;
then |.((s . m) - p).| < r9 by A4;
then A5: s . m in Ball (p9,r) by Th3;
s . m in S . m by A2;
hence S . m meets Ball (p9,r) by A5, XBOOLE_0:3; :: thesis: verum

end;

hence p in Lim_inf S by Th14; :: thesis: verum