let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded holds
( r = lim_inf seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) )
let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( r = lim_inf seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ) )
assume A1: seq is bounded ; :: thesis: ( r = lim_inf seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) )
hence ( r = lim_inf seq implies for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ) by Th83, Th84; :: thesis: ( ( for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ) implies r = lim_inf seq )
assume A2: for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ; :: thesis: r = lim_inf seq
then for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ;
then A3: r <= lim_inf seq by A1, Th84;
for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s by A2;
then lim_inf seq <= r by A1, Th83;
hence r = lim_inf seq by A3, XXREAL_0:1; :: thesis: verum