:: Inferior Limit and Superior Limit of Sequences of Real Numbers
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 29, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

Lm1:  for r1, r2, s being real number st 0 < s &amp; r1 <= r2 holds
( r1 < r2 + s &amp; r1 - s < r2 )
proofend;

theorem Th1: :: RINFSUP1:1
for s, r, t being real number holds
( ( s - r < t &amp; s + r > t ) iff abs (t - s) < r )
proofend;

definition
let seq be Real_Sequence;
func upper_bound seq ->  Real equals :: RINFSUP1:def 1
 upper_bound (rng seq);
coherence
 upper_bound (rng seq) is Real ;
end;

:: deftheorem  defines upper_bound RINFSUP1:def_1_:_
 for seq being Real_Sequence holds upper_bound seq = upper_bound (rng seq);

definition
let seq be Real_Sequence;
func lower_bound seq ->  Real equals :: RINFSUP1:def 2
 lower_bound (rng seq);
coherence
 lower_bound (rng seq) is Real ;
end;

:: deftheorem  defines lower_bound RINFSUP1:def_2_:_
 for seq being Real_Sequence holds lower_bound seq = lower_bound (rng seq);

theorem Th2: :: RINFSUP1:2
for seq1, seq2 being Real_Sequence holds (seq1 + seq2) - seq2 = seq1
proofend;

theorem Th3: :: RINFSUP1:3
for r being real number
for seq being Real_Sequence holds
( r in rng seq iff - r in rng (- seq) )
proofend;

theorem Th4: :: RINFSUP1:4
for seq being Real_Sequence holds rng (- seq) = -- (rng seq)
proofend;

theorem Th5: :: RINFSUP1:5
for seq being Real_Sequence holds
( seq is V88() iff rng seq is bounded_above )
proofend;

theorem Th6: :: RINFSUP1:6
for seq being Real_Sequence holds
( seq is V89() iff rng seq is bounded_below )
proofend;

theorem Th7: :: RINFSUP1:7
for r being real number
for seq being Real_Sequence st seq is V88() holds
( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) &amp; ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) )
proofend;

theorem Th8: :: RINFSUP1:8
for r being real number
for seq being Real_Sequence st seq is V89() holds
( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) &amp; ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) )
proofend;

theorem Th9: :: RINFSUP1:9
for r being real number
for seq being Real_Sequence holds
( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() &amp; upper_bound seq <= r ) )
proofend;

theorem Th10: :: RINFSUP1:10
for r being real number
for seq being Real_Sequence holds
( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() &amp; r <= lower_bound seq ) )
proofend;

theorem :: RINFSUP1:11
for seq being Real_Sequence holds
( seq is V88() iff - seq is V89() )
proofend;

theorem :: RINFSUP1:12
for seq being Real_Sequence holds
( seq is V89() iff - seq is V88() )
proofend;

theorem Th13: :: RINFSUP1:13
for seq being Real_Sequence st seq is V88() holds
upper_bound seq = - (lower_bound (- seq))
proofend;

theorem Th14: :: RINFSUP1:14
for seq being Real_Sequence st seq is V89() holds
lower_bound seq = - (upper_bound (- seq))
proofend;

theorem Th15: :: RINFSUP1:15
for seq1, seq2 being Real_Sequence st seq1 is V89() &amp; seq2 is V89() holds
lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2)
proofend;

theorem Th16: :: RINFSUP1:16
for seq1, seq2 being Real_Sequence st seq1 is V88() &amp; seq2 is V88() holds
upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)
proofend;

notation
let f be Real_Sequence;
synonym  nonnegative f for  nonnegative-yielding ;
end;

definition
let f be Real_Sequence;
redefine attr f is nonnegative-yielding  means :Def3: :: RINFSUP1:def 3
 for n being Element of NAT holds f . n >= 0 ;
compatibility
 ( f is nonnegative iff for n being Element of NAT holds f . n >= 0 )
proofend;
end;

:: deftheorem Def3 defines nonnegative RINFSUP1:def_3_:_
 for f being Real_Sequence holds
( f is nonnegative iff for n being Element of NAT holds f . n >= 0 );

theorem Th17: :: RINFSUP1:17
for k being Element of NAT
for seq being Real_Sequence st seq is nonnegative holds
seq ^\ k is nonnegative
proofend;

theorem Th18: :: RINFSUP1:18
for seq being Real_Sequence st seq is V89() &amp; seq is nonnegative holds
lower_bound seq >= 0
proofend;

theorem :: RINFSUP1:19
for seq being Real_Sequence st seq is V88() &amp; seq is nonnegative holds
upper_bound seq >= 0
proofend;

theorem Th20: :: RINFSUP1:20
for seq1, seq2 being Real_Sequence st seq1 is V89() &amp; seq1 is nonnegative &amp; seq2 is V89() &amp; seq2 is nonnegative holds
( seq1 (#) seq2 is V89() &amp; lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) )
proofend;

theorem Th21: :: RINFSUP1:21
for seq1, seq2 being Real_Sequence st seq1 is V88() &amp; seq1 is nonnegative &amp; seq2 is V88() &amp; seq2 is nonnegative holds
( seq1 (#) seq2 is V88() &amp; upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) )
proofend;

theorem :: RINFSUP1:22
for seq being Real_Sequence st seq is V48() &amp; seq is V88() holds
seq is bounded ;

theorem :: RINFSUP1:23
for seq being Real_Sequence st seq is V49() &amp; seq is V89() holds
seq is bounded ;

theorem Th24: :: RINFSUP1:24
for seq being Real_Sequence st seq is V48() &amp; seq is V88() holds
lim seq = upper_bound seq
proofend;

theorem Th25: :: RINFSUP1:25
for seq being Real_Sequence st seq is V49() &amp; seq is V89() holds
lim seq = lower_bound seq
proofend;

theorem :: RINFSUP1:26
for k being Element of NAT
for seq being Real_Sequence st seq is V88() holds
seq ^\ k is V88() by SEQM_3:27;

theorem :: RINFSUP1:27
for k being Element of NAT
for seq being Real_Sequence st seq is V89() holds
seq ^\ k is V89() by SEQM_3:28;

theorem :: RINFSUP1:28
for k being Element of NAT
for seq being Real_Sequence st seq is bounded holds
seq ^\ k is bounded by SEQM_3:29;

theorem Th29: :: RINFSUP1:29
for seq being Real_Sequence
for n being Element of NAT holds  {  (seq . k) where k is Element of NAT : n <= k  }  is Subset of REAL
proofend;

theorem Th30: :: RINFSUP1:30
for k being Element of NAT
for seq being Real_Sequence holds rng (seq ^\ k) =  {  (seq . n) where n is Element of NAT : k <= n  }
proofend;

theorem Th31: :: RINFSUP1:31
for seq being Real_Sequence st seq is V88() holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_above
proofend;

theorem Th32: :: RINFSUP1:32
for seq being Real_Sequence st seq is V89() holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_below
proofend;

theorem Th33: :: RINFSUP1:33
for seq being Real_Sequence st seq is bounded holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is real-bounded
proofend;

theorem Th34: :: RINFSUP1:34
for seq being Real_Sequence st seq is V48() holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
lower_bound R = seq . n
proofend;

theorem Th35: :: RINFSUP1:35
for seq being Real_Sequence st seq is V49() holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
upper_bound R = seq . n
proofend;

definition
let seq be Real_Sequence;
func inferior_realsequence seq ->  Real_Sequence means :Def4: :: RINFSUP1:def 4
 for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
it . n = lower_bound Y;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = lower_bound Y
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = lower_bound Y ) &amp; ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b2 . n = lower_bound Y ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def_4_:_
 for seq, b2 being Real_Sequence holds
( b2 = inferior_realsequence seq iff for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b2 . n = lower_bound Y );

definition
let seq be Real_Sequence;
func superior_realsequence seq ->  Real_Sequence means :Def5: :: RINFSUP1:def 5
 for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
it . n = upper_bound Y;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = upper_bound Y
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = upper_bound Y ) &amp; ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b2 . n = upper_bound Y ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines superior_realsequence RINFSUP1:def_5_:_
 for seq, b2 being Real_Sequence holds
( b2 = superior_realsequence seq iff for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b2 . n = upper_bound Y );

theorem Th36: :: RINFSUP1:36
for n being Element of NAT
for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n)
proofend;

theorem Th37: :: RINFSUP1:37
for n being Element of NAT
for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n)
proofend;

theorem Th38: :: RINFSUP1:38
for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . 0 = lower_bound seq
proofend;

theorem Th39: :: RINFSUP1:39
for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . 0 = upper_bound seq
proofend;

theorem Th40: :: RINFSUP1:40
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V89() holds
( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) &amp; ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) )
proofend;

theorem Th41: :: RINFSUP1:41
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V88() holds
( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) &amp; ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) )
proofend;

theorem Th42: :: RINFSUP1:42
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V89() holds
( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
proofend;

theorem Th43: :: RINFSUP1:43
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V89() holds
( ( for m being Element of NAT st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )
proofend;

theorem Th44: :: RINFSUP1:44
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V88() holds
( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )
proofend;

theorem Th45: :: RINFSUP1:45
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V88() holds
( ( for m being Element of NAT st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )
proofend;

theorem Th46: :: RINFSUP1:46
for n being Element of NAT
for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
proofend;

theorem Th47: :: RINFSUP1:47
for n being Element of NAT
for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))
proofend;

theorem Th48: :: RINFSUP1:48
for n being Element of NAT
for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)
proofend;

theorem Th49: :: RINFSUP1:49
for n being Element of NAT
for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n
proofend;

theorem Th50: :: RINFSUP1:50
for seq being Real_Sequence st seq is V89() holds
inferior_realsequence seq is V48()
proofend;

theorem Th51: :: RINFSUP1:51
for seq being Real_Sequence st seq is V88() holds
superior_realsequence seq is V49()
proofend;

theorem :: RINFSUP1:52
for n being Element of NAT
for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= (superior_realsequence seq) . n
proofend;

theorem Th53: :: RINFSUP1:53
for n being Element of NAT
for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq)
proofend;

theorem Th54: :: RINFSUP1:54
for n being Element of NAT
for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n
proofend;

theorem Th55: :: RINFSUP1:55
for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)
proofend;

theorem Th56: :: RINFSUP1:56
for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is bounded &amp; inferior_realsequence seq is bounded )
proofend;

theorem Th57: :: RINFSUP1:57
for seq being Real_Sequence st seq is bounded holds
( inferior_realsequence seq is convergent &amp; lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) )
proofend;

theorem Th58: :: RINFSUP1:58
for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is convergent &amp; lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) )
proofend;

theorem Th59: :: RINFSUP1:59
for n being Element of NAT
for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)
proofend;

theorem Th60: :: RINFSUP1:60
for n being Element of NAT
for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)
proofend;

theorem Th61: :: RINFSUP1:61
for seq being Real_Sequence st seq is V89() holds
inferior_realsequence seq = - (superior_realsequence (- seq))
proofend;

theorem Th62: :: RINFSUP1:62
for seq being Real_Sequence st seq is V88() holds
superior_realsequence seq = - (inferior_realsequence (- seq))
proofend;

theorem :: RINFSUP1:63
for n being Element of NAT
for seq being Real_Sequence st seq is V48() holds
seq . n <= (inferior_realsequence seq) . (n + 1)
proofend;

Lm2:  for n being Element of NAT
for seq being Real_Sequence st seq is V48() holds
(inferior_realsequence seq) . n = seq . n
proofend;

theorem :: RINFSUP1:64
for seq being Real_Sequence st seq is V48() holds
inferior_realsequence seq = seq
proofend;

theorem Th65: :: RINFSUP1:65
for n being Element of NAT
for seq being Real_Sequence st seq is V48() &amp; seq is V88() holds
seq . n <= (superior_realsequence seq) . (n + 1)
proofend;

theorem Th66: :: RINFSUP1:66
for n being Element of NAT
for seq being Real_Sequence st seq is V48() &amp; seq is V88() holds
(superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)
proofend;

theorem Th67: :: RINFSUP1:67
for n being Element of NAT
for seq being Real_Sequence st seq is V48() &amp; seq is V88() holds
( (superior_realsequence seq) . n = upper_bound seq &amp; superior_realsequence seq is constant )
proofend;

theorem :: RINFSUP1:68
for seq being Real_Sequence st seq is V48() &amp; seq is V88() holds
lower_bound (superior_realsequence seq) = upper_bound seq
proofend;

theorem :: RINFSUP1:69
for n being Element of NAT
for seq being Real_Sequence st seq is V49() holds
(superior_realsequence seq) . (n + 1) <= seq . n
proofend;

Lm3:  for n being Element of NAT
for seq being Real_Sequence st seq is V49() holds
(superior_realsequence seq) . n = seq . n
proofend;

theorem :: RINFSUP1:70
for seq being Real_Sequence st seq is V49() holds
superior_realsequence seq = seq
proofend;

theorem Th71: :: RINFSUP1:71
for n being Element of NAT
for seq being Real_Sequence st seq is V49() &amp; seq is V89() holds
(inferior_realsequence seq) . (n + 1) <= seq . n
proofend;

theorem Th72: :: RINFSUP1:72
for n being Element of NAT
for seq being Real_Sequence st seq is V49() &amp; seq is V89() holds
(inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)
proofend;

theorem Th73: :: RINFSUP1:73
for n being Element of NAT
for seq being Real_Sequence st seq is V49() &amp; seq is V89() holds
( (inferior_realsequence seq) . n = lower_bound seq &amp; inferior_realsequence seq is constant )
proofend;

theorem :: RINFSUP1:74
for seq being Real_Sequence st seq is V49() &amp; seq is V89() holds
upper_bound (inferior_realsequence seq) = lower_bound seq
proofend;

theorem Th75: :: RINFSUP1:75
for seq1, seq2 being Real_Sequence st seq1 is bounded &amp; seq2 is bounded &amp; ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds
( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) &amp; ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) )
proofend;

theorem :: RINFSUP1:76
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V89() &amp; seq2 is V89() holds
(inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)
proofend;

theorem :: RINFSUP1:77
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V88() &amp; seq2 is V88() holds
(superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)
proofend;

theorem :: RINFSUP1:78
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V89() &amp; seq1 is nonnegative &amp; seq2 is V89() &amp; seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
proofend;

theorem Th79: :: RINFSUP1:79
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V89() &amp; seq1 is nonnegative &amp; seq2 is V89() &amp; seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
proofend;

theorem Th80: :: RINFSUP1:80
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V88() &amp; seq1 is nonnegative &amp; seq2 is V88() &amp; seq2 is nonnegative holds
(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)
proofend;

definition
let seq be Real_Sequence;
func lim_sup seq ->  Element of REAL  equals :: RINFSUP1:def 6
 lower_bound (superior_realsequence seq);
coherence
 lower_bound (superior_realsequence seq) is Element of REAL ;
end;

:: deftheorem  defines lim_sup RINFSUP1:def_6_:_
 for seq being Real_Sequence holds lim_sup seq = lower_bound (superior_realsequence seq);

definition
let seq be Real_Sequence;
func lim_inf seq ->  Element of REAL  equals :: RINFSUP1:def 7
 upper_bound (inferior_realsequence seq);
coherence
 upper_bound (inferior_realsequence seq) is Element of REAL ;
end;

:: deftheorem  defines lim_inf RINFSUP1:def_7_:_
 for seq being Real_Sequence holds lim_inf seq = upper_bound (inferior_realsequence seq);

theorem Th81: :: RINFSUP1:81
for r being real number
for seq being Real_Sequence st seq is bounded holds
( lim_inf seq <= r 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 )
proofend;

theorem Th82: :: RINFSUP1:82
for r being real number
for seq being Real_Sequence st seq is bounded holds
( r <= lim_inf seq iff 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) )
proofend;

theorem :: RINFSUP1:83
for r being real number
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 ) &amp; ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) )
proofend;

theorem Th84: :: RINFSUP1:84
for r being real number
for seq being Real_Sequence st seq is bounded holds
( r <= lim_sup 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 )
proofend;

theorem Th85: :: RINFSUP1:85
for r being real number
for seq being Real_Sequence st seq is bounded holds
( lim_sup seq <= r iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s )
proofend;

theorem :: RINFSUP1:86
for r being real number
for seq being Real_Sequence st seq is bounded holds
( r = lim_sup 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 ) &amp; ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) )
proofend;

theorem :: RINFSUP1:87
for seq being Real_Sequence st seq is bounded holds
lim_inf seq <= lim_sup seq by Th55;

theorem Th88: :: RINFSUP1:88
for seq being Real_Sequence holds
( ( seq is bounded &amp; lim_sup seq = lim_inf seq ) iff seq is convergent )
proofend;

theorem :: RINFSUP1:89
for seq being Real_Sequence st seq is convergent holds
( lim seq = lim_sup seq &amp; lim seq = lim_inf seq )
proofend;

theorem Th90: :: RINFSUP1:90
for seq being Real_Sequence st seq is bounded holds
( lim_sup (- seq) = - (lim_inf seq) &amp; lim_inf (- seq) = - (lim_sup seq) )
proofend;

theorem :: RINFSUP1:91
for seq1, seq2 being Real_Sequence st seq1 is bounded &amp; seq2 is bounded &amp; ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds
( lim_sup seq1 <= lim_sup seq2 &amp; lim_inf seq1 <= lim_inf seq2 )
proofend;

theorem :: RINFSUP1:92
for seq1, seq2 being Real_Sequence st seq1 is bounded &amp; seq2 is bounded holds
( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) &amp; lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) &amp; lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) &amp; (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) &amp; (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) &amp; lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) &amp; ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) &amp; lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) )
proofend;

theorem :: RINFSUP1:93
for seq1, seq2 being Real_Sequence st seq1 is bounded &amp; seq1 is nonnegative &amp; seq2 is bounded &amp; seq2 is nonnegative holds
( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) &amp; lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )
proofend;