let n be Element of NAT ; 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 Element of 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); for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st
( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S
let p be Point of (TOP-REAL n); ( ex s being Real_Sequence of n st
( s is convergent & ( for x being Element of 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 Element of NAT holds s . x in S . x
and
A3:
p = lim s
; p in Lim_inf S
for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r)
proof
let r be
real number ;
( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )
reconsider r9 =
r as
Real by XREAL_0:def 1;
assume
r > 0
;
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r)
then consider l being
Element of
NAT such that A4:
for
m being
Element of
NAT st
l <= m holds
|.((s . m) - p).| < r9
by A1, A3, TOPRNS_1:def 9;
take v =
max (
0,
l);
for m being Element of NAT st m > v holds
S . m meets Ball (p9,r)
let m be
Element of
NAT ;
( m > v implies S . m meets Ball (p9,r) )
assume
v < m
;
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 Th33;
s . m in S . m
by A2;
hence
S . m meets Ball (
p9,
r)
by A5, XBOOLE_0:3;
verum
end;
hence
p in Lim_inf S
by Th48; verum