:: RINFSUP1 semantic presentation

Lemma1: for b₁, b₂, b₃ being real number st 0 < b₃ & b₁ <= b₂ holds
( b₁ < b₂ + b₃ & b₁ - b₃ < b₂ )

proof end;

theorem Th1: :: RINFSUP1:1

for b₁, b₂, b₃ being real number holds
( ( b₁ - b₂ < b₃ & b₁ + b₂ > b₃ ) iff abs (b₃ - b₁) < b₂ )

proof end;

definition

let c₁ be Real_Sequence;
func sup c₁ -> Real equals :: RINFSUP1:def 1
sup (rng a₁);
coherence ;

end;

:: deftheorem Def1 defines sup RINFSUP1:def 1 :

definition

let c₁ be Real_Sequence;
func inf c₁ -> Real equals :: RINFSUP1:def 2
inf (rng a₁);
coherence ;

end;

:: deftheorem Def2 defines inf RINFSUP1:def 2 :

theorem Th2: :: RINFSUP1:2

for b₁, b₂ being Real_Sequence holds (b₁ + b₂) - b₂ = b₁

proof end;

theorem Th3: :: RINFSUP1:3

for b₁ being real number
for b₂ being Real_Sequence holds
( b₁ in rng b₂ iff - b₁ in rng (- b₂) )

proof end;

theorem Th4: :: RINFSUP1:4

for b₁ being Real_Sequence holds rng (- b₁) = - (rng b₁)

proof end;

theorem Th5: :: RINFSUP1:5

for b₁ being Real_Sequence holds
( b₁ is bounded_above iff rng b₁ is bounded_above )

proof end;

theorem Th6: :: RINFSUP1:6

for b₁ being Real_Sequence holds
( b₁ is bounded_below iff rng b₁ is bounded_below )

proof end;

theorem Th7: :: RINFSUP1:7

for b₁ being real number
for b₂ being Real_Sequence st b₂ is bounded_above holds
( b₁ = sup b₂ iff ( ( for b₃ being Nat holds b₂ . b₃ <= b₁ ) & ( for b₃ being real number st 0 < b₃ holds
ex b₄ being Nat st b₁ - b₃ < b₂ . b₄ ) ) )

proof end;

theorem Th8: :: RINFSUP1:8

for b₁ being real number
for b₂ being Real_Sequence st b₂ is bounded_below holds
( b₁ = inf b₂ iff ( ( for b₃ being Nat holds b₁ <= b₂ . b₃ ) & ( for b₃ being real number st 0 < b₃ holds
ex b₄ being Nat st b₂ . b₄ < b₁ + b₃ ) ) )

proof end;

theorem Th9: :: RINFSUP1:9

for b₁ being real number
for b₂ being Real_Sequence holds
( ( for b₃ being Nat holds b₂ . b₃ <= b₁ ) iff ( b₂ is bounded_above & sup b₂ <= b₁ ) )

proof end;

theorem Th10: :: RINFSUP1:10

for b₁ being real number
for b₂ being Real_Sequence holds
( ( for b₃ being Nat holds b₁ <= b₂ . b₃ ) iff ( b₂ is bounded_below & b₁ <= inf b₂ ) )

proof end;

theorem Th11: :: RINFSUP1:11

for b₁ being Real_Sequence holds
( b₁ is bounded_above iff - b₁ is bounded_below )

proof end;

theorem Th12: :: RINFSUP1:12

for b₁ being Real_Sequence holds
( b₁ is bounded_below iff - b₁ is bounded_above )

proof end;

theorem Th13: :: RINFSUP1:13

for b₁ being Real_Sequence st b₁ is bounded_above holds
sup b₁ = - (inf (- b₁))

proof end;

theorem Th14: :: RINFSUP1:14

for b₁ being Real_Sequence st b₁ is bounded_below holds
inf b₁ = - (sup (- b₁))

proof end;

theorem Th15: :: RINFSUP1:15

for b₁, b₂ being Real_Sequence st b₁ is bounded_below & b₂ is bounded_below holds
inf (b₁ + b₂) >= (inf b₁) + (inf b₂)

proof end;

theorem Th16: :: RINFSUP1:16

for b₁, b₂ being Real_Sequence st b₁ is bounded_above & b₂ is bounded_above holds
sup (b₁ + b₂) <= (sup b₁) + (sup b₂)

proof end;

notation

let c₁ be Real_Sequence;
synonym nonnegative c₁ for nonnegative-yielding c₁;

end;

definition

let c₁ be Real_Sequence;
redefine attr a₁ is nonnegative-yielding means :Def3: :: RINFSUP1:def 3
for b₁ being Nat holds a₁ . b₁ >= 0;
compatibility

proof end;

end;

:: deftheorem Def3 defines nonnegative RINFSUP1:def 3 :

theorem Th17: :: RINFSUP1:17

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is nonnegative holds
b₂ ^\ b₁ is nonnegative

proof end;

theorem Th18: :: RINFSUP1:18

for b₁ being Real_Sequence st b₁ is bounded_below & b₁ is nonnegative holds
inf b₁ >= 0

proof end;

theorem Th19: :: RINFSUP1:19

for b₁ being Real_Sequence st b₁ is bounded_above & b₁ is nonnegative holds
sup b₁ >= 0

proof end;

theorem Th20: :: RINFSUP1:20

for b₁, b₂ being Real_Sequence st b₁ is bounded_below & b₁ is nonnegative & b₂ is bounded_below & b₂ is nonnegative holds
( b₁ (#) b₂ is bounded_below & inf (b₁ (#) b₂) >= (inf b₁) * (inf b₂) )

proof end;

theorem Th21: :: RINFSUP1:21

for b₁, b₂ being Real_Sequence st b₁ is bounded_above & b₁ is nonnegative & b₂ is bounded_above & b₂ is nonnegative holds
( b₁ (#) b₂ is bounded_above & sup (b₁ (#) b₂) <= (sup b₁) * (sup b₂) )

proof end;

theorem Th22: :: RINFSUP1:22

for b₁ being Real_Sequence st b₁ is non-decreasing & b₁ is bounded_above holds
b₁ is bounded

proof end;

theorem Th23: :: RINFSUP1:23

for b₁ being Real_Sequence st b₁ is non-increasing & b₁ is bounded_below holds
b₁ is bounded

proof end;

theorem Th24: :: RINFSUP1:24

for b₁ being Real_Sequence st b₁ is non-decreasing & b₁ is bounded_above holds
lim b₁ = sup b₁

proof end;

theorem Th25: :: RINFSUP1:25

for b₁ being Real_Sequence st b₁ is non-increasing & b₁ is bounded_below holds
lim b₁ = inf b₁

proof end;

theorem Th26: :: RINFSUP1:26

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded_above holds
b₂ ^\ b₁ is bounded_above

proof end;

theorem Th27: :: RINFSUP1:27

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded_below holds
b₂ ^\ b₁ is bounded_below

proof end;

theorem Th28: :: RINFSUP1:28

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded holds
b₂ ^\ b₁ is bounded

proof end;

theorem Th29: :: RINFSUP1:29

for b₁ being Real_Sequence
for b₂ being Nat holds { (b₁ . b₃) where B is Nat : b₂ <= b₃ } is Subset of REAL

proof end;

theorem Th30: :: RINFSUP1:30

for b₁ being Nat
for b₂ being Real_Sequence holds rng (b₂ ^\ b₁) = { (b₂ . b₃) where B is Nat : b₁ <= b₃ }

proof end;

theorem Th31: :: RINFSUP1:31

for b₁ being Real_Sequence st b₁ is bounded_above holds
for b₂ being Nat
for b₃ being Subset of REAL st b₃ = { (b₁ . b₄) where B is Nat : b₂ <= b₄ } holds
b₃ is bounded_above

proof end;

theorem Th32: :: RINFSUP1:32

for b₁ being Real_Sequence st b₁ is bounded_below holds
for b₂ being Nat
for b₃ being Subset of REAL st b₃ = { (b₁ . b₄) where B is Nat : b₂ <= b₄ } holds
b₃ is bounded_below

proof end;

theorem Th33: :: RINFSUP1:33

for b₁ being Real_Sequence st b₁ is bounded holds
for b₂ being Nat
for b₃ being Subset of REAL st b₃ = { (b₁ . b₄) where B is Nat : b₂ <= b₄ } holds
b₃ is bounded

proof end;

theorem Th34: :: RINFSUP1:34

for b₁ being Real_Sequence st b₁ is non-decreasing holds
for b₂ being Nat
for b₃ being Subset of REAL st b₃ = { (b₁ . b₄) where B is Nat : b₂ <= b₄ } holds
inf b₃ = b₁ . b₂

proof end;

theorem Th35: :: RINFSUP1:35

for b₁ being Real_Sequence st b₁ is non-increasing holds
for b₂ being Nat
for b₃ being Subset of REAL st b₃ = { (b₁ . b₄) where B is Nat : b₂ <= b₄ } holds
sup b₃ = b₁ . b₂

proof end;

theorem Th36: :: RINFSUP1:36

for b₁ being Real_Sequence ex b₂ being Function of NAT , REAL st
for b₃ being Nat
for b₄ being Subset of REAL st b₄ = { (b₁ . b₅) where B is Nat : b₃ <= b₅ } holds
b₂ . b₃ = sup b₄

proof end;

theorem Th37: :: RINFSUP1:37

for b₁ being Real_Sequence ex b₂ being Function of NAT , REAL st
for b₃ being Nat
for b₄ being Subset of REAL st b₄ = { (b₁ . b₅) where B is Nat : b₃ <= b₅ } holds
b₂ . b₃ = inf b₄

proof end;

definition

let c₁ be Real_Sequence;
func inferior_realsequence c₁ -> Real_Sequence means :Def4: :: RINFSUP1:def 4
for b₁ being Nat
for b₂ being Subset of REAL st b₂ = { (a₁ . b₃) where B is Nat : b₁ <= b₃ } holds
a₂ . b₁ = inf b₂;
existence by Th37;
uniqueness

proof end;

end;

:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def 4 :

definition

let c₁ be Real_Sequence;
func superior_realsequence c₁ -> Real_Sequence means :Def5: :: RINFSUP1:def 5
for b₁ being Nat
for b₂ being Subset of REAL st b₂ = { (a₁ . b₃) where B is Nat : b₁ <= b₃ } holds
a₂ . b₁ = sup b₂;
existence by Th36;
uniqueness

proof end;

end;

:: deftheorem Def5 defines superior_realsequence RINFSUP1:def 5 :

theorem Th38: :: RINFSUP1:38

for b₁ being Nat
for b₂ being Real_Sequence holds (inferior_realsequence b₂) . b₁ = inf (b₂ ^\ b₁)

proof end;

theorem Th39: :: RINFSUP1:39

for b₁ being Nat
for b₂ being Real_Sequence holds (superior_realsequence b₂) . b₁ = sup (b₂ ^\ b₁)

proof end;

theorem Th40: :: RINFSUP1:40

for b₁ being Real_Sequence st b₁ is bounded_below holds
(inferior_realsequence b₁) . 0 = inf b₁

proof end;

theorem Th41: :: RINFSUP1:41

for b₁ being Real_Sequence st b₁ is bounded_above holds
(superior_realsequence b₁) . 0 = sup b₁

proof end;

theorem Th42: :: RINFSUP1:42

for b₁ being Nat
for b₂ being real number
for b₃ being Real_Sequence st b₃ is bounded_below holds
( b₂ = (inferior_realsequence b₃) . b₁ iff ( ( for b₄ being Nat holds b₂ <= b₃ . (b₁ + b₄) ) & ( for b₄ being real number st 0 < b₄ holds
ex b₅ being Nat st b₃ . (b₁ + b₅) < b₂ + b₄ ) ) )

proof end;

theorem Th43: :: RINFSUP1:43

for b₁ being Nat
for b₂ being real number
for b₃ being Real_Sequence st b₃ is bounded_above holds
( b₂ = (superior_realsequence b₃) . b₁ iff ( ( for b₄ being Nat holds b₃ . (b₁ + b₄) <= b₂ ) & ( for b₄ being real number st 0 < b₄ holds
ex b₅ being Nat st b₂ - b₄ < b₃ . (b₁ + b₅) ) ) )

proof end;

theorem Th44: :: RINFSUP1:44

for b₁ being Nat
for b₂ being real number
for b₃ being Real_Sequence st b₃ is bounded_below holds
( ( for b₄ being Nat holds b₂ <= b₃ . (b₁ + b₄) ) iff b₂ <= (inferior_realsequence b₃) . b₁ )

proof end;

theorem Th45: :: RINFSUP1:45

for b₁ being Nat
for b₂ being real number
for b₃ being Real_Sequence st b₃ is bounded_below holds
( ( for b₄ being Nat st b₁ <= b₄ holds
b₂ <= b₃ . b₄ ) iff b₂ <= (inferior_realsequence b₃) . b₁ )

proof end;

theorem Th46: :: RINFSUP1:46

for b₁ being Nat
for b₂ being real number
for b₃ being Real_Sequence st b₃ is bounded_above holds
( ( for b₄ being Nat holds b₃ . (b₁ + b₄) <= b₂ ) iff (superior_realsequence b₃) . b₁ <= b₂ )

proof end;

theorem Th47: :: RINFSUP1:47

for b₁ being Nat
for b₂ being real number
for b₃ being Real_Sequence st b₃ is bounded_above holds
( ( for b₄ being Nat st b₁ <= b₄ holds
b₃ . b₄ <= b₂ ) iff (superior_realsequence b₃) . b₁ <= b₂ )

proof end;

theorem Th48: :: RINFSUP1:48

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded_below holds
(inferior_realsequence b₂) . b₁ = min ((inferior_realsequence b₂) . (b₁ + 1)),(b₂ . b₁)

proof end;

theorem Th49: :: RINFSUP1:49

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded_above holds
(superior_realsequence b₂) . b₁ = max ((superior_realsequence b₂) . (b₁ + 1)),(b₂ . b₁)

proof end;

theorem Th50: :: RINFSUP1:50

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded_below holds
(inferior_realsequence b₂) . b₁ <= (inferior_realsequence b₂) . (b₁ + 1)

proof end;

theorem Th51: :: RINFSUP1:51

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded_above holds
(superior_realsequence b₂) . (b₁ + 1) <= (superior_realsequence b₂) . b₁

proof end;

theorem Th52: :: RINFSUP1:52

for b₁ being Real_Sequence st b₁ is bounded_below holds
inferior_realsequence b₁ is non-decreasing

proof end;

theorem Th53: :: RINFSUP1:53

for b₁ being Real_Sequence st b₁ is bounded_above holds
superior_realsequence b₁ is non-increasing

proof end;

theorem Th54: :: RINFSUP1:54

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded holds
(inferior_realsequence b₂) . b₁ <= (superior_realsequence b₂) . b₁

proof end;

theorem Th55: :: RINFSUP1:55

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded holds
(inferior_realsequence b₂) . b₁ <= inf (superior_realsequence b₂)

proof end;

theorem Th56: :: RINFSUP1:56

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded holds
sup (inferior_realsequence b₂) <= (superior_realsequence b₂) . b₁

proof end;

theorem Th57: :: RINFSUP1:57

for b₁ being Real_Sequence st b₁ is bounded holds
sup (inferior_realsequence b₁) <= inf (superior_realsequence b₁)

proof end;

theorem Th58: :: RINFSUP1:58

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

proof end;

theorem Th59: :: RINFSUP1:59

for b₁ being Real_Sequence st b₁ is bounded holds
( inferior_realsequence b₁ is convergent & lim (inferior_realsequence b₁) = sup (inferior_realsequence b₁) )

proof end;

theorem Th60: :: RINFSUP1:60

for b₁ being Real_Sequence st b₁ is bounded holds
( superior_realsequence b₁ is convergent & lim (superior_realsequence b₁) = inf (superior_realsequence b₁) )

proof end;

theorem Th61: :: RINFSUP1:61

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded_below holds
(inferior_realsequence b₂) . b₁ = - ((superior_realsequence (- b₂)) . b₁)

proof end;

theorem Th62: :: RINFSUP1:62

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is bounded_above holds
(superior_realsequence b₂) . b₁ = - ((inferior_realsequence (- b₂)) . b₁)

proof end;

theorem Th63: :: RINFSUP1:63

for b₁ being Real_Sequence st b₁ is bounded_below holds
inferior_realsequence b₁ = - (superior_realsequence (- b₁))

proof end;

theorem Th64: :: RINFSUP1:64

for b₁ being Real_Sequence st b₁ is bounded_above holds
superior_realsequence b₁ = - (inferior_realsequence (- b₁))

proof end;

theorem Th65: :: RINFSUP1:65

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-decreasing holds
b₂ . b₁ <= (inferior_realsequence b₂) . (b₁ + 1)

proof end;

Lemma66: for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-decreasing holds
(inferior_realsequence b₂) . b₁ = b₂ . b₁

proof end;

theorem Th66: :: RINFSUP1:66

for b₁ being Real_Sequence st b₁ is non-decreasing holds
inferior_realsequence b₁ = b₁

proof end;

theorem Th67: :: RINFSUP1:67

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-decreasing & b₂ is bounded_above holds
b₂ . b₁ <= (superior_realsequence b₂) . (b₁ + 1)

proof end;

theorem Th68: :: RINFSUP1:68

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-decreasing & b₂ is bounded_above holds
(superior_realsequence b₂) . b₁ = (superior_realsequence b₂) . (b₁ + 1)

proof end;

theorem Th69: :: RINFSUP1:69

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-decreasing & b₂ is bounded_above holds
( (superior_realsequence b₂) . b₁ = sup b₂ & superior_realsequence b₂ is constant )

proof end;

theorem Th70: :: RINFSUP1:70

for b₁ being Real_Sequence st b₁ is non-decreasing & b₁ is bounded_above holds
inf (superior_realsequence b₁) = sup b₁

proof end;

theorem Th71: :: RINFSUP1:71

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-increasing holds
(superior_realsequence b₂) . (b₁ + 1) <= b₂ . b₁

proof end;

Lemma70: for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-increasing holds
(superior_realsequence b₂) . b₁ = b₂ . b₁

proof end;

theorem Th72: :: RINFSUP1:72

for b₁ being Real_Sequence st b₁ is non-increasing holds
superior_realsequence b₁ = b₁

proof end;

theorem Th73: :: RINFSUP1:73

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-increasing & b₂ is bounded_below holds
(inferior_realsequence b₂) . (b₁ + 1) <= b₂ . b₁

proof end;

theorem Th74: :: RINFSUP1:74

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-increasing & b₂ is bounded_below holds
(inferior_realsequence b₂) . b₁ = (inferior_realsequence b₂) . (b₁ + 1)

proof end;

theorem Th75: :: RINFSUP1:75

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is non-increasing & b₂ is bounded_below holds
( (inferior_realsequence b₂) . b₁ = inf b₂ & inferior_realsequence b₂ is constant )

proof end;

theorem Th76: :: RINFSUP1:76

for b₁ being Real_Sequence st b₁ is non-increasing & b₁ is bounded_below holds
sup (inferior_realsequence b₁) = inf b₁

proof end;

theorem Th77: :: RINFSUP1:77

for b₁, b₂ being Real_Sequence st b₁ is bounded & b₂ is bounded & ( for b₃ being Nat holds b₁ . b₃ <= b₂ . b₃ ) holds
( ( for b₃ being Nat holds (superior_realsequence b₁) . b₃ <= (superior_realsequence b₂) . b₃ ) & ( for b₃ being Nat holds (inferior_realsequence b₁) . b₃ <= (inferior_realsequence b₂) . b₃ ) )

proof end;

theorem Th78: :: RINFSUP1:78

for b₁ being Nat
for b₂, b₃ being Real_Sequence st b₂ is bounded_below & b₃ is bounded_below holds
(inferior_realsequence (b₂ + b₃)) . b₁ >= ((inferior_realsequence b₂) . b₁) + ((inferior_realsequence b₃) . b₁)

proof end;

theorem Th79: :: RINFSUP1:79

for b₁ being Nat
for b₂, b₃ being Real_Sequence st b₂ is bounded_above & b₃ is bounded_above holds
(superior_realsequence (b₂ + b₃)) . b₁ <= ((superior_realsequence b₂) . b₁) + ((superior_realsequence b₃) . b₁)

proof end;

theorem Th80: :: RINFSUP1:80

for b₁ being Nat
for b₂, b₃ being Real_Sequence st b₂ is bounded_below & b₂ is nonnegative & b₃ is bounded_below & b₃ is nonnegative holds
(inferior_realsequence (b₂ (#) b₃)) . b₁ >= ((inferior_realsequence b₂) . b₁) * ((inferior_realsequence b₃) . b₁)

proof end;

theorem Th81: :: RINFSUP1:81

proof end;

theorem Th82: :: RINFSUP1:82

for b₁ being Nat
for b₂, b₃ being Real_Sequence st b₂ is bounded_above & b₂ is nonnegative & b₃ is bounded_above & b₃ is nonnegative holds
(superior_realsequence (b₂ (#) b₃)) . b₁ <= ((superior_realsequence b₂) . b₁) * ((superior_realsequence b₃) . b₁)

proof end;

definition

let c₁ be Real_Sequence;
func lim_sup c₁ -> Element of REAL equals :: RINFSUP1:def 6
inf (superior_realsequence a₁);
coherence ;

end;

:: deftheorem Def6 defines lim_sup RINFSUP1:def 6 :

definition

let c₁ be Real_Sequence;
func lim_inf c₁ -> Element of REAL equals :: RINFSUP1:def 7
sup (inferior_realsequence a₁);
coherence ;

end;

:: deftheorem Def7 defines lim_inf RINFSUP1:def 7 :

theorem Th83: :: RINFSUP1:83

for b₁ being real number
for b₂ being Real_Sequence st b₂ is bounded holds
( lim_inf b₂ <= b₁ iff for b₃ being real number st 0 < b₃ holds
for b₄ being Nat ex b₅ being Nat st b₂ . (b₄ + b₅) < b₁ + b₃ )

proof end;

theorem Th84: :: RINFSUP1:84

for b₁ being real number
for b₂ being Real_Sequence st b₂ is bounded holds
( b₁ <= lim_inf b₂ iff for b₃ being real number st 0 < b₃ holds
ex b₄ being Nat st
for b₅ being Nat holds b₁ - b₃ < b₂ . (b₄ + b₅) )

proof end;

theorem Th85: :: RINFSUP1:85

for b₁ being real number
for b₂ being Real_Sequence st b₂ is bounded holds
( b₁ = lim_inf b₂ iff for b₃ being real number st 0 < b₃ holds
( ( for b₄ being Nat ex b₅ being Nat st b₂ . (b₄ + b₅) < b₁ + b₃ ) & ex b₄ being Nat st
for b₅ being Nat holds b₁ - b₃ < b₂ . (b₄ + b₅) ) )

proof end;

theorem Th86: :: RINFSUP1:86

for b₁ being real number
for b₂ being Real_Sequence st b₂ is bounded holds
( b₁ <= lim_sup b₂ iff for b₃ being real number st 0 < b₃ holds
for b₄ being Nat ex b₅ being Nat st b₂ . (b₄ + b₅) > b₁ - b₃ )

proof end;

theorem Th87: :: RINFSUP1:87

for b₁ being real number
for b₂ being Real_Sequence st b₂ is bounded holds
( lim_sup b₂ <= b₁ iff for b₃ being real number st 0 < b₃ holds
ex b₄ being Nat st
for b₅ being Nat holds b₂ . (b₄ + b₅) < b₁ + b₃ )

proof end;

theorem Th88: :: RINFSUP1:88

for b₁ being real number
for b₂ being Real_Sequence st b₂ is bounded holds
( b₁ = lim_sup b₂ iff for b₃ being real number st 0 < b₃ holds
( ( for b₄ being Nat ex b₅ being Nat st b₂ . (b₄ + b₅) > b₁ - b₃ ) & ex b₄ being Nat st
for b₅ being Nat holds b₂ . (b₄ + b₅) < b₁ + b₃ ) )

proof end;

theorem Th89: :: RINFSUP1:89

for b₁ being Real_Sequence st b₁ is bounded holds
lim_inf b₁ <= lim_sup b₁ by Th57;

theorem Th90: :: RINFSUP1:90

for b₁ being Real_Sequence holds
( ( b₁ is bounded & lim_sup b₁ = lim_inf b₁ ) iff b₁ is convergent )

proof end;

theorem Th91: :: RINFSUP1:91

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

proof end;

theorem Th92: :: RINFSUP1:92

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

proof end;

theorem Th93: :: RINFSUP1:93

for b₁, b₂ being Real_Sequence st b₁ is bounded & b₂ is bounded & ( for b₃ being Nat holds b₁ . b₃ <= b₂ . b₃ ) holds
( lim_sup b₁ <= lim_sup b₂ & lim_inf b₁ <= lim_inf b₂ )

proof end;

theorem Th94: :: RINFSUP1:94

for b₁, b₂ being Real_Sequence st b₁ is bounded & b₂ is bounded holds
( (lim_inf b₁) + (lim_inf b₂) <= lim_inf (b₁ + b₂) & lim_inf (b₁ + b₂) <= (lim_inf b₁) + (lim_sup b₂) & lim_inf (b₁ + b₂) <= (lim_sup b₁) + (lim_inf b₂) & (lim_inf b₁) + (lim_sup b₂) <= lim_sup (b₁ + b₂) & (lim_sup b₁) + (lim_inf b₂) <= lim_sup (b₁ + b₂) & lim_sup (b₁ + b₂) <= (lim_sup b₁) + (lim_sup b₂) & ( ( b₁ is convergent or b₂ is convergent ) implies ( lim_inf (b₁ + b₂) = (lim_inf b₁) + (lim_inf b₂) & lim_sup (b₁ + b₂) = (lim_sup b₁) + (lim_sup b₂) ) ) )

proof end;

theorem Th95: :: RINFSUP1:95

for b₁, b₂ being Real_Sequence st b₁ is bounded & b₁ is nonnegative & b₂ is bounded & b₂ is nonnegative holds
( (lim_inf b₁) * (lim_inf b₂) <= lim_inf (b₁ (#) b₂) & lim_sup (b₁ (#) b₂) <= (lim_sup b₁) * (lim_sup b₂) )

proof end;