:: Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
:: by Hiroshi Yamazaki , Noboru Endou , Yasunari Shidama and Hiroyuki Okazaki
::
:: Received August 28, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: RINFSUP2:1
for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & Y is bounded_above holds
( X is bounded_above & sup X = upper_bound Y )
proofend;

theorem :: RINFSUP2:2
for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & X is bounded_above holds
( Y is bounded_above & sup X = upper_bound Y ) by Th1;

theorem Th3: :: RINFSUP2:3
for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & Y is bounded_below holds
( X is bounded_below & inf X = lower_bound Y )
proofend;

theorem :: RINFSUP2:4
for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & X is bounded_below holds
( Y is bounded_below & inf X = lower_bound Y ) by Th3;

definition
let seq be ExtREAL_sequence;
func sup seq ->  Element of ExtREAL  equals :: RINFSUP2:def 1
 sup (rng seq);
coherence
 sup (rng seq) is Element of ExtREAL ;
func inf seq ->  Element of ExtREAL  equals :: RINFSUP2:def 2
 inf (rng seq);
coherence
 inf (rng seq) is Element of ExtREAL ;
end;

:: deftheorem  defines sup RINFSUP2:def_1_:_
 for seq being ExtREAL_sequence holds sup seq = sup (rng seq);

:: deftheorem  defines inf RINFSUP2:def_2_:_
 for seq being ExtREAL_sequence holds inf seq = inf (rng seq);

definition
let seq be ExtREAL_sequence;
attrseq is bounded_below  means :Def3: :: RINFSUP2:def 3
 rng seq is bounded_below ;
attrseq is bounded_above  means :Def4: :: RINFSUP2:def 4
 rng seq is bounded_above ;
end;

:: deftheorem Def3 defines bounded_below RINFSUP2:def_3_:_
 for seq being ExtREAL_sequence holds
( seq is bounded_below iff rng seq is bounded_below );

:: deftheorem Def4 defines bounded_above RINFSUP2:def_4_:_
 for seq being ExtREAL_sequence holds
( seq is bounded_above iff rng seq is bounded_above );

definition
let seq be ExtREAL_sequence;
attrseq is bounded  means :Def5: :: RINFSUP2:def 5
( seq is bounded_above & seq is bounded_below );
end;

:: deftheorem Def5 defines bounded RINFSUP2:def_5_:_
 for seq being ExtREAL_sequence holds
( seq is bounded iff ( seq is bounded_above & seq is bounded_below ) );

theorem Th5: :: RINFSUP2:5
for seq being ExtREAL_sequence
for n being Element of NAT holds  {  (seq . k) where k is Element of NAT : n <= k  }  is non empty Subset of ExtREAL
proofend;

definition
let seq be ExtREAL_sequence;
func inferior_realsequence seq ->  ExtREAL_sequence means :Def6: :: RINFSUP2:def 6
 for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; it . n = inf Y );
existence
 ex b1 being ExtREAL_sequence st
for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; b1 . n = inf Y )
proofend;
uniqueness
 for b1, b2 being ExtREAL_sequence st ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; b1 . n = inf Y ) ) &amp; ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; b2 . n = inf Y ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines inferior_realsequence RINFSUP2:def_6_:_
 for seq, b2 being ExtREAL_sequence holds
( b2 = inferior_realsequence seq iff for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; b2 . n = inf Y ) );

definition
let seq be ExtREAL_sequence;
func superior_realsequence seq ->  ExtREAL_sequence means :Def7: :: RINFSUP2:def 7
 for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; it . n = sup Y );
existence
 ex b1 being ExtREAL_sequence st
for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; b1 . n = sup Y )
proofend;
uniqueness
 for b1, b2 being ExtREAL_sequence st ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; b1 . n = sup Y ) ) &amp; ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; b2 . n = sup Y ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines superior_realsequence RINFSUP2:def_7_:_
 for seq, b2 being ExtREAL_sequence holds
( b2 = superior_realsequence seq iff for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y =  {  (seq . k) where k is Element of NAT : n <= k  }  &amp; b2 . n = sup Y ) );

theorem :: RINFSUP2:6
for seq being ExtREAL_sequence st seq is real-valued holds
seq is Real_Sequence
proofend;

theorem Th7: :: RINFSUP2:7
for seq being ExtREAL_sequence holds
( ( seq is increasing implies for n, m being Element of NAT st m < n holds
seq . m < seq . n ) &amp; ( ( for n, m being Element of NAT st m < n holds
seq . m < seq . n ) implies seq is increasing ) &amp; ( seq is decreasing implies for n, m being Element of NAT st m < n holds
seq . n < seq . m ) &amp; ( ( for n, m being Element of NAT st m < n holds
seq . n < seq . m ) implies seq is decreasing ) &amp; ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) &amp; ( ( for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing ) &amp; ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) &amp; ( ( for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) implies seq is non-increasing ) )
proofend;

theorem Th8: :: RINFSUP2:8
for n being Element of NAT
for seq being ExtREAL_sequence holds
( (inferior_realsequence seq) . n <= seq . n &amp; seq . n <= (superior_realsequence seq) . n )
proofend;

Lm1:  for seq being ExtREAL_sequence holds superior_realsequence seq is non-increasing
proofend;

Lm2:  for seq being ExtREAL_sequence holds inferior_realsequence seq is non-decreasing
proofend;

registration
let seq be ExtREAL_sequence;
cluster superior_realsequence seq ->  non-increasing ;
coherence
 superior_realsequence seq is non-increasing by Lm1;
cluster inferior_realsequence seq ->  non-decreasing ;
coherence
 inferior_realsequence seq is non-decreasing by Lm2;
end;

definition
let seq be ExtREAL_sequence;
func lim_sup seq ->  Element of ExtREAL  equals :: RINFSUP2:def 8
 inf (superior_realsequence seq);
coherence
 inf (superior_realsequence seq) is Element of ExtREAL ;
func lim_inf seq ->  Element of ExtREAL  equals :: RINFSUP2:def 9
 sup (inferior_realsequence seq);
coherence
 sup (inferior_realsequence seq) is Element of ExtREAL ;
end;

:: deftheorem  defines lim_sup RINFSUP2:def_8_:_
 for seq being ExtREAL_sequence holds lim_sup seq = inf (superior_realsequence seq);

:: deftheorem  defines lim_inf RINFSUP2:def_9_:_
 for seq being ExtREAL_sequence holds lim_inf seq = sup (inferior_realsequence seq);

theorem Th9: :: RINFSUP2:9
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq &amp; rseq is bounded holds
( superior_realsequence seq = superior_realsequence rseq &amp; lim_sup seq = lim_sup rseq )
proofend;

theorem Th10: :: RINFSUP2:10
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq &amp; rseq is bounded holds
( inferior_realsequence seq = inferior_realsequence rseq &amp; lim_inf seq = lim_inf rseq )
proofend;

theorem Th11: :: RINFSUP2:11
for seq being ExtREAL_sequence st seq is bounded holds
seq is Real_Sequence
proofend;

theorem Th12: :: RINFSUP2:12
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_above iff rseq is V64() )
proofend;

theorem Th13: :: RINFSUP2:13
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_below iff rseq is V65() )
proofend;

theorem Th14: :: RINFSUP2:14
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq &amp; rseq is convergent holds
( seq is convergent_to_finite_number &amp; seq is convergent &amp; lim seq = lim rseq )
proofend;

theorem Th15: :: RINFSUP2:15
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq &amp; seq is convergent_to_finite_number holds
( rseq is convergent &amp; lim seq = lim rseq )
proofend;

theorem Th16: :: RINFSUP2:16
for k being Element of NAT
for seq being ExtREAL_sequence st seq ^\ k is convergent_to_finite_number holds
( seq is convergent_to_finite_number &amp; seq is convergent &amp; lim seq = lim (seq ^\ k) )
proofend;

theorem Th17: :: RINFSUP2:17
for k being Element of NAT
for seq being ExtREAL_sequence st seq ^\ k is convergent holds
( seq is convergent &amp; lim seq = lim (seq ^\ k) )
proofend;

theorem Th18: :: RINFSUP2:18
for seq being ExtREAL_sequence st lim_sup seq = lim_inf seq &amp; lim_inf seq in REAL holds
ex k being Element of NAT st seq ^\ k is bounded
proofend;

theorem Th19: :: RINFSUP2:19
for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds
ex k being Element of NAT st seq ^\ k is bounded
proofend;

theorem Th20: :: RINFSUP2:20
for k being Element of NAT
for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds
( seq ^\ k is convergent_to_finite_number &amp; seq ^\ k is convergent &amp; lim seq = lim (seq ^\ k) )
proofend;

theorem :: RINFSUP2:21
for k being Element of NAT
for seq being ExtREAL_sequence st seq is convergent holds
( seq ^\ k is convergent &amp; lim seq = lim (seq ^\ k) )
proofend;

theorem :: RINFSUP2:22
for k being Element of NAT
for seq being ExtREAL_sequence holds
( ( seq is bounded_above implies seq ^\ k is bounded_above ) &amp; ( seq is bounded_below implies seq ^\ k is bounded_below ) )
proofend;

theorem Th23: :: RINFSUP2:23
for n being Element of NAT
for seq being ExtREAL_sequence holds
( inf seq <= seq . n &amp; seq . n <= sup seq )
proofend;

theorem Th24: :: RINFSUP2:24
for seq being ExtREAL_sequence holds inf seq <= sup seq
proofend;

theorem Th25: :: RINFSUP2:25
for k being Element of NAT
for seq being ExtREAL_sequence st seq is non-increasing holds
( seq ^\ k is non-increasing &amp; inf seq = inf (seq ^\ k) )
proofend;

theorem Th26: :: RINFSUP2:26
for k being Element of NAT
for seq being ExtREAL_sequence st seq is non-decreasing holds
( seq ^\ k is non-decreasing &amp; sup seq = sup (seq ^\ k) )
proofend;

theorem :: RINFSUP2:27
for n being Element of NAT
for seq being ExtREAL_sequence holds
( (superior_realsequence seq) . n = sup (seq ^\ n) &amp; (inferior_realsequence seq) . n = inf (seq ^\ n) )
proofend;

theorem Th28: :: RINFSUP2:28
for seq being ExtREAL_sequence
for j being Element of NAT holds
( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j &amp; lim_sup (seq ^\ j) = lim_sup seq )
proofend;

theorem Th29: :: RINFSUP2:29
for seq being ExtREAL_sequence
for j being Element of NAT holds
( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j &amp; lim_inf (seq ^\ j) = lim_inf seq )
proofend;

theorem Th30: :: RINFSUP2:30
for seq being ExtREAL_sequence
for k being Element of NAT st seq is non-increasing &amp; -infty < seq . k &amp; seq . k < +infty holds
( seq ^\ k is bounded_above &amp; sup (seq ^\ k) = seq . k )
proofend;

theorem Th31: :: RINFSUP2:31
for seq being ExtREAL_sequence
for k being Element of NAT st seq is non-decreasing &amp; -infty < seq . k &amp; seq . k < +infty holds
( seq ^\ k is bounded_below &amp; inf (seq ^\ k) = seq . k )
proofend;

Lm3:  for seq being ExtREAL_sequence st seq is bounded &amp; seq is non-increasing holds
( seq is convergent_to_finite_number &amp; seq is convergent &amp; lim seq = inf seq )
proofend;

Lm4:  for seq being ExtREAL_sequence st seq is bounded &amp; seq is non-decreasing holds
( seq is convergent_to_finite_number &amp; seq is convergent &amp; lim seq = sup seq )
proofend;

theorem Th32: :: RINFSUP2:32
for seq being ExtREAL_sequence st ( for n being Element of NAT holds +infty <= seq . n ) holds
seq is convergent_to_+infty
proofend;

theorem Th33: :: RINFSUP2:33
for seq being ExtREAL_sequence st ( for n being Element of NAT holds seq . n <= -infty ) holds
seq is convergent_to_-infty
proofend;

theorem Th34: :: RINFSUP2:34
for seq being ExtREAL_sequence st seq is non-increasing &amp; -infty = inf seq holds
( seq is convergent_to_-infty &amp; lim seq = -infty )
proofend;

theorem Th35: :: RINFSUP2:35
for seq being ExtREAL_sequence st seq is non-decreasing &amp; +infty = sup seq holds
( seq is convergent_to_+infty &amp; lim seq = +infty )
proofend;

theorem Th36: :: RINFSUP2:36
for seq being ExtREAL_sequence st seq is non-increasing holds
( seq is convergent &amp; lim seq = inf seq )
proofend;

theorem Th37: :: RINFSUP2:37
for seq being ExtREAL_sequence st seq is non-decreasing holds
( seq is convergent &amp; lim seq = sup seq )
proofend;

theorem Th38: :: RINFSUP2:38
for seq1, seq2 being ExtREAL_sequence st seq1 is convergent &amp; seq2 is convergent &amp; ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds
lim seq1 <= lim seq2
proofend;

theorem :: RINFSUP2:39
for seq being ExtREAL_sequence holds lim_inf seq <= lim_sup seq
proofend;

Lm5:  for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq &amp; lim_inf seq = +infty holds
( seq is convergent &amp; lim seq = lim_inf seq &amp; lim seq = lim_sup seq )
proofend;

Lm6:  for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq &amp; lim_inf seq = -infty holds
( seq is convergent &amp; lim seq = lim_inf seq &amp; lim seq = lim_sup seq )
proofend;

Lm7:  for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq &amp; lim_inf seq in REAL holds
( seq is convergent &amp; lim seq = lim_inf seq &amp; lim seq = lim_sup seq )
proofend;

theorem Th40: :: RINFSUP2:40
for seq being ExtREAL_sequence holds
( seq is convergent iff lim_inf seq = lim_sup seq )
proofend;

theorem :: RINFSUP2:41
for seq being ExtREAL_sequence st seq is convergent holds
( lim seq = lim_inf seq &amp; lim seq = lim_sup seq )
proofend;