:: Convergent Sequences and the Limit of Sequences
:: by Jaros{\l}aw Kotowicz
::
:: Received July 4, 1989
:: Copyright (c) 1990 Association of Mizar Users


begin

theorem :: SEQ_2:1
canceled;

theorem :: SEQ_2:2
canceled;

theorem :: SEQ_2:3
canceled;

theorem :: SEQ_2:4
canceled;

theorem :: SEQ_2:5
canceled;

theorem :: SEQ_2:6
canceled;

theorem :: SEQ_2:7
canceled;

theorem :: SEQ_2:8
canceled;

theorem Th9: :: SEQ_2:9
for g, r being real number holds
( ( - g < r & r < g ) iff abs r < g )
proof end;

theorem :: SEQ_2:10
canceled;

theorem Th11: :: SEQ_2:11
for g, r being real number st g <> 0 & r <> 0 holds
abs ((g ") - (r ")) = (abs (g - r)) / ((abs g) * (abs r))
proof end;

definition
let f be real-valued Function;
attr f is bounded_above means :Def1: :: SEQ_2:def 1
 ex r being real number st
for y being set st y in dom f holds
f . y < r;
attr f is bounded_below means :Def2: :: SEQ_2:def 2
 ex r being real number st
for y being set st y in dom f holds
r < f . y;
end;

:: deftheorem Def1 defines bounded_above SEQ_2:def 1 :
for f being real-valued Function holds
( f is bounded_above iff ex r being real number st
for y being set st y in dom f holds
f . y < r );

:: deftheorem Def2 defines bounded_below SEQ_2:def 2 :
for f being real-valued Function holds
( f is bounded_below iff ex r being real number st
for y being set st y in dom f holds
r < f . y );

definition
let seq be Real_Sequence;
A1: dom seq = NAT by SEQ_1:3;
redefine attr seq is bounded_above means :Def3: :: SEQ_2:def 3
 ex r being real number st
for n being Element of NAT holds seq . n < r;
compatibility
( seq is bounded_above iff ex r being real number st
for n being Element of NAT holds seq . n < r )
proof end;
redefine attr seq is bounded_below means :Def4: :: SEQ_2:def 4
 ex r being real number st
for n being Element of NAT holds r < seq . n;
compatibility
( seq is bounded_below iff ex r being real number st
for n being Element of NAT holds r < seq . n )
proof end;
end;

:: deftheorem Def3 defines bounded_above SEQ_2:def 3 :
for seq being Real_Sequence holds
( seq is bounded_above iff ex r being real number st
for n being Element of NAT holds seq . n < r );

:: deftheorem Def4 defines bounded_below SEQ_2:def 4 :
for seq being Real_Sequence holds
( seq is bounded_below iff ex r being real number st
for n being Element of NAT holds r < seq . n );

definition
let f be complex-valued Function;
attr f is bounded means :: SEQ_2:def 5
 ex r being real number st
for y being set st y in dom f holds
abs (f . y) < r;
end;

:: deftheorem defines bounded SEQ_2:def 5 :
for f being complex-valued Function holds
( f is bounded iff ex r being real number st
for y being set st y in dom f holds
abs (f . y) < r );

registration
cluster Relation-like Function-like real-valued bounded -> real-valued bounded_above bounded_below set ;
coherence
for b1 being real-valued Function st b1 is bounded holds
( b1 is bounded_above & b1 is bounded_below )
proof end;
cluster Relation-like Function-like real-valued bounded_above bounded_below -> real-valued bounded set ;
coherence
for b1 being real-valued Function st b1 is bounded_above & b1 is bounded_below holds
b1 is bounded
proof end;
end;

theorem :: SEQ_2:12
canceled;

theorem :: SEQ_2:13
canceled;

theorem :: SEQ_2:14
canceled;

theorem Th15: :: SEQ_2:15
for seq being Real_Sequence holds
( seq is bounded iff ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) )
proof end;

theorem Th16: :: SEQ_2:16
for seq being Real_Sequence
for n being Element of NAT ex r being real number st
( 0 < r & ( for m being Element of NAT st m <= n holds
abs (seq . m) < r ) )
proof end;

definition
let seq be Real_Sequence;
attr seq is convergent means :Def6: :: SEQ_2:def 6
 ex g being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p;
end;

:: deftheorem Def6 defines convergent SEQ_2:def 6 :
for seq being Real_Sequence holds
( seq is convergent iff ex g being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p );

definition
let seq be Real_Sequence;
assume A1: seq is convergent ;
func lim seq -> real number means :Def7: :: SEQ_2:def 7
 for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - it) < p;
existence
ex b1 being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - b1) < p by A1, Def6;
uniqueness
for b1, b2 being real number st ( for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - b1) < p ) & ( for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - b2) < p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines lim SEQ_2:def 7 :
for seq being Real_Sequence st seq is convergent holds
for b2 being real number holds
( b2 = lim seq iff for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - b2) < p );

definition
let f be real-valued Function;
redefine attr f is bounded means :: SEQ_2:def 8
( f is bounded_above & f is bounded_below );
compatibility
( f is bounded iff ( f is bounded_above & f is bounded_below ) ) ;
end;

:: deftheorem defines bounded SEQ_2:def 8 :
for f being real-valued Function holds
( f is bounded iff ( f is bounded_above & f is bounded_below ) );

definition
let seq be Real_Sequence;
:: original: lim
redefine func lim seq -> Real;
coherence
lim seq is Real by XREAL_0:def 1;
end;

theorem :: SEQ_2:17
canceled;

theorem :: SEQ_2:18
canceled;

theorem Th19: :: SEQ_2:19
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
seq + seq9 is convergent
proof end;

theorem Th20: :: SEQ_2:20
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
lim (seq + seq9) = (lim seq) + (lim seq9)
proof end;

theorem Th21: :: SEQ_2:21
for r being real number
for seq being Real_Sequence st seq is convergent holds
r (#) seq is convergent
proof end;

theorem Th22: :: SEQ_2:22
for r being real number
for seq being Real_Sequence st seq is convergent holds
lim (r (#) seq) = r * (lim seq)
proof end;

theorem :: SEQ_2:23
for seq being Real_Sequence st seq is convergent holds
- seq is convergent by Th21;

theorem Th24: :: SEQ_2:24
for seq being Real_Sequence st seq is convergent holds
lim (- seq) = - (lim seq)
proof end;

theorem Th25: :: SEQ_2:25
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
seq - seq9 is convergent
proof end;

theorem Th26: :: SEQ_2:26
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
lim (seq - seq9) = (lim seq) - (lim seq9)
proof end;

theorem Th27: :: SEQ_2:27
for seq being Real_Sequence st seq is convergent holds
seq is bounded
proof end;

theorem Th28: :: SEQ_2:28
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
seq (#) seq9 is convergent
proof end;

theorem Th29: :: SEQ_2:29
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
lim (seq (#) seq9) = (lim seq) * (lim seq9)
proof end;

theorem Th30: :: SEQ_2:30
for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(abs (lim seq)) / 2 < abs (seq . m)
proof end;

theorem Th31: :: SEQ_2:31
for seq being Real_Sequence st seq is convergent & ( for n being Element of NAT holds 0 <= seq . n ) holds
0 <= lim seq
proof end;

theorem :: SEQ_2:32
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent & ( for n being Element of NAT holds seq . n <= seq9 . n ) holds
lim seq <= lim seq9
proof end;

theorem Th33: :: SEQ_2:33
for seq, seq9, seq1 being Real_Sequence st seq is convergent & seq9 is convergent & ( for n being Element of NAT holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 holds
seq1 is convergent
proof end;

theorem :: SEQ_2:34
for seq, seq9, seq1 being Real_Sequence st seq is convergent & seq9 is convergent & ( for n being Element of NAT holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 holds
lim seq1 = lim seq
proof end;

theorem Th35: :: SEQ_2:35
for seq being Real_Sequence st seq is convergent & lim seq <> 0 & seq is non-empty holds
seq " is convergent
proof end;

theorem Th36: :: SEQ_2:36
for seq being Real_Sequence st seq is convergent & lim seq <> 0 & seq is non-empty holds
lim (seq ") = (lim seq) "
proof end;

theorem :: SEQ_2:37
for seq9, seq being Real_Sequence st seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-empty holds
seq9 /" seq is convergent
proof end;

theorem :: SEQ_2:38
for seq9, seq being Real_Sequence st seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-empty holds
lim (seq9 /" seq) = (lim seq9) / (lim seq)
proof end;

theorem Th39: :: SEQ_2:39
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is bounded & lim seq = 0 holds
seq (#) seq1 is convergent
proof end;

theorem :: SEQ_2:40
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is bounded & lim seq = 0 holds
lim (seq (#) seq1) = 0
proof end;