:: 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-2021 Association of Mizar Users

Lm1: for r1, r2, s being Real st 0 < s & r1 <= r2 holds
( r1 < r2 + s & r1 - s < r2 )

proof end;

theorem Th1: :: RINFSUP1:1

for r, s, t being Real holds
( ( s - r < t & s + r > t ) iff |.(t - s).| < r )

proof end;

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

proof end;

theorem Th3: :: RINFSUP1:3

for r being Real
for seq being Real_Sequence holds
( r in rng seq iff - r in rng (- seq) )

proof end;

theorem Th4: :: RINFSUP1:4

for seq being Real_Sequence holds rng (- seq) = -- (rng seq)

proof end;

theorem Th5: :: RINFSUP1:5

for seq being Real_Sequence holds
( seq is V95() iff rng seq is bounded_above )

proof end;

theorem Th6: :: RINFSUP1:6

for seq being Real_Sequence holds
( seq is V96() iff rng seq is bounded_below )

proof end;

theorem Th7: :: RINFSUP1:7

for r being Real
for seq being Real_Sequence st seq is V95() holds
( r = upper_bound seq iff ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) )

proof end;

theorem Th8: :: RINFSUP1:8

for r being Real
for seq being Real_Sequence st seq is V96() holds
( r = lower_bound seq iff ( ( for n being Nat holds r <= seq . n ) & ( for s being Real st 0 < s holds
ex k being Nat st seq . k < r + s ) ) )

proof end;

theorem Th9: :: RINFSUP1:9

for r being Real
for seq being Real_Sequence holds
( ( for n being Nat holds seq . n <= r ) iff ( seq is V95() & upper_bound seq <= r ) )

proof end;

theorem Th10: :: RINFSUP1:10

for r being Real
for seq being Real_Sequence holds
( ( for n being Nat holds r <= seq . n ) iff ( seq is V96() & r <= lower_bound seq ) )

proof end;

theorem :: RINFSUP1:11

for seq being Real_Sequence holds
( seq is V95() iff - seq is V96() )

proof end;

theorem :: RINFSUP1:12

for seq being Real_Sequence holds
( seq is V96() iff - seq is V95() )

proof end;

theorem Th13: :: RINFSUP1:13

for seq being Real_Sequence st seq is V95() holds
upper_bound seq = - (lower_bound (- seq))

proof end;

theorem Th14: :: RINFSUP1:14

for seq being Real_Sequence st seq is V96() holds
lower_bound seq = - (upper_bound (- seq))

proof end;

theorem Th15: :: RINFSUP1:15

for seq1, seq2 being Real_Sequence st seq1 is V96() & seq2 is V96() holds
lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2)

proof end;

theorem Th16: :: RINFSUP1:16

for seq1, seq2 being Real_Sequence st seq1 is V95() & seq2 is V95() holds
upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)

proof end;

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 :: RINFSUP1:def 3
for n being Nat holds f . n >= 0 ;

compatibility
( f is nonnegative iff for n being Nat holds f . n >= 0 )

proof end;

end;

:: deftheorem defines nonnegative RINFSUP1:def 3 :
for f being Real_Sequence holds
( f is nonnegative iff for n being Nat holds f . n >= 0 );

theorem Th17: :: RINFSUP1:17

for k being Nat
for seq being Real_Sequence st seq is nonnegative holds
seq ^\ k is nonnegative

proof end;

theorem Th18: :: RINFSUP1:18

for seq being Real_Sequence st seq is V96() & seq is nonnegative holds
lower_bound seq >= 0 by Th10;

theorem :: RINFSUP1:19

for seq being Real_Sequence st seq is V95() & seq is nonnegative holds
upper_bound seq >= 0

proof end;

theorem Th20: :: RINFSUP1:20

for seq1, seq2 being Real_Sequence st seq1 is V96() & seq1 is nonnegative & seq2 is V96() & seq2 is nonnegative holds
( seq1 (#) seq2 is V96() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) )

proof end;

theorem Th21: :: RINFSUP1:21

for seq1, seq2 being Real_Sequence st seq1 is V95() & seq1 is nonnegative & seq2 is V95() & seq2 is nonnegative holds
( seq1 (#) seq2 is V95() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) )

proof end;

theorem :: RINFSUP1:22

for seq being Real_Sequence st seq is V54() & seq is V95() holds
seq is bounded ;

theorem :: RINFSUP1:23

for seq being Real_Sequence st seq is V55() & seq is V96() holds
seq is bounded ;

theorem Th24: :: RINFSUP1:24

for seq being Real_Sequence st seq is V54() & seq is V95() holds
lim seq = upper_bound seq

proof end;

theorem Th25: :: RINFSUP1:25

for seq being Real_Sequence st seq is V55() & seq is V96() holds
lim seq = lower_bound seq

proof end;

theorem :: RINFSUP1:26

for k being Nat
for seq being Real_Sequence st seq is V95() holds
seq ^\ k is V95() by SEQM_3:27;

theorem :: RINFSUP1:27

for k being Nat
for seq being Real_Sequence st seq is V96() holds
seq ^\ k is V96() by SEQM_3:28;

theorem :: RINFSUP1:28

for k being 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 Nat holds { (seq . k) where k is Nat : n <= k } is Subset of REAL

proof end;

theorem Th30: :: RINFSUP1:30

for k being Nat
for seq being Real_Sequence holds rng (seq ^\ k) = { (seq . n) where n is Nat : k <= n }

proof end;

theorem Th31: :: RINFSUP1:31

for seq being Real_Sequence st seq is V95() holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_above

proof end;

theorem Th32: :: RINFSUP1:32

for seq being Real_Sequence st seq is V96() holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_below

proof end;

theorem Th33: :: RINFSUP1:33

for seq being Real_Sequence st seq is bounded holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is real-bounded by Th31, Th32;

theorem Th34: :: RINFSUP1:34

for seq being Real_Sequence st seq is V54() holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n

proof end;

theorem Th35: :: RINFSUP1:35

for seq being Real_Sequence st seq is V55() holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
upper_bound R = seq . n

proof end;

definition

let seq be Real_Sequence;

func inferior_realsequence seq -> Real_Sequence means :Def4: :: RINFSUP1:def 4
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
it . n = lower_bound Y;

existence
ex b₁ being Real_Sequence st
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₁ . n = lower_bound Y

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₁ . n = lower_bound Y ) & ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₂ . n = lower_bound Y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def 4 :
for seq, b₂ being Real_Sequence holds
( b₂ = inferior_realsequence seq iff for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₂ . n = lower_bound Y );

definition

let seq be Real_Sequence;

func superior_realsequence seq -> Real_Sequence means :Def5: :: RINFSUP1:def 5
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
it . n = upper_bound Y;

existence
ex b₁ being Real_Sequence st
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₁ . n = upper_bound Y

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₁ . n = upper_bound Y ) & ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₂ . n = upper_bound Y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines superior_realsequence RINFSUP1:def 5 :
for seq, b₂ being Real_Sequence holds
( b₂ = superior_realsequence seq iff for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₂ . n = upper_bound Y );

theorem Th36: :: RINFSUP1:36

for n being Nat
for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n)

proof end;

theorem Th37: :: RINFSUP1:37

for n being Nat
for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n)

proof end;

theorem Th38: :: RINFSUP1:38

for seq being Real_Sequence st seq is V96() holds
(inferior_realsequence seq) . 0 = lower_bound seq

proof end;

theorem Th39: :: RINFSUP1:39

for seq being Real_Sequence st seq is V95() holds
(superior_realsequence seq) . 0 = upper_bound seq

proof end;

theorem Th40: :: RINFSUP1:40

for n being Nat
for r being Real
for seq being Real_Sequence st seq is V96() holds
( r = (inferior_realsequence seq) . n iff ( ( for k being Nat holds r <= seq . (n + k) ) & ( for s being Real st 0 < s holds
ex k being Nat st seq . (n + k) < r + s ) ) )

proof end;

theorem Th41: :: RINFSUP1:41

for n being Nat
for r being Real
for seq being Real_Sequence st seq is V95() holds
( r = (superior_realsequence seq) . n iff ( ( for k being Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ) ) )

proof end;

theorem Th42: :: RINFSUP1:42

for n being Nat
for r being Real
for seq being Real_Sequence st seq is V96() holds
( ( for k being Nat holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )

proof end;

theorem Th43: :: RINFSUP1:43

for n being Nat
for r being Real
for seq being Real_Sequence st seq is V96() holds
( ( for m being Nat st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )

proof end;

theorem Th44: :: RINFSUP1:44

for n being Nat
for r being Real
for seq being Real_Sequence st seq is V95() holds
( ( for k being Nat holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )

proof end;

theorem Th45: :: RINFSUP1:45

for n being Nat
for r being Real
for seq being Real_Sequence st seq is V95() holds
( ( for m being Nat st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )

proof end;

theorem Th46: :: RINFSUP1:46

for n being Nat
for seq being Real_Sequence st seq is V96() holds
(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))

proof end;

theorem Th47: :: RINFSUP1:47

for n being Nat
for seq being Real_Sequence st seq is V95() holds
(superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))

proof end;

theorem Th48: :: RINFSUP1:48

for n being Nat
for seq being Real_Sequence st seq is V96() holds
(inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)

proof end;

theorem Th49: :: RINFSUP1:49

for n being Nat
for seq being Real_Sequence st seq is V95() holds
(superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n

proof end;

theorem Th50: :: RINFSUP1:50

for seq being Real_Sequence st seq is V96() holds
inferior_realsequence seq is V54() by Th48;

theorem Th51: :: RINFSUP1:51

for seq being Real_Sequence st seq is V95() holds
superior_realsequence seq is V55() by Th49;

theorem :: RINFSUP1:52

for n being Nat
for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= (superior_realsequence seq) . n

proof end;

theorem Th53: :: RINFSUP1:53

for n being Nat
for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq)

proof end;

theorem Th54: :: RINFSUP1:54

for n being Nat
for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n

proof end;

theorem Th55: :: RINFSUP1:55

for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)

proof end;

theorem Th56: :: RINFSUP1:56

for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )

proof end;

theorem Th57: :: RINFSUP1:57

for seq being Real_Sequence st seq is bounded holds
( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) )

proof end;

theorem Th58: :: RINFSUP1:58

for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) )

proof end;

theorem Th59: :: RINFSUP1:59

for n being Nat
for seq being Real_Sequence st seq is V96() holds
(inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)

proof end;

theorem Th60: :: RINFSUP1:60

for n being Nat
for seq being Real_Sequence st seq is V95() holds
(superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)

proof end;

theorem Th61: :: RINFSUP1:61

for seq being Real_Sequence st seq is V96() holds
inferior_realsequence seq = - (superior_realsequence (- seq))

proof end;

theorem Th62: :: RINFSUP1:62

for seq being Real_Sequence st seq is V95() holds
superior_realsequence seq = - (inferior_realsequence (- seq))

proof end;

theorem :: RINFSUP1:63

for n being Nat
for seq being Real_Sequence st seq is V54() holds
seq . n <= (inferior_realsequence seq) . (n + 1)

proof end;

Lm2: for n being Nat
for seq being Real_Sequence st seq is V54() holds
(inferior_realsequence seq) . n = seq . n

proof end;

theorem :: RINFSUP1:64

for seq being Real_Sequence st seq is V54() holds
inferior_realsequence seq = seq

proof end;

theorem Th65: :: RINFSUP1:65

for n being Nat
for seq being Real_Sequence st seq is V54() & seq is V95() holds
seq . n <= (superior_realsequence seq) . (n + 1)

proof end;

theorem Th66: :: RINFSUP1:66

for n being Nat
for seq being Real_Sequence st seq is V54() & seq is V95() holds
(superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)

proof end;

theorem Th67: :: RINFSUP1:67

for n being Nat
for seq being Real_Sequence st seq is V54() & seq is V95() holds
( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )

proof end;

theorem :: RINFSUP1:68

for seq being Real_Sequence st seq is V54() & seq is V95() holds
lower_bound (superior_realsequence seq) = upper_bound seq

proof end;

theorem :: RINFSUP1:69

for n being Nat
for seq being Real_Sequence st seq is V55() holds
(superior_realsequence seq) . (n + 1) <= seq . n

proof end;

Lm3: for n being Nat
for seq being Real_Sequence st seq is V55() holds
(superior_realsequence seq) . n = seq . n

proof end;

theorem :: RINFSUP1:70

for seq being Real_Sequence st seq is V55() holds
superior_realsequence seq = seq

proof end;

theorem Th71: :: RINFSUP1:71

for n being Nat
for seq being Real_Sequence st seq is V55() & seq is V96() holds
(inferior_realsequence seq) . (n + 1) <= seq . n

proof end;

theorem Th72: :: RINFSUP1:72

for n being Nat
for seq being Real_Sequence st seq is V55() & seq is V96() holds
(inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)

proof end;

theorem Th73: :: RINFSUP1:73

for n being Nat
for seq being Real_Sequence st seq is V55() & seq is V96() holds
( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )

proof end;

theorem :: RINFSUP1:74

for seq being Real_Sequence st seq is V55() & seq is V96() holds
upper_bound (inferior_realsequence seq) = lower_bound seq

proof end;

theorem Th75: :: RINFSUP1:75

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( ( for n being Nat holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Nat holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) )

proof end;

theorem :: RINFSUP1:76

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq2 is V96() holds
(inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)

proof end;

theorem :: RINFSUP1:77

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V95() & seq2 is V95() holds
(superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)

proof end;

theorem :: RINFSUP1:78

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq1 is nonnegative & seq2 is V96() & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)

proof end;

theorem Th79: :: RINFSUP1:79

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq1 is nonnegative & seq2 is V96() & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)

proof end;

theorem Th80: :: RINFSUP1:80

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V95() & seq1 is nonnegative & seq2 is V95() & seq2 is nonnegative holds
(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)

proof end;

definition

let seq be Real_Sequence;

func lim_sup seq -> Real equals :: RINFSUP1:def 6
lower_bound (superior_realsequence seq);

coherence
lower_bound (superior_realsequence seq) is 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 -> Real equals :: RINFSUP1:def 7
upper_bound (inferior_realsequence seq);

coherence
upper_bound (inferior_realsequence seq) is 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
for seq being Real_Sequence st seq is bounded holds
( lim_inf seq <= r iff for s being Real st 0 < s holds
for n being Nat ex k being Nat st seq . (n + k) < r + s )

proof end;

theorem Th82: :: RINFSUP1:82

for r being Real
for seq being Real_Sequence st seq is bounded holds
( r <= lim_inf seq iff for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds r - s < seq . (n + k) )

proof end;

theorem :: RINFSUP1:83

for r being Real
for seq being Real_Sequence st seq is bounded holds
( r = lim_inf seq iff for s being Real st 0 < s holds
( ( for n being Nat ex k being Nat st seq . (n + k) < r + s ) & ex n being Nat st
for k being Nat holds r - s < seq . (n + k) ) )

proof end;

theorem Th84: :: RINFSUP1:84

for r being Real
for seq being Real_Sequence st seq is bounded holds
( r <= lim_sup seq iff for s being Real st 0 < s holds
for n being Nat ex k being Nat st seq . (n + k) > r - s )

proof end;

theorem Th85: :: RINFSUP1:85

for r being Real
for seq being Real_Sequence st seq is bounded holds
( lim_sup seq <= r iff for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s )

proof end;

theorem :: RINFSUP1:86

for r being Real
for seq being Real_Sequence st seq is bounded holds
( r = lim_sup seq iff for s being Real st 0 < s holds
( ( for n being Nat ex k being Nat st seq . (n + k) > r - s ) & ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ) )

proof end;

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 & lim_sup seq = lim_inf seq ) iff seq is convergent )

proof end;

theorem :: RINFSUP1:89

for seq being Real_Sequence st seq is convergent holds
( lim seq = lim_sup seq & lim seq = lim_inf seq )

proof end;

theorem Th90: :: RINFSUP1:90

for seq being Real_Sequence st seq is bounded holds
( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) )

proof end;

theorem :: RINFSUP1:91

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )

proof end;

theorem :: RINFSUP1:92

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) )

proof end;

theorem :: RINFSUP1:93

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds
( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )

proof end;