:: RINFSUP1 semantic presentation

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

proof end;

theorem Th1: :: RINFSUP1:1

for s, r, t being real number holds
( ( s - r < t & s + r > t ) iff abs (t - s) < r )

proof end;

definition

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

end;

:: deftheorem defines sup RINFSUP1:def 1 :

definition

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

end;

:: deftheorem defines inf RINFSUP1:def 2 :

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 number
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 bounded_above iff rng seq is bounded_above )

proof end;

theorem Th6: :: RINFSUP1:6

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

proof end;

theorem Th7: :: RINFSUP1:7

for r being real number
for seq being Real_Sequence st seq is bounded_above holds
( r = sup seq iff ( ( for n being Nat holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Nat st r - s < seq . k ) ) )

proof end;

theorem Th8: :: RINFSUP1:8

for r being real number
for seq being Real_Sequence st seq is bounded_below holds
( r = inf seq iff ( ( for n being Nat holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Nat st seq . k < r + s ) ) )

proof end;

theorem Th9: :: RINFSUP1:9

for r being real number
for seq being Real_Sequence holds
( ( for n being Nat holds seq . n <= r ) iff ( seq is bounded_above & sup seq <= r ) )

proof end;

theorem Th10: :: RINFSUP1:10

for r being real number
for seq being Real_Sequence holds
( ( for n being Nat holds r <= seq . n ) iff ( seq is bounded_below & r <= inf seq ) )

proof end;

theorem Th11: :: RINFSUP1:11

for seq being Real_Sequence holds
( seq is bounded_above iff - seq is bounded_below )

proof end;

theorem Th12: :: RINFSUP1:12

for seq being Real_Sequence holds
( seq is bounded_below iff - seq is bounded_above )

proof end;

theorem Th13: :: RINFSUP1:13

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

proof end;

theorem Th14: :: RINFSUP1:14

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

proof end;

theorem Th15: :: RINFSUP1:15

for seq1, seq2 being Real_Sequence st seq1 is bounded_below & seq2 is bounded_below holds
inf (seq1 + seq2) >= (inf seq1) + (inf seq2)

proof end;

theorem Th16: :: RINFSUP1:16

for seq1, seq2 being Real_Sequence st seq1 is bounded_above & seq2 is bounded_above holds
sup (seq1 + seq2) <= (sup seq1) + (sup seq2)

proof end;

notation

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

end;

definition

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

proof end;

end;

:: deftheorem Def3 defines nonnegative RINFSUP1:def 3 :

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 bounded_below & seq is nonnegative holds
inf seq >= 0

proof end;

theorem :: RINFSUP1:19

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

proof end;

theorem Th20: :: RINFSUP1:20

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

proof end;

theorem Th21: :: RINFSUP1:21

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

proof end;

theorem Th22: :: RINFSUP1:22

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

proof end;

theorem Th23: :: RINFSUP1:23

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

proof end;

theorem Th24: :: RINFSUP1:24

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

proof end;

theorem Th25: :: RINFSUP1:25

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

proof end;

theorem Th26: :: RINFSUP1:26

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

proof end;

theorem Th27: :: RINFSUP1:27

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

proof end;

theorem :: RINFSUP1:28

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

proof end;

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 bounded_above 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 bounded_below 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 bounded

proof end;

theorem Th34: :: RINFSUP1:34

for seq being Real_Sequence st seq is non-decreasing holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
inf R = seq . n

proof end;

theorem Th35: :: RINFSUP1:35

for seq being Real_Sequence st seq is non-increasing holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
sup R = seq . n

proof end;

theorem Th36: :: RINFSUP1:36

for seq being Real_Sequence ex f being Function of NAT , REAL st
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
f . n = sup Y

proof end;

theorem Th37: :: RINFSUP1:37

for seq being Real_Sequence ex f being Function of NAT , REAL st
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
f . n = inf Y

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 = inf Y;
existence by Th37;
uniqueness

proof end;

end;

:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def 4 :

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 = sup Y;
existence by Th36;
uniqueness

proof end;

end;

:: deftheorem Def5 defines superior_realsequence RINFSUP1:def 5 :

theorem Th38: :: RINFSUP1:38

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

proof end;

theorem Th39: :: RINFSUP1:39

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

proof end;

theorem Th40: :: RINFSUP1:40

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

proof end;

theorem Th41: :: RINFSUP1:41

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

proof end;

theorem Th42: :: RINFSUP1:42

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

proof end;

theorem Th43: :: RINFSUP1:43

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

proof end;

theorem Th44: :: RINFSUP1:44

for n being Nat
for r being real number
for seq being Real_Sequence st seq is bounded_below holds
( ( for k being Nat holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )

proof end;

theorem Th45: :: RINFSUP1:45

for n being Nat
for r being real number
for seq being Real_Sequence st seq is bounded_below holds
( ( for m being Nat st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )

proof end;

theorem Th46: :: RINFSUP1:46

for n being Nat
for r being real number
for seq being Real_Sequence st seq is bounded_above holds
( ( for k being Nat holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )

proof end;

theorem Th47: :: RINFSUP1:47

for n being Nat
for r being real number
for seq being Real_Sequence st seq is bounded_above holds
( ( for m being Nat st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )

proof end;

theorem Th48: :: RINFSUP1:48

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

proof end;

theorem Th49: :: RINFSUP1:49

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

proof end;

theorem Th50: :: RINFSUP1:50

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

proof end;

theorem Th51: :: RINFSUP1:51

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

proof end;

theorem Th52: :: RINFSUP1:52

for seq being Real_Sequence st seq is bounded_below holds
inferior_realsequence seq is non-decreasing

proof end;

theorem Th53: :: RINFSUP1:53

for seq being Real_Sequence st seq is bounded_above holds
superior_realsequence seq is non-increasing

proof end;

theorem :: RINFSUP1:54

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 Th55: :: RINFSUP1:55

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

proof end;

theorem Th56: :: RINFSUP1:56

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

proof end;

theorem Th57: :: RINFSUP1:57

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

proof end;

theorem Th58: :: RINFSUP1:58

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

proof end;

theorem Th59: :: RINFSUP1:59

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

proof end;

theorem Th60: :: RINFSUP1:60

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

proof end;

theorem Th61: :: RINFSUP1:61

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

proof end;

theorem Th62: :: RINFSUP1:62

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

proof end;

theorem Th63: :: RINFSUP1:63

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

proof end;

theorem Th64: :: RINFSUP1:64

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

proof end;

theorem :: RINFSUP1:65

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

proof end;

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

proof end;

theorem :: RINFSUP1:66

for seq being Real_Sequence st seq is non-decreasing holds
inferior_realsequence seq = seq

proof end;

theorem Th67: :: RINFSUP1:67

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

proof end;

theorem Th68: :: RINFSUP1:68

for n being Nat
for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
(superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)

proof end;

theorem Th69: :: RINFSUP1:69

for n being Nat
for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
( (superior_realsequence seq) . n = sup seq & superior_realsequence seq is constant )

proof end;

theorem :: RINFSUP1:70

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

proof end;

theorem :: RINFSUP1:71

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

proof end;

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

proof end;

theorem :: RINFSUP1:72

for seq being Real_Sequence st seq is non-increasing holds
superior_realsequence seq = seq

proof end;

theorem Th73: :: RINFSUP1:73

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

proof end;

theorem Th74: :: RINFSUP1:74

for n being Nat
for seq being Real_Sequence st seq is non-increasing & seq is bounded_below holds
(inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)

proof end;

theorem Th75: :: RINFSUP1:75

for n being Nat
for seq being Real_Sequence st seq is non-increasing & seq is bounded_below holds
( (inferior_realsequence seq) . n = inf seq & inferior_realsequence seq is constant )

proof end;

theorem :: RINFSUP1:76

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

proof end;

theorem Th77: :: RINFSUP1:77

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:78

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

proof end;

theorem :: RINFSUP1:79

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

proof end;

theorem :: RINFSUP1:80

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

proof end;

theorem Th81: :: RINFSUP1:81

proof end;

theorem Th82: :: RINFSUP1:82

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is bounded_above & seq1 is nonnegative & seq2 is bounded_above & 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 -> Element of REAL equals :: RINFSUP1:def 6
inf (superior_realsequence seq);
coherence ;

end;

:: deftheorem defines lim_sup RINFSUP1:def 6 :

definition

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

end;

:: deftheorem defines lim_inf RINFSUP1:def 7 :

theorem Th83: :: RINFSUP1:83

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 Nat ex k being Nat st seq . (n + k) < r + s )

proof end;

theorem Th84: :: RINFSUP1:84

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 Nat st
for k being Nat holds r - s < seq . (n + k) )

proof end;

theorem :: RINFSUP1:85

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 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 Th86: :: 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 Nat ex k being Nat st seq . (n + k) > r - s )

proof end;

theorem Th87: :: RINFSUP1:87

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 Nat st
for k being Nat holds seq . (n + k) < r + s )

proof end;

theorem :: RINFSUP1:88

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 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:89

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

theorem Th90: :: RINFSUP1:90

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

proof end;

theorem :: RINFSUP1:91

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

proof end;

theorem Th92: :: RINFSUP1:92

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:93

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:94

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:95

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;