let seq be ExtREAL_sequence; :: thesis: ( seq is non-increasing implies ( seq is convergent & lim seq = inf seq ) )
assume A1: seq is non-increasing ; :: thesis: ( seq is convergent & lim seq = inf seq )
per cases ( for n being Element of NAT holds +infty <= seq . n or ex n being Element of NAT st not +infty <= seq . n ) ;
suppose A2: for n being Element of NAT holds +infty <= seq . n ; :: thesis: ( seq is convergent & lim seq = inf seq )
now :: thesis: for y being object st y in holds
y in rng seq
let y be object ; :: thesis: ( y in implies y in rng seq )
assume y in ; :: thesis: y in rng seq
then A3: y = +infty by TARSKI:def 1;
now :: thesis: y in rng seq
assume A4: not y in rng seq ; :: thesis: contradiction
now :: thesis: for n being Element of NAT holds contradictionend;
hence contradiction ; :: thesis: verum
end;
hence y in rng seq ; :: thesis: verum
end;
then A5: {+infty} c= rng seq ;
A6: seq is convergent_to_+infty by ;
hence A7: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = inf seq
now :: thesis: for y being object st y in rng seq holds
y in
let y be object ; :: thesis: ( y in rng seq implies y in )
assume y in rng seq ; :: thesis:
then ex x being object st
( x in dom seq & seq . x = y ) by FUNCT_1:def 3;
then y = +infty by ;
hence y in by TARSKI:def 1; :: thesis: verum
end;
then rng seq c= ;
then rng seq = by ;
then inf seq = +infty by XXREAL_2:13;
hence lim seq = inf seq by ; :: thesis: verum
end;
suppose not for n being Element of NAT holds +infty <= seq . n ; :: thesis: ( seq is convergent & lim seq = inf seq )
then consider k being Element of NAT such that
A8: seq . k < +infty ;
per cases ( -infty <> inf seq or -infty = inf seq ) ;
suppose A9: -infty <> inf seq ; :: thesis: ( seq is convergent & lim seq = inf seq )
set seq0 = seq ^\ k;
A10: inf seq = inf (seq ^\ k) by ;
A11: now :: thesis: not rng (seq ^\ k) = end;
A13: inf (seq ^\ k) <= sup (seq ^\ k) by Th24;
A14: inf (rng (seq ^\ k)) is LowerBound of rng (seq ^\ k) by XXREAL_2:def 4;
inf seq <= seq . k by Th23;
then -infty < seq . k by ;
then A15: seq ^\ k is bounded_above by A1, A8, Th30;
then rng (seq ^\ k) is bounded_above ;
then sup (rng (seq ^\ k)) < +infty by ;
then inf (rng (seq ^\ k)) in REAL by ;
then rng (seq ^\ k) is bounded_below by ;
then seq ^\ k is bounded_below ;
then A16: seq ^\ k is bounded by A15;
A17: seq ^\ k is non-increasing by ;
then A18: lim (seq ^\ k) = inf (seq ^\ k) by ;
seq ^\ k is convergent by ;
hence ( seq is convergent & lim seq = inf seq ) by ; :: thesis: verum
end;
end;
end;
end;