:: RINFSUP2 semantic presentation
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 )
proof
let X be non empty Subset of ExtREAL; ::_thesis: 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 )
let Y be non empty Subset of REAL; ::_thesis: ( X = Y & Y is bounded_above implies ( X is bounded_above & sup X = upper_bound Y ) )
assume that
A1: X = Y and
A2: Y is bounded_above ; ::_thesis: ( X is bounded_above & sup X = upper_bound Y )
A3: for s being real number st s in Y holds
s <= sup X by A1, XXREAL_2:4;
not -infty in X by A1;
then A4: X <> {-infty} by TARSKI:def_1;
for r being ext-real number st r in X holds
r <= upper_bound Y by A1, A2, SEQ_4:def_1;
then A5: upper_bound Y is UpperBound of X by XXREAL_2:def_1;
hence X is bounded_above by XXREAL_2:def_10; ::_thesis: sup X = upper_bound Y
then sup X in REAL by A4, XXREAL_2:57;
then A6: upper_bound Y <= sup X by A3, SEQ_4:45;
sup X <= upper_bound Y by A5, XXREAL_2:def_3;
hence sup X = upper_bound Y by A6, XXREAL_0:1; ::_thesis: verum
end;
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 )
proof
let X be non empty Subset of ExtREAL; ::_thesis: 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 )
let Y be non empty Subset of REAL; ::_thesis: ( X = Y & Y is bounded_below implies ( X is bounded_below & inf X = lower_bound Y ) )
assume that
A1: X = Y and
A2: Y is bounded_below ; ::_thesis: ( X is bounded_below & inf X = lower_bound Y )
A3: for s being real number st s in Y holds
inf X <= s by A1, XXREAL_2:3;
not +infty in X by A1;
then A4: X <> {+infty} by TARSKI:def_1;
for r being ext-real number st r in X holds
lower_bound Y <= r by A1, A2, SEQ_4:def_2;
then A5: lower_bound Y is LowerBound of X by XXREAL_2:def_2;
hence X is bounded_below by XXREAL_2:def_9; ::_thesis: inf X = lower_bound Y
then inf X in REAL by A4, XXREAL_2:58;
then A6: inf X <= lower_bound Y by A3, SEQ_4:43;
lower_bound Y <= inf X by A5, XXREAL_2:def_4;
hence inf X = lower_bound Y by A6, XXREAL_0:1; ::_thesis: verum
end;
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
proof
let seq be ExtREAL_sequence; ::_thesis: for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL
let n be Element of NAT ; ::_thesis: { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL
deffunc H1( Element of NAT ) -> Element of ExtREAL = seq . $1;
defpred S1[ Element of NAT ] means n <= $1;
set Y = { H1(k) where k is Element of NAT : S1[k] } ;
A1: seq . n in { H1(k) where k is Element of NAT : S1[k] } ;
{ H1(k) where k is Element of NAT : S1[k] } is Subset of ExtREAL from DOMAIN_1:sch_8();
hence { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL by A1; ::_thesis: verum
end;
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 } & 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 } & b1 . n = inf Y )
proof
defpred S1[ Element of NAT , Element of ExtREAL ] means ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : $1 <= k } & $2 = inf Y );
A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S1[n,y]
reconsider Y = { (seq . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by Th5;
reconsider y = inf Y as Element of ExtREAL ;
take y ; ::_thesis: S1[n,y]
thus S1[n,y] ; ::_thesis: verum
end;
thus ex f being Function of NAT,ExtREAL st
for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1); ::_thesis: verum
end;
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 } & b1 . n = inf Y ) ) & ( 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 } & b2 . n = inf Y ) ) holds
b1 = b2
proof
let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( 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 } & seq1 . n = inf Y ) ) & ( 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 } & seq2 . n = inf Y ) ) implies seq1 = seq2 )
assume that
A2: 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 } & seq1 . n = inf Y ) and
A3: 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 } & seq2 . n = inf Y ) ; ::_thesis: seq1 = seq2
A4: for y being set st y in NAT holds
seq1 . y = seq2 . y
proof
let y be set ; ::_thesis: ( y in NAT implies seq1 . y = seq2 . y )
assume y in NAT ; ::_thesis: seq1 . y = seq2 . y
then reconsider n = y as Element of NAT ;
A5: ex Z being non empty Subset of ExtREAL st
( Z = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = inf Z ) by A3;
ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = inf Y ) by A2;
hence seq1 . y = seq2 . y by A5; ::_thesis: verum
end;
A6: NAT = dom seq2 by FUNCT_2:def_1;
NAT = dom seq1 by FUNCT_2:def_1;
hence seq1 = seq2 by A4, A6, FUNCT_1:2; ::_thesis: verum
end;
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 } & 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 } & 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 } & b1 . n = sup Y )
proof
defpred S1[ Element of NAT , Element of ExtREAL ] means ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : $1 <= k } & $2 = sup Y );
A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S1[n,y]
reconsider Y = { (seq . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by Th5;
reconsider y = sup Y as Element of ExtREAL ;
take y ; ::_thesis: S1[n,y]
thus S1[n,y] ; ::_thesis: verum
end;
thus ex f being Function of NAT,ExtREAL st
for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1); ::_thesis: verum
end;
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 } & b1 . n = sup Y ) ) & ( 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 } & b2 . n = sup Y ) ) holds
b1 = b2
proof
let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( 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 } & seq1 . n = sup Y ) ) & ( 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 } & seq2 . n = sup Y ) ) implies seq1 = seq2 )
assume that
A2: 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 } & seq1 . n = sup Y ) and
A3: for m being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : m <= k } & seq2 . m = sup Y ) ; ::_thesis: seq1 = seq2
A4: for y being set st y in NAT holds
seq1 . y = seq2 . y
proof
let y be set ; ::_thesis: ( y in NAT implies seq1 . y = seq2 . y )
assume y in NAT ; ::_thesis: seq1 . y = seq2 . y
then reconsider n = y as Element of NAT ;
A5: ex Z being non empty Subset of ExtREAL st
( Z = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = sup Z ) by A3;
ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = sup Y ) by A2;
hence seq1 . y = seq2 . y by A5; ::_thesis: verum
end;
A6: NAT = dom seq2 by FUNCT_2:def_1;
NAT = dom seq1 by FUNCT_2:def_1;
hence seq1 = seq2 by A4, A6, FUNCT_1:2; ::_thesis: verum
end;
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 } & b2 . n = sup Y ) );
theorem :: RINFSUP2:6
for seq being ExtREAL_sequence st seq is real-valued holds
seq is Real_Sequence
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is real-valued implies seq is Real_Sequence )
assume seq is real-valued ; ::_thesis: seq is Real_Sequence
then rng seq is Subset of REAL by MESFUNC2:32;
hence seq is Real_Sequence by FUNCT_2:6; ::_thesis: verum
end;
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 ) & ( ( for n, m being Element of NAT st m < n holds
seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds
seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) implies seq is non-increasing ) )
proof
let seq be ExtREAL_sequence; ::_thesis: ( ( seq is increasing implies for n, m being Element of NAT st m < n holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st m < n holds
seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds
seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) implies seq is non-increasing ) )
A1: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m < seq . n ) implies seq is increasing )
proof
assume A2: for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m < seq . n ; ::_thesis: seq is increasing
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for b1 being set holds
( not e1 in K86(seq) or not b1 in K86(seq) or b1 <= e1 or not K68(seq,b1) <= K68(seq,e1) )
let e2 be ext-real number ; ::_thesis: ( not e1 in K86(seq) or not e2 in K86(seq) or e2 <= e1 or not K68(seq,e2) <= K68(seq,e1) )
thus ( not e1 in K86(seq) or not e2 in K86(seq) or e2 <= e1 or not K68(seq,e2) <= K68(seq,e1) ) by A2; ::_thesis: verum
end;
A3: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m > seq . n ) implies seq is decreasing )
proof
assume A4: for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m > seq . n ; ::_thesis: seq is decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for b1 being set holds
( not e1 in K86(seq) or not b1 in K86(seq) or b1 <= e1 or not K68(seq,e1) <= K68(seq,b1) )
let e2 be ext-real number ; ::_thesis: ( not e1 in K86(seq) or not e2 in K86(seq) or e2 <= e1 or not K68(seq,e1) <= K68(seq,e2) )
thus ( not e1 in K86(seq) or not e2 in K86(seq) or e2 <= e1 or not K68(seq,e1) <= K68(seq,e2) ) by A4; ::_thesis: verum
end;
A5: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing )
proof
assume A6: for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m <= seq . n ; ::_thesis: seq is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for b1 being set holds
( not e1 in K86(seq) or not b1 in K86(seq) or not e1 <= b1 or K68(seq,e1) <= K68(seq,b1) )
let e2 be ext-real number ; ::_thesis: ( not e1 in K86(seq) or not e2 in K86(seq) or not e1 <= e2 or K68(seq,e1) <= K68(seq,e2) )
thus ( not e1 in K86(seq) or not e2 in K86(seq) or not e1 <= e2 or K68(seq,e1) <= K68(seq,e2) ) by A6; ::_thesis: verum
end;
A7: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m >= seq . n ) implies seq is non-increasing )
proof
assume A8: for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m >= seq . n ; ::_thesis: seq is non-increasing
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for b1 being set holds
( not e1 in K86(seq) or not b1 in K86(seq) or not e1 <= b1 or K68(seq,b1) <= K68(seq,e1) )
let e2 be ext-real number ; ::_thesis: ( not e1 in K86(seq) or not e2 in K86(seq) or not e1 <= e2 or K68(seq,e2) <= K68(seq,e1) )
thus ( not e1 in K86(seq) or not e2 in K86(seq) or not e1 <= e2 or K68(seq,e2) <= K68(seq,e1) ) by A8; ::_thesis: verum
end;
dom seq = NAT by FUNCT_2:def_1;
hence ( ( seq is increasing implies for n, m being Element of NAT st m < n holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st m < n holds
seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds
seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) implies seq is non-increasing ) ) by A1, A3, A7, A5, VALUED_0:def_13, VALUED_0:def_14, VALUED_0:def_15, VALUED_0:def_16; ::_thesis: verum
end;
theorem Th8: :: RINFSUP2:8
for n being Element of NAT
for seq being ExtREAL_sequence holds
( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )
proof
let n be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence holds
( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )
let seq be ExtREAL_sequence; ::_thesis: ( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )
consider Y being non empty Subset of ExtREAL such that
A1: Y = { (seq . k) where k is Element of NAT : n <= k } and
A2: (inferior_realsequence seq) . n = inf Y by Def6;
A3: seq . n in Y by A1;
hence (inferior_realsequence seq) . n <= seq . n by A2, XXREAL_2:3; ::_thesis: seq . n <= (superior_realsequence seq) . n
ex Z being non empty Subset of ExtREAL st
( Z = { (seq . k) where k is Element of NAT : n <= k } & (superior_realsequence seq) . n = sup Z ) by Def7;
hence seq . n <= (superior_realsequence seq) . n by A1, A3, XXREAL_2:4; ::_thesis: verum
end;
Lm1: for seq being ExtREAL_sequence holds superior_realsequence seq is non-increasing
proof
let seq be ExtREAL_sequence; ::_thesis: superior_realsequence seq is non-increasing
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_
(superior_realsequence_seq)_._n_<=_(superior_realsequence_seq)_._m
let n, m be Element of NAT ; ::_thesis: ( m <= n implies (superior_realsequence seq) . n <= (superior_realsequence seq) . m )
consider Y being non empty Subset of ExtREAL such that
A1: Y = { (seq . k) where k is Element of NAT : m <= k } and
A2: (superior_realsequence seq) . m = sup Y by Def7;
consider Z being non empty Subset of ExtREAL such that
A3: Z = { (seq . k) where k is Element of NAT : n <= k } and
A4: (superior_realsequence seq) . n = sup Z by Def7;
assume A5: m <= n ; ::_thesis: (superior_realsequence seq) . n <= (superior_realsequence seq) . m
Z c= Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in Y )
assume z in Z ; ::_thesis: z in Y
then consider k being Element of NAT such that
A6: z = seq . k and
A7: n <= k by A3;
m <= k by A5, A7, XXREAL_0:2;
hence z in Y by A1, A6; ::_thesis: verum
end;
hence (superior_realsequence seq) . n <= (superior_realsequence seq) . m by A2, A4, XXREAL_2:59; ::_thesis: verum
end;
hence superior_realsequence seq is non-increasing by Th7; ::_thesis: verum
end;
Lm2: for seq being ExtREAL_sequence holds inferior_realsequence seq is non-decreasing
proof
let seq be ExtREAL_sequence; ::_thesis: inferior_realsequence seq is non-decreasing
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_
(inferior_realsequence_seq)_._m_<=_(inferior_realsequence_seq)_._n
let n, m be Element of NAT ; ::_thesis: ( m <= n implies (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n )
consider Y being non empty Subset of ExtREAL such that
A1: Y = { (seq . k) where k is Element of NAT : m <= k } and
A2: (inferior_realsequence seq) . m = inf Y by Def6;
consider Z being non empty Subset of ExtREAL such that
A3: Z = { (seq . k) where k is Element of NAT : n <= k } and
A4: (inferior_realsequence seq) . n = inf Z by Def6;
assume A5: m <= n ; ::_thesis: (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n
Z c= Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in Y )
assume z in Z ; ::_thesis: z in Y
then consider k being Element of NAT such that
A6: z = seq . k and
A7: n <= k by A3;
m <= k by A5, A7, XXREAL_0:2;
hence z in Y by A1, A6; ::_thesis: verum
end;
hence (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n by A2, A4, XXREAL_2:60; ::_thesis: verum
end;
hence inferior_realsequence seq is non-decreasing by Th7; ::_thesis: verum
end;
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 & rseq is bounded holds
( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq )
proof
let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq & rseq is bounded holds
( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq )
let rseq be Real_Sequence; ::_thesis: ( seq = rseq & rseq is bounded implies ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) )
assume that
A1: seq = rseq and
A2: rseq is bounded ; ::_thesis: ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq )
A3: NAT = dom (superior_realsequence rseq) by FUNCT_2:def_1;
A4: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
(superior_realsequence_seq)_._x_=_(superior_realsequence_rseq)_._x
let x be set ; ::_thesis: ( x in NAT implies (superior_realsequence seq) . x = (superior_realsequence rseq) . x )
assume x in NAT ; ::_thesis: (superior_realsequence seq) . x = (superior_realsequence rseq) . x
then reconsider n = x as Element of NAT ;
now__::_thesis:_for_x_being_set_st_x_in__{__(rseq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in_REAL
let x be set ; ::_thesis: ( x in { (rseq . k) where k is Element of NAT : n <= k } implies x in REAL )
assume x in { (rseq . k) where k is Element of NAT : n <= k } ; ::_thesis: x in REAL
then ex k being Element of NAT st
( x = rseq . k & n <= k ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider Y2 = { (rseq . k) where k is Element of NAT : n <= k } as Subset of REAL by TARSKI:def_3;
A5: Y2 is bounded_above by A2, RINFSUP1:31;
ex Y1 being non empty Subset of ExtREAL st
( Y1 = { (seq . k) where k is Element of NAT : n <= k } & (superior_realsequence seq) . n = sup Y1 ) by Def7;
then (superior_realsequence seq) . x = upper_bound Y2 by A1, A5, Th1;
hence (superior_realsequence seq) . x = (superior_realsequence rseq) . x by RINFSUP1:def_5; ::_thesis: verum
end;
superior_realsequence rseq is bounded by A2, RINFSUP1:56;
then A6: rng (superior_realsequence rseq) is bounded_below by RINFSUP1:6;
NAT = dom (superior_realsequence seq) by FUNCT_2:def_1;
then superior_realsequence seq = superior_realsequence rseq by A4, A3, FUNCT_1:2;
hence ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) by A6, Th3; ::_thesis: verum
end;
theorem Th10: :: RINFSUP2:10
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & rseq is bounded holds
( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq )
proof
let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq & rseq is bounded holds
( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq )
let rseq be Real_Sequence; ::_thesis: ( seq = rseq & rseq is bounded implies ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) )
assume that
A1: seq = rseq and
A2: rseq is bounded ; ::_thesis: ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq )
A3: NAT = dom (inferior_realsequence rseq) by FUNCT_2:def_1;
A4: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
(inferior_realsequence_seq)_._x_=_(inferior_realsequence_rseq)_._x
let x be set ; ::_thesis: ( x in NAT implies (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x )
assume x in NAT ; ::_thesis: (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x
then reconsider n = x as Element of NAT ;
consider Y1 being non empty Subset of ExtREAL such that
A5: Y1 = { (seq . k) where k is Element of NAT : n <= k } and
A6: (inferior_realsequence seq) . n = inf Y1 by Def6;
now__::_thesis:_for_x_being_set_st_x_in__{__(rseq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in_REAL
let x be set ; ::_thesis: ( x in { (rseq . k) where k is Element of NAT : n <= k } implies x in REAL )
assume x in { (rseq . k) where k is Element of NAT : n <= k } ; ::_thesis: x in REAL
then ex k being Element of NAT st
( x = rseq . k & n <= k ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider Y2 = { (rseq . k) where k is Element of NAT : n <= k } as Subset of REAL by TARSKI:def_3;
Y2 is bounded_below by A2, RINFSUP1:32;
then inf Y1 = lower_bound Y2 by A1, A5, Th3;
hence (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x by A6, RINFSUP1:def_4; ::_thesis: verum
end;
inferior_realsequence rseq is bounded by A2, RINFSUP1:56;
then A7: rng (inferior_realsequence rseq) is bounded_above by RINFSUP1:5;
NAT = dom (inferior_realsequence seq) by FUNCT_2:def_1;
then inferior_realsequence seq = inferior_realsequence rseq by A4, A3, FUNCT_1:2;
hence ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) by A7, Th1; ::_thesis: verum
end;
theorem Th11: :: RINFSUP2:11
for seq being ExtREAL_sequence st seq is bounded holds
seq is Real_Sequence
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is bounded implies seq is Real_Sequence )
assume A1: seq is bounded ; ::_thesis: seq is Real_Sequence
then seq is bounded_below by Def5;
then rng seq is bounded_below by Def3;
then consider UL being real number such that
A2: UL is LowerBound of rng seq by XXREAL_2:def_9;
A3: UL in REAL by XREAL_0:def_1;
seq is bounded_above by A1, Def5;
then rng seq is bounded_above by Def4;
then consider UB being real number such that
A4: UB is UpperBound of rng seq by XXREAL_2:def_10;
A5: UB in REAL by XREAL_0:def_1;
A6: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
seq_._x_in_REAL
let x be set ; ::_thesis: ( x in NAT implies seq . x in REAL )
assume x in NAT ; ::_thesis: seq . x in REAL
then A7: seq . x in rng seq by FUNCT_2:4;
then A8: seq . x <> -infty by A2, A3, XXREAL_0:12, XXREAL_2:def_2;
seq . x <> +infty by A5, A4, A7, XXREAL_0:9, XXREAL_2:def_1;
hence seq . x in REAL by A8, XXREAL_0:14; ::_thesis: verum
end;
dom seq = NAT by FUNCT_2:def_1;
hence seq is Real_Sequence by A6, FUNCT_2:3; ::_thesis: verum
end;
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() )
proof
let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_above iff rseq is V64() )
let rseq be Real_Sequence; ::_thesis: ( seq = rseq implies ( seq is bounded_above iff rseq is V64() ) )
assume A1: seq = rseq ; ::_thesis: ( seq is bounded_above iff rseq is V64() )
hereby ::_thesis: ( rseq is V64() implies seq is bounded_above )
assume seq is bounded_above ; ::_thesis: rseq is V64()
then rng rseq is bounded_above by A1, Def4;
then consider p being real number such that
A2: p is UpperBound of rng rseq by XXREAL_2:def_10;
A3: for y being real number st y in rng rseq holds
y <= p by A2, XXREAL_2:def_1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_rseq_._n_<_p_+_1
let n be Element of NAT ; ::_thesis: rseq . n < p + 1
rseq . n in rng rseq by FUNCT_2:4;
then 0 + (rseq . n) < 1 + p by A3, XREAL_1:8;
hence rseq . n < p + 1 ; ::_thesis: verum
end;
hence rseq is V64() by SEQ_2:def_3; ::_thesis: verum
end;
assume rseq is V64() ; ::_thesis: seq is bounded_above
then consider q being real number such that
A4: for n being Element of NAT holds rseq . n < q by SEQ_2:def_3;
now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_seq_holds_
r_<=_q
let r be ext-real number ; ::_thesis: ( r in rng seq implies r <= q )
assume r in rng seq ; ::_thesis: r <= q
then ex x being set st
( x in dom rseq & r = rseq . x ) by A1, FUNCT_1:def_3;
hence r <= q by A4; ::_thesis: verum
end;
then q is UpperBound of rng seq by XXREAL_2:def_1;
hence rng seq is bounded_above by XXREAL_2:def_10; :: according to RINFSUP2:def_4 ::_thesis: verum
end;
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() )
proof
let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_below iff rseq is V65() )
let rseq be Real_Sequence; ::_thesis: ( seq = rseq implies ( seq is bounded_below iff rseq is V65() ) )
assume A1: seq = rseq ; ::_thesis: ( seq is bounded_below iff rseq is V65() )
hereby ::_thesis: ( rseq is V65() implies seq is bounded_below )
assume seq is bounded_below ; ::_thesis: rseq is V65()
then rng rseq is bounded_below by A1, Def3;
then consider p being real number such that
A2: p is LowerBound of rng rseq by XXREAL_2:def_9;
A3: for y being real number st y in rng rseq holds
p <= y by A2, XXREAL_2:def_2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_p_-_1_<_rseq_._n
let n be Element of NAT ; ::_thesis: p - 1 < rseq . n
rseq . n in rng rseq by FUNCT_2:4;
then p - 1 < (rseq . n) - 0 by A3, XREAL_1:15;
hence p - 1 < rseq . n ; ::_thesis: verum
end;
hence rseq is V65() by SEQ_2:def_4; ::_thesis: verum
end;
assume rseq is V65() ; ::_thesis: seq is bounded_below
then consider q being real number such that
A4: for n being Element of NAT holds q < rseq . n by SEQ_2:def_4;
now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_seq_holds_
q_<=_r
let r be ext-real number ; ::_thesis: ( r in rng seq implies q <= r )
assume r in rng seq ; ::_thesis: q <= r
then ex x being set st
( x in dom rseq & r = rseq . x ) by A1, FUNCT_1:def_3;
hence q <= r by A4; ::_thesis: verum
end;
then q is LowerBound of rng seq by XXREAL_2:def_2;
hence rng seq is bounded_below by XXREAL_2:def_9; :: according to RINFSUP2:def_3 ::_thesis: verum
end;
theorem Th14: :: RINFSUP2:14
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & rseq is convergent holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq )
proof
let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq & rseq is convergent holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq )
let rseq be Real_Sequence; ::_thesis: ( seq = rseq & rseq is convergent implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) )
assume that
A1: seq = rseq and
A2: rseq is convergent ; ::_thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq )
A3: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_
ex_N_being_Nat_st_
for_m_being_Nat_st_N_<=_m_holds_
|.((seq_._m)_-_(R_EAL_(lim_rseq))).|_<_e
let e be real number ; ::_thesis: ( 0 < e implies ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - (R_EAL (lim rseq))).| < e )
assume 0 < e ; ::_thesis: ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - (R_EAL (lim rseq))).| < e
then consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
abs ((rseq . m) - (lim rseq)) < e by A2, SEQ_2:def_7;
set N = n;
now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_
|.((seq_._m)_-_(R_EAL_(lim_rseq))).|_<_e
let m be Nat; ::_thesis: ( n <= m implies |.((seq . m) - (R_EAL (lim rseq))).| < e )
A5: m is Element of NAT by ORDINAL1:def_12;
A6: (rseq . m) - (lim rseq) = (seq . m) - (R_EAL (lim rseq)) by A1, SUPINF_2:3;
assume n <= m ; ::_thesis: |.((seq . m) - (R_EAL (lim rseq))).| < e
then abs ((rseq . m) - (lim rseq)) < e by A4, A5;
hence |.((seq . m) - (R_EAL (lim rseq))).| < e by A6, EXTREAL2:1; ::_thesis: verum
end;
hence ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - (R_EAL (lim rseq))).| < e ; ::_thesis: verum
end;
then A7: seq is convergent_to_finite_number by MESFUNC5:def_8;
then seq is convergent by MESFUNC5:def_11;
hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) by A3, A7, MESFUNC5:def_12; ::_thesis: verum
end;
theorem Th15: :: RINFSUP2:15
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds
( rseq is convergent & lim seq = lim rseq )
proof
let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds
( rseq is convergent & lim seq = lim rseq )
let rseq be Real_Sequence; ::_thesis: ( seq = rseq & seq is convergent_to_finite_number implies ( rseq is convergent & lim seq = lim rseq ) )
assume that
A1: seq = rseq and
A2: seq is convergent_to_finite_number ; ::_thesis: ( rseq is convergent & lim seq = lim rseq )
A3: ( not lim seq = +infty or not seq is convergent_to_+infty ) by A2, MESFUNC5:50;
A4: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A2, MESFUNC5:51;
seq is convergent by A2, MESFUNC5:def_11;
then consider g being real number such that
A5: lim seq = g and
A6: for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p and
seq is convergent_to_finite_number by A3, A4, MESFUNC5:def_12;
A7: 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 ((rseq . m) - g) < p
proof
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - g) < p )
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - g) < p
then consider n being Nat such that
A8: for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p by A6;
reconsider N = n as Element of NAT by ORDINAL1:def_12;
take N ; ::_thesis: for m being Element of NAT st N <= m holds
abs ((rseq . m) - g) < p
hereby ::_thesis: verum
let m be Element of NAT ; ::_thesis: ( N <= m implies abs ((rseq . m) - g) < p )
assume N <= m ; ::_thesis: abs ((rseq . m) - g) < p
then A9: |.((seq . m) - (lim seq)).| < p by A8;
g is Real by XREAL_0:def_1;
then (rseq . m) - g = (seq . m) - (lim seq) by A1, A5, SUPINF_2:3;
hence abs ((rseq . m) - g) < p by A9, EXTREAL2:1; ::_thesis: verum
end;
end;
then rseq is convergent by SEQ_2:def_6;
hence ( rseq is convergent & lim seq = lim rseq ) by A5, A7, SEQ_2:def_7; ::_thesis: verum
end;
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 & seq is convergent & lim seq = lim (seq ^\ k) )
proof
let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq ^\ k is convergent_to_finite_number holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) )
let seq be ExtREAL_sequence; ::_thesis: ( seq ^\ k is convergent_to_finite_number implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq ^\ k is convergent_to_finite_number ; ::_thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) )
then A2: ( not lim (seq ^\ k) = +infty or not seq ^\ k is convergent_to_+infty ) by MESFUNC5:50;
A3: ( not lim (seq ^\ k) = -infty or not seq ^\ k is convergent_to_-infty ) by A1, MESFUNC5:51;
seq ^\ k is convergent by A1, MESFUNC5:def_11;
then A4: ex g being real number st
( lim (seq ^\ k) = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim (seq ^\ k))).| < p ) & seq ^\ k is convergent_to_finite_number ) by A2, A3, MESFUNC5:def_12;
then consider g being real number such that
A5: lim (seq ^\ k) = g ;
A6: for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p
proof
let p be real number ; ::_thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p )
assume 0 < p ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p
then consider n being Nat such that
A7: for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim (seq ^\ k))).| < p by A4;
take n1 = n + k; ::_thesis: for m being Nat st n1 <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p
hereby ::_thesis: verum
let m be Nat; ::_thesis: ( n1 <= m implies |.((seq . m) - (lim (seq ^\ k))).| < p )
assume A8: n1 <= m ; ::_thesis: |.((seq . m) - (lim (seq ^\ k))).| < p
k <= n + k by NAT_1:11;
then reconsider mk = m - k as Element of NAT by A8, INT_1:5, XXREAL_0:2;
A9: (seq ^\ k) . (m - k) = seq . (mk + k) by NAT_1:def_3;
(n + k) - k <= m - k by A8, XREAL_1:9;
hence |.((seq . m) - (lim (seq ^\ k))).| < p by A7, A9; ::_thesis: verum
end;
end;
lim (seq ^\ k) = R_EAL g by A5;
hence A10: seq is convergent_to_finite_number by A6, MESFUNC5:def_8; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )
hence seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k)
hence lim seq = lim (seq ^\ k) by A5, A6, A10, MESFUNC5:def_12; ::_thesis: verum
end;
theorem Th17: :: RINFSUP2:17
for k being Element of NAT
for seq being ExtREAL_sequence st seq ^\ k is convergent holds
( seq is convergent & lim seq = lim (seq ^\ k) )
proof
let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq ^\ k is convergent holds
( seq is convergent & lim seq = lim (seq ^\ k) )
let seq be ExtREAL_sequence; ::_thesis: ( seq ^\ k is convergent implies ( seq is convergent & lim seq = lim (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq ^\ k is convergent ; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )
percases ( seq ^\ k is convergent_to_finite_number or seq ^\ k is convergent_to_+infty or seq ^\ k is convergent_to_-infty ) by A1, MESFUNC5:def_11;
suppose seq ^\ k is convergent_to_finite_number ; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )
hence ( seq is convergent & lim seq = lim (seq ^\ k) ) by Th16; ::_thesis: verum
end;
supposeA2: seq ^\ k is convergent_to_+infty ; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )
for g being real number st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m
proof
let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m )
assume 0 < g ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m
then consider n being Nat such that
A3: for m being Nat st n <= m holds
g <= (seq ^\ k) . m by A2, MESFUNC5:def_9;
take n1 = n + k; ::_thesis: for m being Nat st n1 <= m holds
g <= seq . m
hereby ::_thesis: verum
let m be Nat; ::_thesis: ( n1 <= m implies g <= seq . m )
assume A4: n1 <= m ; ::_thesis: g <= seq . m
k <= n + k by NAT_1:11;
then reconsider mk = m - k as Element of NAT by A4, INT_1:5, XXREAL_0:2;
A5: (seq ^\ k) . (m - k) = seq . (mk + k) by NAT_1:def_3;
(n + k) - k <= m - k by A4, XREAL_1:9;
hence g <= seq . m by A3, A5; ::_thesis: verum
end;
end;
then A6: seq is convergent_to_+infty by MESFUNC5:def_9;
hence A7: seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k)
lim (seq ^\ k) = +infty by A1, A2, MESFUNC5:def_12;
hence lim seq = lim (seq ^\ k) by A6, A7, MESFUNC5:def_12; ::_thesis: verum
end;
supposeA8: seq ^\ k is convergent_to_-infty ; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )
for g being real number st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g
proof
let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g )
assume g < 0 ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g
then consider n being Nat such that
A9: for m being Nat st n <= m holds
(seq ^\ k) . m <= g by A8, MESFUNC5:def_10;
take n1 = n + k; ::_thesis: for m being Nat st n1 <= m holds
seq . m <= g
hereby ::_thesis: verum
let m be Nat; ::_thesis: ( n1 <= m implies seq . m <= g )
assume A10: n1 <= m ; ::_thesis: seq . m <= g
k <= n + k by NAT_1:11;
then reconsider mk = m - k as Element of NAT by A10, INT_1:5, XXREAL_0:2;
A11: (seq ^\ k) . (m - k) = seq . (mk + k) by NAT_1:def_3;
(n + k) - k <= m - k by A10, XREAL_1:9;
hence seq . m <= g by A9, A11; ::_thesis: verum
end;
end;
then A12: seq is convergent_to_-infty by MESFUNC5:def_10;
hence A13: seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k)
lim (seq ^\ k) = -infty by A1, A8, MESFUNC5:def_12;
hence lim seq = lim (seq ^\ k) by A12, A13, MESFUNC5:def_12; ::_thesis: verum
end;
end;
end;
theorem Th18: :: RINFSUP2:18
for seq being ExtREAL_sequence st lim_sup seq = lim_inf seq & lim_inf seq in REAL holds
ex k being Element of NAT st seq ^\ k is bounded
proof
let seq be ExtREAL_sequence; ::_thesis: ( lim_sup seq = lim_inf seq & lim_inf seq in REAL implies ex k being Element of NAT st seq ^\ k is bounded )
assume that
A1: lim_sup seq = lim_inf seq and
A2: lim_inf seq in REAL ; ::_thesis: ex k being Element of NAT st seq ^\ k is bounded
reconsider a = lim_inf seq as Real by A2;
set K1 = a + 1;
ex k1 being Element of NAT st (superior_realsequence seq) . k1 <= a + 1
proof
assume A3: for k1 being Element of NAT holds not (superior_realsequence seq) . k1 <= a + 1 ; ::_thesis: contradiction
now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_(superior_realsequence_seq)_holds_
a_+_1_<=_x
let x be ext-real number ; ::_thesis: ( x in rng (superior_realsequence seq) implies a + 1 <= x )
assume x in rng (superior_realsequence seq) ; ::_thesis: a + 1 <= x
then ex n being set st
( n in dom (superior_realsequence seq) & x = (superior_realsequence seq) . n ) by FUNCT_1:def_3;
hence a + 1 <= x by A3; ::_thesis: verum
end;
then a + 1 is LowerBound of rng (superior_realsequence seq) by XXREAL_2:def_2;
then a + 1 <= a by A1, XXREAL_2:def_4;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
then consider k1 being Element of NAT such that
A4: (superior_realsequence seq) . k1 <= a + 1 ;
set K2 = a - 1;
ex k2 being Element of NAT st a - 1 <= (inferior_realsequence seq) . k2
proof
assume A5: for k2 being Element of NAT holds not a - 1 <= (inferior_realsequence seq) . k2 ; ::_thesis: contradiction
now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_(inferior_realsequence_seq)_holds_
x_<=_a_-_1
let x be ext-real number ; ::_thesis: ( x in rng (inferior_realsequence seq) implies x <= a - 1 )
assume x in rng (inferior_realsequence seq) ; ::_thesis: x <= a - 1
then ex n being set st
( n in dom (inferior_realsequence seq) & x = (inferior_realsequence seq) . n ) by FUNCT_1:def_3;
hence x <= a - 1 by A5; ::_thesis: verum
end;
then a - 1 is UpperBound of rng (inferior_realsequence seq) by XXREAL_2:def_1;
then a <= a - 1 by XXREAL_2:def_3;
then a + 0 < (a - 1) + 1 by XREAL_1:8;
hence contradiction ; ::_thesis: verum
end;
then consider k2 being Element of NAT such that
A6: a - 1 <= (inferior_realsequence seq) . k2 ;
take k = max (k1,k2); ::_thesis: seq ^\ k is bounded
k2 <= k by XXREAL_0:25;
then (inferior_realsequence seq) . k2 <= (inferior_realsequence seq) . k by Th7;
then A7: a - 1 <= (inferior_realsequence seq) . k by A6, XXREAL_0:2;
k1 <= k by XXREAL_0:25;
then (superior_realsequence seq) . k <= (superior_realsequence seq) . k1 by Th7;
then A8: (superior_realsequence seq) . k <= a + 1 by A4, XXREAL_0:2;
A9: for n being Element of NAT st k <= n holds
( seq . n <= a + 1 & a - 1 <= seq . n )
proof
let n be Element of NAT ; ::_thesis: ( k <= n implies ( seq . n <= a + 1 & a - 1 <= seq . n ) )
A10: (inferior_realsequence seq) . n <= seq . n by Th8;
assume A11: k <= n ; ::_thesis: ( seq . n <= a + 1 & a - 1 <= seq . n )
then (superior_realsequence seq) . n <= (superior_realsequence seq) . k by Th7;
then A12: (superior_realsequence seq) . n <= a + 1 by A8, XXREAL_0:2;
(inferior_realsequence seq) . k <= (inferior_realsequence seq) . n by A11, Th7;
then A13: a - 1 <= (inferior_realsequence seq) . n by A7, XXREAL_0:2;
seq . n <= (superior_realsequence seq) . n by Th8;
hence ( seq . n <= a + 1 & a - 1 <= seq . n ) by A12, A13, A10, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_(seq_^\_k)_holds_
x_<=_a_+_1
let x be ext-real number ; ::_thesis: ( x in rng (seq ^\ k) implies x <= a + 1 )
assume x in rng (seq ^\ k) ; ::_thesis: x <= a + 1
then consider n being set such that
A14: n in dom (seq ^\ k) and
A15: x = (seq ^\ k) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A14;
A16: k <= n + k by NAT_1:11;
x = seq . (n + k) by A15, NAT_1:def_3;
hence x <= a + 1 by A9, A16; ::_thesis: verum
end;
then a + 1 is UpperBound of rng (seq ^\ k) by XXREAL_2:def_1;
hence rng (seq ^\ k) is bounded_above by XXREAL_2:def_10; :: according to RINFSUP2:def_4,RINFSUP2:def_5 ::_thesis: seq ^\ k is bounded_below
now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_(seq_^\_k)_holds_
a_-_1_<=_x
let x be ext-real number ; ::_thesis: ( x in rng (seq ^\ k) implies a - 1 <= x )
assume x in rng (seq ^\ k) ; ::_thesis: a - 1 <= x
then consider n being set such that
A17: n in dom (seq ^\ k) and
A18: x = (seq ^\ k) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A17;
A19: k <= n + k by NAT_1:11;
x = seq . (n + k) by A18, NAT_1:def_3;
hence a - 1 <= x by A9, A19; ::_thesis: verum
end;
then a - 1 is LowerBound of rng (seq ^\ k) by XXREAL_2:def_2;
hence rng (seq ^\ k) is bounded_below by XXREAL_2:def_9; :: according to RINFSUP2:def_3 ::_thesis: verum
end;
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
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent_to_finite_number implies ex k being Element of NAT st seq ^\ k is bounded )
assume A1: seq is convergent_to_finite_number ; ::_thesis: ex k being Element of NAT st seq ^\ k is bounded
then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:50;
A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:51;
seq is convergent by A1, MESFUNC5:def_11;
then A4: ex g being real number st
( lim seq = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) & seq is convergent_to_finite_number ) by A2, A3, MESFUNC5:def_12;
then consider g being real number such that
A5: lim seq = g ;
set UB = g + 1;
consider k being Nat such that
A6: for m being Nat st k <= m holds
|.((seq . m) - (lim seq)).| < 1 by A4;
reconsider K = k as Element of NAT by ORDINAL1:def_12;
take K ; ::_thesis: seq ^\ K is bounded
A7: g is Real by XREAL_0:def_1;
now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_(seq_^\_K)_holds_
r_<=_g_+_1
let r be ext-real number ; ::_thesis: ( r in rng (seq ^\ K) implies r <= g + 1 )
assume r in rng (seq ^\ K) ; ::_thesis: r <= g + 1
then consider n being set such that
A8: n in dom (seq ^\ K) and
A9: r = (seq ^\ K) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A8;
|.((seq . (n + k)) - (lim seq)).| <= 1. by A6, NAT_1:11;
then (seq . (n + k)) - (lim seq) <= 1. by EXTREAL2:12;
then ((seq . (n + k)) + (- (lim seq))) + (lim seq) <= 1. + (lim seq) by XXREAL_3:36;
then (seq . (n + k)) + ((- (lim seq)) + (lim seq)) <= 1. + (lim seq) by A5, XXREAL_3:29;
then (seq . (n + k)) + 0. <= 1. + (lim seq) by XXREAL_3:7;
then seq . (n + k) <= 1. + (lim seq) by XXREAL_3:4;
then seq . (n + k) <= g + 1 by A5, A7, SUPINF_2:1;
hence r <= g + 1 by A9, NAT_1:def_3; ::_thesis: verum
end;
then g + 1 is UpperBound of rng (seq ^\ K) by XXREAL_2:def_1;
hence rng (seq ^\ K) is bounded_above by XXREAL_2:def_10; :: according to RINFSUP2:def_4,RINFSUP2:def_5 ::_thesis: seq ^\ K is bounded_below
set UL = g - 1;
now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_(seq_^\_K)_holds_
g_-_1_<=_r
let r be ext-real number ; ::_thesis: ( r in rng (seq ^\ K) implies g - 1 <= r )
assume r in rng (seq ^\ K) ; ::_thesis: g - 1 <= r
then consider n being set such that
A10: n in dom (seq ^\ K) and
A11: r = (seq ^\ K) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A10;
|.((seq . (n + k)) - (lim seq)).| < 1 by A6, NAT_1:11;
then - 1. <= (seq . (n + k)) - (lim seq) by EXTREAL2:12;
then (- 1.) + (lim seq) <= ((seq . (n + k)) + (- (lim seq))) + (lim seq) by XXREAL_3:36;
then (- 1.) + (lim seq) <= (seq . (n + k)) + ((- (lim seq)) + (lim seq)) by A5, XXREAL_3:29;
then A12: (- 1.) + (lim seq) <= (seq . (n + k)) + 0. by XXREAL_3:7;
- 1. = - 1 by SUPINF_2:2;
then (- 1) + g = (- 1.) + (lim seq) by A5, A7, SUPINF_2:1;
then g - 1 <= seq . (n + k) by A12, XXREAL_3:4;
hence g - 1 <= r by A11, NAT_1:def_3; ::_thesis: verum
end;
then g - 1 is LowerBound of rng (seq ^\ K) by XXREAL_2:def_2;
hence rng (seq ^\ K) is bounded_below by XXREAL_2:def_9; :: according to RINFSUP2:def_3 ::_thesis: verum
end;
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 & seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
proof
let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds
( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent_to_finite_number implies ( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq is convergent_to_finite_number ; ::_thesis: ( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:50;
A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:51;
seq is convergent by A1, MESFUNC5:def_11;
then A4: ex g being real number st
( lim seq = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) & seq is convergent_to_finite_number ) by A2, A3, MESFUNC5:def_12;
then consider g being real number such that
A5: lim seq = g ;
A6: for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim seq)).| < p
proof
let p be real number ; ::_thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim seq)).| < p )
assume 0 < p ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim seq)).| < p
then consider n being Nat such that
A7: for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p by A4;
take n ; ::_thesis: for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim seq)).| < p
hereby ::_thesis: verum
let m be Nat; ::_thesis: ( n <= m implies |.(((seq ^\ k) . m) - (lim seq)).| < p )
assume A8: n <= m ; ::_thesis: |.(((seq ^\ k) . m) - (lim seq)).| < p
m <= m + k by NAT_1:11;
then n <= m + k by A8, XXREAL_0:2;
then |.((seq . (m + k)) - (lim seq)).| < p by A7;
hence |.(((seq ^\ k) . m) - (lim seq)).| < p by NAT_1:def_3; ::_thesis: verum
end;
end;
lim seq = R_EAL g by A5;
hence A9: seq ^\ k is convergent_to_finite_number by A6, MESFUNC5:def_8; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
hence seq ^\ k is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k)
hence lim seq = lim (seq ^\ k) by A5, A6, A9, MESFUNC5:def_12; ::_thesis: verum
end;
theorem :: RINFSUP2:21
for k being Element of NAT
for seq being ExtREAL_sequence st seq is convergent holds
( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
proof
let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq is convergent holds
( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent implies ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq is convergent ; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
percases ( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty ) by A1, MESFUNC5:def_11;
suppose seq is convergent_to_finite_number ; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
hence ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) by Th20; ::_thesis: verum
end;
supposeA2: seq is convergent_to_+infty ; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
for g being real number st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= (seq ^\ k) . m
proof
let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= (seq ^\ k) . m )
assume 0 < g ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= (seq ^\ k) . m
then consider n being Nat such that
A3: for m being Nat st n <= m holds
g <= seq . m by A2, MESFUNC5:def_9;
take n ; ::_thesis: for m being Nat st n <= m holds
g <= (seq ^\ k) . m
hereby ::_thesis: verum
let m be Nat; ::_thesis: ( n <= m implies g <= (seq ^\ k) . m )
assume A4: n <= m ; ::_thesis: g <= (seq ^\ k) . m
m <= m + k by NAT_1:11;
then n <= m + k by A4, XXREAL_0:2;
then g <= seq . (m + k) by A3;
hence g <= (seq ^\ k) . m by NAT_1:def_3; ::_thesis: verum
end;
end;
then A5: seq ^\ k is convergent_to_+infty by MESFUNC5:def_9;
hence A6: seq ^\ k is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k)
lim seq = +infty by A1, A2, MESFUNC5:def_12;
hence lim seq = lim (seq ^\ k) by A5, A6, MESFUNC5:def_12; ::_thesis: verum
end;
supposeA7: seq is convergent_to_-infty ; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
for g being real number st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(seq ^\ k) . m <= g
proof
let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
(seq ^\ k) . m <= g )
assume g < 0 ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
(seq ^\ k) . m <= g
then consider n being Nat such that
A8: for m being Nat st n <= m holds
seq . m <= g by A7, MESFUNC5:def_10;
take n ; ::_thesis: for m being Nat st n <= m holds
(seq ^\ k) . m <= g
hereby ::_thesis: verum
let m be Nat; ::_thesis: ( n <= m implies (seq ^\ k) . m <= g )
assume A9: n <= m ; ::_thesis: (seq ^\ k) . m <= g
m <= m + k by NAT_1:11;
then n <= m + k by A9, XXREAL_0:2;
then seq . (m + k) <= g by A8;
hence (seq ^\ k) . m <= g by NAT_1:def_3; ::_thesis: verum
end;
end;
then A10: seq ^\ k is convergent_to_-infty by MESFUNC5:def_10;
hence A11: seq ^\ k is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k)
lim seq = -infty by A1, A7, MESFUNC5:def_12;
hence lim seq = lim (seq ^\ k) by A10, A11, MESFUNC5:def_12; ::_thesis: verum
end;
end;
end;
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 ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) )
proof
let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence holds
( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) )
let seq be ExtREAL_sequence; ::_thesis: ( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) )
hereby ::_thesis: ( seq is bounded_below implies seq ^\ k is bounded_below )
assume seq is bounded_above ; ::_thesis: seq ^\ k is bounded_above
then rng seq is bounded_above by Def4;
then consider UB being real number such that
A1: UB is UpperBound of rng seq by XXREAL_2:def_10;
now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_(seq_^\_k)_holds_
r_<=_UB
let r be ext-real number ; ::_thesis: ( r in rng (seq ^\ k) implies r <= UB )
assume r in rng (seq ^\ k) ; ::_thesis: r <= UB
then consider n being set such that
A2: n in dom (seq ^\ k) and
A3: r = (seq ^\ k) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A2;
seq . (n + k) <= UB by A1, FUNCT_2:4, XXREAL_2:def_1;
hence r <= UB by A3, NAT_1:def_3; ::_thesis: verum
end;
then UB is UpperBound of rng (seq ^\ k) by XXREAL_2:def_1;
then rng (seq ^\ k) is bounded_above by XXREAL_2:def_10;
hence seq ^\ k is bounded_above by Def4; ::_thesis: verum
end;
hereby ::_thesis: verum
assume seq is bounded_below ; ::_thesis: seq ^\ k is bounded_below
then rng seq is bounded_below by Def3;
then consider UB being real number such that
A4: UB is LowerBound of rng seq by XXREAL_2:def_9;
now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_(seq_^\_k)_holds_
UB_<=_r
let r be ext-real number ; ::_thesis: ( r in rng (seq ^\ k) implies UB <= r )
assume r in rng (seq ^\ k) ; ::_thesis: UB <= r
then consider n being set such that
A5: n in dom (seq ^\ k) and
A6: r = (seq ^\ k) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A5;
seq . (n + k) in rng seq by FUNCT_2:4;
then UB <= seq . (n + k) by A4, XXREAL_2:def_2;
hence UB <= r by A6, NAT_1:def_3; ::_thesis: verum
end;
then UB is LowerBound of rng (seq ^\ k) by XXREAL_2:def_2;
then rng (seq ^\ k) is bounded_below by XXREAL_2:def_9;
hence seq ^\ k is bounded_below by Def3; ::_thesis: verum
end;
end;
theorem Th23: :: RINFSUP2:23
for n being Element of NAT
for seq being ExtREAL_sequence holds
( inf seq <= seq . n & seq . n <= sup seq )
proof
let n be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence holds
( inf seq <= seq . n & seq . n <= sup seq )
let seq be ExtREAL_sequence; ::_thesis: ( inf seq <= seq . n & seq . n <= sup seq )
A1: inf (rng seq) is LowerBound of rng seq by XXREAL_2:def_4;
A2: sup (rng seq) is UpperBound of rng seq by XXREAL_2:def_3;
seq . n in rng seq by FUNCT_2:4;
hence ( inf seq <= seq . n & seq . n <= sup seq ) by A1, A2, XXREAL_2:def_1, XXREAL_2:def_2; ::_thesis: verum
end;
theorem Th24: :: RINFSUP2:24
for seq being ExtREAL_sequence holds inf seq <= sup seq
proof
let seq be ExtREAL_sequence; ::_thesis: inf seq <= sup seq
A1: seq . 0 <= sup seq by Th23;
inf seq <= seq . 0 by Th23;
hence inf seq <= sup seq by A1, XXREAL_0:2; ::_thesis: verum
end;
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 & inf seq = inf (seq ^\ k) )
proof
let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq is non-increasing holds
( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )
let seq be ExtREAL_sequence; ::_thesis: ( seq is non-increasing implies ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq is non-increasing ; ::_thesis: ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_
(seq_^\_k)_._n_<=_(seq_^\_k)_._m
let n, m be Element of NAT ; ::_thesis: ( m <= n implies (seq ^\ k) . n <= (seq ^\ k) . m )
assume m <= n ; ::_thesis: (seq ^\ k) . n <= (seq ^\ k) . m
then k + m <= k + n by XREAL_1:6;
then seq . (k + n) <= seq . (k + m) by A1, Th7;
then (seq ^\ k) . n <= seq . (k + m) by NAT_1:def_3;
hence (seq ^\ k) . n <= (seq ^\ k) . m by NAT_1:def_3; ::_thesis: verum
end;
hence seq ^\ k is non-increasing by Th7; ::_thesis: inf seq = inf (seq ^\ k)
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_seq_holds_
inf_(rng_(seq_^\_k))_<=_y
let y be ext-real number ; ::_thesis: ( y in rng seq implies inf (rng (seq ^\ k)) <= y )
assume y in rng seq ; ::_thesis: inf (rng (seq ^\ k)) <= y
then consider n being set such that
A2: n in dom seq and
A3: y = seq . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A2;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def_3;
then A4: inf (seq ^\ k) <= seq . (n + k) by Th23;
n <= n + k by NAT_1:11;
then seq . (n + k) <= seq . n by A1, Th7;
hence inf (rng (seq ^\ k)) <= y by A3, A4, XXREAL_0:2; ::_thesis: verum
end;
then inf (rng (seq ^\ k)) is LowerBound of rng seq by XXREAL_2:def_2;
then A5: inf (rng (seq ^\ k)) <= inf (rng seq) by XXREAL_2:def_4;
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(seq_^\_k)_holds_
inf_(rng_seq)_<=_y
let y be ext-real number ; ::_thesis: ( y in rng (seq ^\ k) implies inf (rng seq) <= y )
assume y in rng (seq ^\ k) ; ::_thesis: inf (rng seq) <= y
then consider n being set such that
A6: n in dom (seq ^\ k) and
A7: y = (seq ^\ k) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A6;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def_3;
then inf seq <= (seq ^\ k) . n by Th23;
hence inf (rng seq) <= y by A7; ::_thesis: verum
end;
then inf (rng seq) is LowerBound of rng (seq ^\ k) by XXREAL_2:def_2;
then inf (rng seq) <= inf (rng (seq ^\ k)) by XXREAL_2:def_4;
hence inf seq = inf (seq ^\ k) by A5, XXREAL_0:1; ::_thesis: verum
end;
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 & sup seq = sup (seq ^\ k) )
proof
let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq is non-decreasing holds
( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) )
let seq be ExtREAL_sequence; ::_thesis: ( seq is non-decreasing implies ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq is non-decreasing ; ::_thesis: ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) )
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_
(seq_^\_k)_._m_<=_(seq_^\_k)_._n
let n, m be Element of NAT ; ::_thesis: ( m <= n implies (seq ^\ k) . m <= (seq ^\ k) . n )
assume m <= n ; ::_thesis: (seq ^\ k) . m <= (seq ^\ k) . n
then k + m <= k + n by XREAL_1:6;
then seq . (k + m) <= seq . (k + n) by A1, Th7;
then (seq ^\ k) . m <= seq . (k + n) by NAT_1:def_3;
hence (seq ^\ k) . m <= (seq ^\ k) . n by NAT_1:def_3; ::_thesis: verum
end;
hence seq ^\ k is non-decreasing by Th7; ::_thesis: sup seq = sup (seq ^\ k)
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_seq_holds_
y_<=_sup_(rng_(seq_^\_k))
let y be ext-real number ; ::_thesis: ( y in rng seq implies y <= sup (rng (seq ^\ k)) )
assume y in rng seq ; ::_thesis: y <= sup (rng (seq ^\ k))
then consider n being set such that
A2: n in dom seq and
A3: y = seq . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A2;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def_3;
then A4: seq . (n + k) <= sup (seq ^\ k) by Th23;
n <= n + k by NAT_1:11;
then seq . n <= seq . (n + k) by A1, Th7;
hence y <= sup (rng (seq ^\ k)) by A3, A4, XXREAL_0:2; ::_thesis: verum
end;
then sup (rng (seq ^\ k)) is UpperBound of rng seq by XXREAL_2:def_1;
then A5: sup (rng seq) <= sup (rng (seq ^\ k)) by XXREAL_2:def_3;
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(seq_^\_k)_holds_
y_<=_sup_(rng_seq)
let y be ext-real number ; ::_thesis: ( y in rng (seq ^\ k) implies y <= sup (rng seq) )
assume y in rng (seq ^\ k) ; ::_thesis: y <= sup (rng seq)
then consider n being set such that
A6: n in dom (seq ^\ k) and
A7: y = (seq ^\ k) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A6;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def_3;
then (seq ^\ k) . n <= sup seq by Th23;
hence y <= sup (rng seq) by A7; ::_thesis: verum
end;
then sup (rng seq) is UpperBound of rng (seq ^\ k) by XXREAL_2:def_1;
then sup (rng (seq ^\ k)) <= sup (rng seq) by XXREAL_2:def_3;
hence sup seq = sup (seq ^\ k) by A5, XXREAL_0:1; ::_thesis: verum
end;
theorem :: RINFSUP2:27
for n being Element of NAT
for seq being ExtREAL_sequence holds
( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )
proof
let n be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence holds
( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )
let seq be ExtREAL_sequence; ::_thesis: ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )
set rseq = seq ^\ n;
A1: ex Z being non empty Subset of ExtREAL st
( Z = { (seq . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq) . n = inf Z ) by Def6;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in_rng_(seq_^\_n)
let x be set ; ::_thesis: ( x in { (seq . k) where k is Element of NAT : n <= k } implies x in rng (seq ^\ n) )
assume x in { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: x in rng (seq ^\ n)
then consider k being Element of NAT such that
A2: x = seq . k and
A3: n <= k ;
reconsider k1 = k - n as Element of NAT by A3, INT_1:5;
x = seq . (n + k1) by A2;
then x = (seq ^\ n) . k1 by NAT_1:def_3;
hence x in rng (seq ^\ n) by FUNCT_2:4; ::_thesis: verum
end;
then A4: { (seq . k) where k is Element of NAT : n <= k } c= rng (seq ^\ n) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_rng_(seq_^\_n)_holds_
x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}_
let x be set ; ::_thesis: ( x in rng (seq ^\ n) implies x in { (seq . k) where k is Element of NAT : n <= k } )
assume x in rng (seq ^\ n) ; ::_thesis: x in { (seq . k) where k is Element of NAT : n <= k }
then consider z being set such that
A5: z in dom (seq ^\ n) and
A6: x = (seq ^\ n) . z by FUNCT_1:def_3;
reconsider k0 = z as Element of NAT by A5;
A7: n <= n + k0 by NAT_1:11;
x = seq . (n + k0) by A6, NAT_1:def_3;
hence x in { (seq . k) where k is Element of NAT : n <= k } by A7; ::_thesis: verum
end;
then A8: rng (seq ^\ n) c= { (seq . k) where k is Element of NAT : n <= k } by TARSKI:def_3;
ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & (superior_realsequence seq) . n = sup Y ) by Def7;
hence ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) ) by A1, A4, A8, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th28: :: RINFSUP2:28
for seq being ExtREAL_sequence
for j being Element of NAT holds
( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq )
proof
let seq be ExtREAL_sequence; ::_thesis: for j being Element of NAT holds
( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq )
let j be Element of NAT ; ::_thesis: ( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq )
set rseq = seq ^\ j;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(superior_realsequence_(seq_^\_j))_._n_=_((superior_realsequence_seq)_^\_j)_._n
let n be Element of NAT ; ::_thesis: (superior_realsequence (seq ^\ j)) . n = ((superior_realsequence seq) ^\ j) . n
A1: ex Y2 being non empty Subset of ExtREAL st
( Y2 = { ((seq ^\ j) . k) where k is Element of NAT : n <= k } & (superior_realsequence (seq ^\ j)) . n = sup Y2 ) by Def7;
A2: ex Y3 being non empty Subset of ExtREAL st
( Y3 = { (seq . k) where k is Element of NAT : j + n <= k } & (superior_realsequence seq) . (j + n) = sup Y3 ) by Def7;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_j_+_n_<=_k__}__holds_
x_in__{__(seq_._(j_+_k2))_where_k2_is_Element_of_NAT_:_n_<=_k2__}_
let x be set ; ::_thesis: ( x in { (seq . k) where k is Element of NAT : j + n <= k } implies x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } )
assume x in { (seq . k) where k is Element of NAT : j + n <= k } ; ::_thesis: x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 }
then consider k being Element of NAT such that
A3: x = seq . k and
A4: j + n <= k ;
j <= j + n by NAT_1:11;
then reconsider k1 = k - j as Element of NAT by A4, INT_1:5, XXREAL_0:2;
A5: x = seq . (j + k1) by A3;
(j + n) - j <= k - j by A4, XREAL_1:9;
hence x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } by A5; ::_thesis: verum
end;
then A6: { (seq . k) where k is Element of NAT : j + n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._(j_+_k))_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in__{__(seq_._k1)_where_k1_is_Element_of_NAT_:_j_+_n_<=_k1__}_
let x be set ; ::_thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } )
assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; ::_thesis: x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 }
then consider k being Element of NAT such that
A7: x = seq . (j + k) and
A8: n <= k ;
j + n <= j + k by A8, XREAL_1:6;
hence x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } by A7; ::_thesis: verum
end;
then { (seq . (j + k)) where k is Element of NAT : n <= k } c= { (seq . k) where k is Element of NAT : j + n <= k } by TARSKI:def_3;
then A9: { (seq . (j + k)) where k is Element of NAT : n <= k } = { (seq . k) where k is Element of NAT : j + n <= k } by A6, XBOOLE_0:def_10;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._(j_+_k))_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in__{__((seq_^\_j)_._k1)_where_k1_is_Element_of_NAT_:_n_<=_k1__}_
let x be set ; ::_thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } )
assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; ::_thesis: x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 }
then consider k being Element of NAT such that
A10: x = seq . (j + k) and
A11: n <= k ;
x = (seq ^\ j) . k by A10, NAT_1:def_3;
hence x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } by A11; ::_thesis: verum
end;
then A12: { (seq . (j + k)) where k is Element of NAT : n <= k } c= { ((seq ^\ j) . k) where k is Element of NAT : n <= k } by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in__{__((seq_^\_j)_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in__{__(seq_._(j_+_k1))_where_k1_is_Element_of_NAT_:_n_<=_k1__}_
let x be set ; ::_thesis: ( x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } implies x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } )
assume x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } ; ::_thesis: x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 }
then consider k being Element of NAT such that
A13: x = (seq ^\ j) . k and
A14: n <= k ;
x = seq . (j + k) by A13, NAT_1:def_3;
hence x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } by A14; ::_thesis: verum
end;
then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def_3;
then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } = { (seq . (j + k)) where k is Element of NAT : n <= k } by A12, XBOOLE_0:def_10;
hence (superior_realsequence (seq ^\ j)) . n = ((superior_realsequence seq) ^\ j) . n by A1, A2, A9, NAT_1:def_3; ::_thesis: verum
end;
then (superior_realsequence seq) ^\ j = superior_realsequence (seq ^\ j) by FUNCT_2:63;
hence ( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq ) by Th25; ::_thesis: verum
end;
theorem Th29: :: RINFSUP2:29
for seq being ExtREAL_sequence
for j being Element of NAT holds
( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )
proof
let seq be ExtREAL_sequence; ::_thesis: for j being Element of NAT holds
( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )
let j be Element of NAT ; ::_thesis: ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )
set rseq = seq ^\ j;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_realsequence_(seq_^\_j))_._n_=_((inferior_realsequence_seq)_^\_j)_._n
let n be Element of NAT ; ::_thesis: (inferior_realsequence (seq ^\ j)) . n = ((inferior_realsequence seq) ^\ j) . n
A1: ex Y2 being non empty Subset of ExtREAL st
( Y2 = { ((seq ^\ j) . k) where k is Element of NAT : n <= k } & (inferior_realsequence (seq ^\ j)) . n = inf Y2 ) by Def6;
A2: ex Y3 being non empty Subset of ExtREAL st
( Y3 = { (seq . k) where k is Element of NAT : j + n <= k } & (inferior_realsequence seq) . (j + n) = inf Y3 ) by Def6;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_j_+_n_<=_k__}__holds_
x_in__{__(seq_._(j_+_k2))_where_k2_is_Element_of_NAT_:_n_<=_k2__}_
let x be set ; ::_thesis: ( x in { (seq . k) where k is Element of NAT : j + n <= k } implies x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } )
assume x in { (seq . k) where k is Element of NAT : j + n <= k } ; ::_thesis: x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 }
then consider k being Element of NAT such that
A3: x = seq . k and
A4: j + n <= k ;
j <= j + n by NAT_1:11;
then reconsider k1 = k - j as Element of NAT by A4, INT_1:5, XXREAL_0:2;
A5: x = seq . (j + k1) by A3;
(j + n) - j <= k - j by A4, XREAL_1:9;
hence x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } by A5; ::_thesis: verum
end;
then A6: { (seq . k) where k is Element of NAT : j + n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._(j_+_k))_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in__{__(seq_._k1)_where_k1_is_Element_of_NAT_:_j_+_n_<=_k1__}_
let x be set ; ::_thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } )
assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; ::_thesis: x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 }
then consider k being Element of NAT such that
A7: x = seq . (j + k) and
A8: n <= k ;
j + n <= j + k by A8, XREAL_1:6;
hence x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } by A7; ::_thesis: verum
end;
then { (seq . (j + k)) where k is Element of NAT : n <= k } c= { (seq . k) where k is Element of NAT : j + n <= k } by TARSKI:def_3;
then A9: { (seq . (j + k)) where k is Element of NAT : n <= k } = { (seq . k) where k is Element of NAT : j + n <= k } by A6, XBOOLE_0:def_10;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._(j_+_k))_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in__{__((seq_^\_j)_._k1)_where_k1_is_Element_of_NAT_:_n_<=_k1__}_
let x be set ; ::_thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } )
assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; ::_thesis: x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 }
then consider k being Element of NAT such that
A10: x = seq . (j + k) and
A11: n <= k ;
x = (seq ^\ j) . k by A10, NAT_1:def_3;
hence x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } by A11; ::_thesis: verum
end;
then A12: { (seq . (j + k)) where k is Element of NAT : n <= k } c= { ((seq ^\ j) . k) where k is Element of NAT : n <= k } by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in__{__((seq_^\_j)_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in__{__(seq_._(j_+_k1))_where_k1_is_Element_of_NAT_:_n_<=_k1__}_
let x be set ; ::_thesis: ( x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } implies x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } )
assume x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } ; ::_thesis: x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 }
then consider k being Element of NAT such that
A13: x = (seq ^\ j) . k and
A14: n <= k ;
x = seq . (j + k) by A13, NAT_1:def_3;
hence x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } by A14; ::_thesis: verum
end;
then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def_3;
then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } = { (seq . (j + k)) where k is Element of NAT : n <= k } by A12, XBOOLE_0:def_10;
hence (inferior_realsequence (seq ^\ j)) . n = ((inferior_realsequence seq) ^\ j) . n by A1, A2, A9, NAT_1:def_3; ::_thesis: verum
end;
then (inferior_realsequence seq) ^\ j = inferior_realsequence (seq ^\ j) by FUNCT_2:63;
hence ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq ) by Th26; ::_thesis: verum
end;
theorem Th30: :: RINFSUP2:30
for seq being ExtREAL_sequence
for k being Element of NAT st seq is non-increasing & -infty < seq . k & seq . k < +infty holds
( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k )
proof
let seq be ExtREAL_sequence; ::_thesis: for k being Element of NAT st seq is non-increasing & -infty < seq . k & seq . k < +infty holds
( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k )
let k be Element of NAT ; ::_thesis: ( seq is non-increasing & -infty < seq . k & seq . k < +infty implies ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) )
assume that
A1: seq is non-increasing and
A2: -infty < seq . k and
A3: seq . k < +infty ; ::_thesis: ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k )
set seq0 = seq ^\ k;
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(seq_^\_k)_holds_
y_<=_seq_._k
let y be ext-real number ; ::_thesis: ( y in rng (seq ^\ k) implies y <= seq . k )
assume y in rng (seq ^\ k) ; ::_thesis: y <= seq . k
then consider n being set such that
A4: n in dom (seq ^\ k) and
A5: y = (seq ^\ k) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A4;
k <= n + k by NAT_1:11;
then seq . (n + k) <= seq . k by A1, Th7;
hence y <= seq . k by A5, NAT_1:def_3; ::_thesis: verum
end;
then A6: seq . k is UpperBound of rng (seq ^\ k) by XXREAL_2:def_1;
(seq ^\ k) . 0 = seq . (0 + k) by NAT_1:def_3;
then A7: seq . k in rng (seq ^\ k) by FUNCT_2:4;
seq . k in REAL by A2, A3, XXREAL_0:14;
then rng (seq ^\ k) is bounded_above by A6, XXREAL_2:def_10;
hence ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) by A6, A7, Def4, XXREAL_2:55; ::_thesis: verum
end;
theorem Th31: :: RINFSUP2:31
for seq being ExtREAL_sequence
for k being Element of NAT st seq is non-decreasing & -infty < seq . k & seq . k < +infty holds
( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k )
proof
let seq be ExtREAL_sequence; ::_thesis: for k being Element of NAT st seq is non-decreasing & -infty < seq . k & seq . k < +infty holds
( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k )
let k be Element of NAT ; ::_thesis: ( seq is non-decreasing & -infty < seq . k & seq . k < +infty implies ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) )
assume that
A1: seq is non-decreasing and
A2: -infty < seq . k and
A3: seq . k < +infty ; ::_thesis: ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k )
set seq0 = seq ^\ k;
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(seq_^\_k)_holds_
seq_._k_<=_y
let y be ext-real number ; ::_thesis: ( y in rng (seq ^\ k) implies seq . k <= y )
assume y in rng (seq ^\ k) ; ::_thesis: seq . k <= y
then consider n being set such that
A4: n in dom (seq ^\ k) and
A5: y = (seq ^\ k) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A4;
k <= n + k by NAT_1:11;
then seq . k <= seq . (n + k) by A1, Th7;
hence seq . k <= y by A5, NAT_1:def_3; ::_thesis: verum
end;
then A6: seq . k is LowerBound of rng (seq ^\ k) by XXREAL_2:def_2;
(seq ^\ k) . 0 = seq . (0 + k) by NAT_1:def_3;
then A7: seq . k in rng (seq ^\ k) by FUNCT_2:4;
seq . k in REAL by A2, A3, XXREAL_0:14;
then rng (seq ^\ k) is bounded_below by A6, XXREAL_2:def_9;
hence ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) by A6, A7, Def3, XXREAL_2:56; ::_thesis: verum
end;
Lm3: for seq being ExtREAL_sequence st seq is bounded & seq is non-increasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is bounded & seq is non-increasing implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) )
assume that
A1: seq is bounded and
A2: seq is non-increasing ; ::_thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq )
reconsider rseq = seq as Real_Sequence by A1, Th11;
A3: seq is bounded_below by A1, Def5;
then A4: rseq is V65() by Th13;
then lim rseq = lim_sup rseq by A2, RINFSUP1:89;
then lim rseq = lower_bound rseq by A2, RINFSUP1:70;
then A5: lim seq = lower_bound rseq by A2, A4, Th14;
rng seq is bounded_below by A3, Def3;
hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) by A2, A4, A5, Th3, Th14; ::_thesis: verum
end;
Lm4: for seq being ExtREAL_sequence st seq is bounded & seq is non-decreasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is bounded & seq is non-decreasing implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) )
assume that
A1: seq is bounded and
A2: seq is non-decreasing ; ::_thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq )
reconsider rseq = seq as Real_Sequence by A1, Th11;
A3: seq is bounded_above by A1, Def5;
then A4: rseq is V64() by Th12;
then lim rseq = lim_inf rseq by A2, RINFSUP1:89;
then lim rseq = upper_bound rseq by A2, RINFSUP1:64;
then A5: lim seq = upper_bound rseq by A2, A4, Th14;
rng seq is bounded_above by A3, Def4;
hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) by A2, A4, A5, Th1, Th14; ::_thesis: verum
end;
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
proof
let seq be ExtREAL_sequence; ::_thesis: ( ( for n being Element of NAT holds +infty <= seq . n ) implies seq is convergent_to_+infty )
assume A1: for n being Element of NAT holds +infty <= seq . n ; ::_thesis: seq is convergent_to_+infty
now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_
ex_n_being_Nat_st_
for_m_being_Nat_st_n_<=_m_holds_
g_<=_seq_._m
let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m )
assume 0 < g ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m
now__::_thesis:_for_m_being_Nat_st_0_<=_m_holds_
g_<=_seq_._m
let m be Nat; ::_thesis: ( 0 <= m implies g <= seq . m )
assume 0 <= m ; ::_thesis: g <= seq . m
m is Element of NAT by ORDINAL1:def_12;
then A2: +infty <= seq . m by A1;
g <= +infty by XXREAL_0:3;
hence g <= seq . m by A2, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m ; ::_thesis: verum
end;
hence seq is convergent_to_+infty by MESFUNC5:def_9; ::_thesis: verum
end;
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
proof
let seq be ExtREAL_sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n <= -infty ) implies seq is convergent_to_-infty )
assume A1: for n being Element of NAT holds seq . n <= -infty ; ::_thesis: seq is convergent_to_-infty
now__::_thesis:_for_g_being_real_number_st_g_<_0_holds_
ex_n_being_Nat_st_
for_m_being_Nat_st_n_<=_m_holds_
seq_._m_<=_g
let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g )
assume g < 0 ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g
now__::_thesis:_for_m_being_Nat_st_0_<=_m_holds_
seq_._m_<=_g
let m be Nat; ::_thesis: ( 0 <= m implies seq . m <= g )
assume 0 <= m ; ::_thesis: seq . m <= g
m is Element of NAT by ORDINAL1:def_12;
then A2: seq . m <= -infty by A1;
-infty <= g by XXREAL_0:5;
hence seq . m <= g by A2, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g ; ::_thesis: verum
end;
hence seq is convergent_to_-infty by MESFUNC5:def_10; ::_thesis: verum
end;
theorem Th34: :: RINFSUP2:34
for seq being ExtREAL_sequence st seq is non-increasing & -infty = inf seq holds
( seq is convergent_to_-infty & lim seq = -infty )
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is non-increasing & -infty = inf seq implies ( seq is convergent_to_-infty & lim seq = -infty ) )
assume that
A1: seq is non-increasing and
A2: -infty = inf seq ; ::_thesis: ( seq is convergent_to_-infty & lim seq = -infty )
A3: seq is convergent_to_-infty
proof
assume not seq is convergent_to_-infty ; ::_thesis: contradiction
then consider g being real number such that
g < 0 and
A4: for n being Nat ex m being Nat st
( n <= m & g < seq . m ) by MESFUNC5:def_10;
for y being ext-real number st y in rng seq holds
g <= y
proof
let y be ext-real number ; ::_thesis: ( y in rng seq implies g <= y )
assume y in rng seq ; ::_thesis: g <= y
then consider n being set such that
A5: n in NAT and
A6: y = seq . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A5;
consider m being Nat such that
A7: n <= m and
A8: g < seq . m by A4;
m is Element of NAT by ORDINAL1:def_12;
then seq . m <= seq . n by A1, A7, Th7;
hence g <= y by A6, A8, XXREAL_0:2; ::_thesis: verum
end;
then g is LowerBound of rng seq by XXREAL_2:def_2;
then A9: g <= inf (rng seq) by XXREAL_2:def_4;
g in REAL by XREAL_0:def_1;
hence contradiction by A2, A9, XXREAL_0:12; ::_thesis: verum
end;
then seq is convergent by MESFUNC5:def_11;
hence ( seq is convergent_to_-infty & lim seq = -infty ) by A3, MESFUNC5:def_12; ::_thesis: verum
end;
theorem Th35: :: RINFSUP2:35
for seq being ExtREAL_sequence st seq is non-decreasing & +infty = sup seq holds
( seq is convergent_to_+infty & lim seq = +infty )
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is non-decreasing & +infty = sup seq implies ( seq is convergent_to_+infty & lim seq = +infty ) )
assume that
A1: seq is non-decreasing and
A2: +infty = sup seq ; ::_thesis: ( seq is convergent_to_+infty & lim seq = +infty )
A3: seq is convergent_to_+infty
proof
assume not seq is convergent_to_+infty ; ::_thesis: contradiction
then consider g being real number such that
0 < g and
A4: for n being Nat ex m being Nat st
( n <= m & seq . m < g ) by MESFUNC5:def_9;
for y being ext-real number st y in rng seq holds
y <= g
proof
let y be ext-real number ; ::_thesis: ( y in rng seq implies y <= g )
assume y in rng seq ; ::_thesis: y <= g
then consider n being set such that
A5: n in NAT and
A6: y = seq . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A5;
consider m being Nat such that
A7: n <= m and
A8: seq . m < g by A4;
m is Element of NAT by ORDINAL1:def_12;
then seq . n <= seq . m by A1, A7, Th7;
hence y <= g by A6, A8, XXREAL_0:2; ::_thesis: verum
end;
then g is UpperBound of rng seq by XXREAL_2:def_1;
then A9: sup (rng seq) <= g by XXREAL_2:def_3;
g in REAL by XREAL_0:def_1;
hence contradiction by A2, A9, XXREAL_0:9; ::_thesis: verum
end;
then seq is convergent by MESFUNC5:def_11;
hence ( seq is convergent_to_+infty & lim seq = +infty ) by A3, MESFUNC5:def_12; ::_thesis: verum
end;
theorem Th36: :: RINFSUP2:36
for seq being ExtREAL_sequence st seq is non-increasing holds
( seq is convergent & lim seq = inf seq )
proof
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 )
percases ( for n being Element of NAT holds +infty <= seq . n or ex n being Element of NAT st not +infty <= seq . n ) ;
supposeA2: for n being Element of NAT holds +infty <= seq . n ; ::_thesis: ( seq is convergent & lim seq = inf seq )
now__::_thesis:_for_y_being_set_st_y_in_{+infty}_holds_
y_in_rng_seq
let y be set ; ::_thesis: ( y in {+infty} implies y in rng seq )
assume y in {+infty} ; ::_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_contradiction
let n be Element of NAT ; ::_thesis: contradiction
n in NAT ;
then n in dom seq by FUNCT_2:def_1;
then seq . n <> +infty by A3, A4, FUNCT_1:def_3;
hence contradiction by A2, XXREAL_0:4; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
hence y in rng seq ; ::_thesis: verum
end;
then A5: {+infty} c= rng seq by TARSKI:def_3;
A6: seq is convergent_to_+infty by A2, Th32;
hence A7: seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = inf seq
now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_
y_in_{+infty}
let y be set ; ::_thesis: ( y in rng seq implies y in {+infty} )
assume y in rng seq ; ::_thesis: y in {+infty}
then ex x being set st
( x in dom seq & seq . x = y ) by FUNCT_1:def_3;
then y = +infty by A2, XXREAL_0:4;
hence y in {+infty} by TARSKI:def_1; ::_thesis: verum
end;
then rng seq c= {+infty} by TARSKI:def_3;
then rng seq = {+infty} by A5, XBOOLE_0:def_10;
then inf seq = +infty by XXREAL_2:13;
hence lim seq = inf seq by A6, A7, MESFUNC5:def_12; ::_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 ;
percases ( -infty <> inf seq or -infty = inf seq ) ;
supposeA9: -infty <> inf seq ; ::_thesis: ( seq is convergent & lim seq = inf seq )
set seq0 = seq ^\ k;
A10: inf seq = inf (seq ^\ k) by A1, Th25;
A11: now__::_thesis:_not_rng_(seq_^\_k)_=_{-infty}
assume rng (seq ^\ k) = {-infty} ; ::_thesis: contradiction
then A12: -infty in rng (seq ^\ k) by TARSKI:def_1;
-infty is LowerBound of rng (seq ^\ k) by XXREAL_2:42;
hence contradiction by A9, A10, A12, XXREAL_2:56; ::_thesis: verum
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 A9, XXREAL_0:2, XXREAL_0:6;
then A15: seq ^\ k is bounded_above by A1, A8, Th30;
then rng (seq ^\ k) is bounded_above by Def4;
then sup (rng (seq ^\ k)) < +infty by A11, XXREAL_0:9, XXREAL_2:57;
then inf (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14;
then rng (seq ^\ k) is bounded_below by A14, XXREAL_2:def_9;
then seq ^\ k is bounded_below by Def3;
then A16: seq ^\ k is bounded by A15, Def5;
A17: seq ^\ k is non-increasing by A1, Th25;
then A18: lim (seq ^\ k) = inf (seq ^\ k) by A16, Lm3;
seq ^\ k is convergent by A17, A16, Lm3;
hence ( seq is convergent & lim seq = inf seq ) by A10, A18, Th17; ::_thesis: verum
end;
supposeA19: -infty = inf seq ; ::_thesis: ( seq is convergent & lim seq = inf seq )
then seq is convergent_to_-infty by A1, Th34;
hence seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = inf seq
thus lim seq = inf seq by A1, A19, Th34; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th37: :: RINFSUP2:37
for seq being ExtREAL_sequence st seq is non-decreasing holds
( seq is convergent & lim seq = sup seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is non-decreasing implies ( seq is convergent & lim seq = sup seq ) )
assume A1: seq is non-decreasing ; ::_thesis: ( seq is convergent & lim seq = sup seq )
percases ( for n being Element of NAT holds seq . n <= -infty or ex n being Element of NAT st not seq . n <= -infty ) ;
supposeA2: for n being Element of NAT holds seq . n <= -infty ; ::_thesis: ( seq is convergent & lim seq = sup seq )
now__::_thesis:_for_y_being_set_st_y_in_{-infty}_holds_
y_in_rng_seq
let y be set ; ::_thesis: ( y in {-infty} implies y in rng seq )
assume y in {-infty} ; ::_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_contradiction
let n be Element of NAT ; ::_thesis: contradiction
n in NAT ;
then n in dom seq by FUNCT_2:def_1;
then seq . n <> -infty by A3, A4, FUNCT_1:def_3;
hence contradiction by A2, XXREAL_0:6; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
hence y in rng seq ; ::_thesis: verum
end;
then A5: {-infty} c= rng seq by TARSKI:def_3;
A6: seq is convergent_to_-infty by A2, Th33;
hence A7: seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = sup seq
now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_
y_in_{-infty}
let y be set ; ::_thesis: ( y in rng seq implies y in {-infty} )
assume y in rng seq ; ::_thesis: y in {-infty}
then ex x being set st
( x in dom seq & seq . x = y ) by FUNCT_1:def_3;
then y = -infty by A2, XXREAL_0:6;
hence y in {-infty} by TARSKI:def_1; ::_thesis: verum
end;
then rng seq c= {-infty} by TARSKI:def_3;
then rng seq = {-infty} by A5, XBOOLE_0:def_10;
then sup seq = -infty by XXREAL_2:11;
hence lim seq = sup seq by A6, A7, MESFUNC5:def_12; ::_thesis: verum
end;
suppose not for n being Element of NAT holds seq . n <= -infty ; ::_thesis: ( seq is convergent & lim seq = sup seq )
then consider k being Element of NAT such that
A8: -infty < seq . k ;
percases ( +infty <> sup seq or +infty = sup seq ) ;
supposeA9: +infty <> sup seq ; ::_thesis: ( seq is convergent & lim seq = sup seq )
set seq0 = seq ^\ k;
A10: sup seq = sup (seq ^\ k) by A1, Th26;
A11: now__::_thesis:_not_rng_(seq_^\_k)_=_{+infty}
assume rng (seq ^\ k) = {+infty} ; ::_thesis: contradiction
then A12: +infty in rng (seq ^\ k) by TARSKI:def_1;
+infty is UpperBound of rng (seq ^\ k) by XXREAL_2:41;
hence contradiction by A9, A10, A12, XXREAL_2:55; ::_thesis: verum
end;
A13: inf (seq ^\ k) <= sup (seq ^\ k) by Th24;
A14: sup (rng (seq ^\ k)) is UpperBound of rng (seq ^\ k) by XXREAL_2:def_3;
seq . k <= sup seq by Th23;
then seq . k < +infty by A9, XXREAL_0:2, XXREAL_0:4;
then A15: seq ^\ k is bounded_below by A1, A8, Th31;
then rng (seq ^\ k) is bounded_below by Def3;
then -infty < inf (rng (seq ^\ k)) by A11, XXREAL_0:12, XXREAL_2:58;
then sup (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14;
then rng (seq ^\ k) is bounded_above by A14, XXREAL_2:def_10;
then seq ^\ k is bounded_above by Def4;
then A16: seq ^\ k is bounded by A15, Def5;
A17: seq ^\ k is non-decreasing by A1, Th26;
then A18: lim (seq ^\ k) = sup (seq ^\ k) by A16, Lm4;
seq ^\ k is convergent by A17, A16, Lm4;
hence ( seq is convergent & lim seq = sup seq ) by A10, A18, Th17; ::_thesis: verum
end;
supposeA19: +infty = sup seq ; ::_thesis: ( seq is convergent & lim seq = sup seq )
then seq is convergent_to_+infty by A1, Th35;
hence seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = sup seq
thus lim seq = sup seq by A1, A19, Th35; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th38: :: RINFSUP2:38
for seq1, seq2 being ExtREAL_sequence st seq1 is convergent & seq2 is convergent & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds
lim seq1 <= lim seq2
proof
let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( seq1 is convergent & seq2 is convergent & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) implies lim seq1 <= lim seq2 )
assume that
A1: seq1 is convergent and
A2: seq2 is convergent and
A3: for n being Element of NAT holds seq1 . n <= seq2 . n ; ::_thesis: lim seq1 <= lim seq2
percases ( seq1 is convergent_to_finite_number or seq1 is convergent_to_+infty or seq1 is convergent_to_-infty ) by A1, MESFUNC5:def_11;
supposeA4: seq1 is convergent_to_finite_number ; ::_thesis: lim seq1 <= lim seq2
A5: not seq2 is convergent_to_-infty
proof
assume A6: seq2 is convergent_to_-infty ; ::_thesis: contradiction
now__::_thesis:_for_g_being_real_number_st_g_<_0_holds_
ex_n_being_Nat_st_
for_m_being_Nat_st_n_<=_m_holds_
seq1_._m_<=_g
let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
seq1 . m <= g )
assume g < 0 ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
seq1 . m <= g
then consider n being Nat such that
A7: for m being Nat st n <= m holds
seq2 . m <= g by A6, MESFUNC5:def_10;
now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_
seq1_._m_<=_g
let m be Nat; ::_thesis: ( n <= m implies seq1 . m <= g )
m is Element of NAT by ORDINAL1:def_12;
then A8: seq1 . m <= seq2 . m by A3;
assume n <= m ; ::_thesis: seq1 . m <= g
then seq2 . m <= g by A7;
hence seq1 . m <= g by A8, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
seq1 . m <= g ; ::_thesis: verum
end;
then seq1 is convergent_to_-infty by MESFUNC5:def_10;
hence contradiction by A4, MESFUNC5:51; ::_thesis: verum
end;
percases ( seq2 is convergent_to_finite_number or seq2 is convergent_to_+infty ) by A2, A5, MESFUNC5:def_11;
supposeA9: seq2 is convergent_to_finite_number ; ::_thesis: lim seq1 <= lim seq2
consider k1 being Element of NAT such that
A10: seq1 ^\ k1 is bounded by A4, Th19;
seq1 ^\ k1 is bounded_above by A10, Def5;
then rng (seq1 ^\ k1) is bounded_above by Def4;
then consider UB being real number such that
A11: UB is UpperBound of rng (seq1 ^\ k1) by XXREAL_2:def_10;
consider k2 being Element of NAT such that
A12: seq2 ^\ k2 is bounded by A9, Th19;
reconsider k = max (k1,k2) as Element of NAT ;
A13: lim seq2 = lim (seq2 ^\ k) by A9, Th20;
A14: dom (seq1 ^\ k1) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_y_being_set_st_y_in_rng_(seq1_^\_k)_holds_
y_in_rng_(seq1_^\_k1)
reconsider k2 = k - k1 as Element of NAT by INT_1:5, XXREAL_0:25;
let y be set ; ::_thesis: ( y in rng (seq1 ^\ k) implies y in rng (seq1 ^\ k1) )
assume y in rng (seq1 ^\ k) ; ::_thesis: y in rng (seq1 ^\ k1)
then consider n being set such that
A15: n in dom (seq1 ^\ k) and
A16: (seq1 ^\ k) . n = y by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A15;
y = seq1 . (k + n) by A16, NAT_1:def_3;
then y = seq1 . (k1 + (k2 + n)) ;
then y = (seq1 ^\ k1) . (k2 + n) by NAT_1:def_3;
hence y in rng (seq1 ^\ k1) by A14, FUNCT_1:def_3; ::_thesis: verum
end;
then A17: rng (seq1 ^\ k) c= rng (seq1 ^\ k1) by TARSKI:def_3;
then UB is UpperBound of rng (seq1 ^\ k) by A11, XXREAL_2:6;
then rng (seq1 ^\ k) is bounded_above by XXREAL_2:def_10;
then A18: seq1 ^\ k is bounded_above by Def4;
seq1 ^\ k1 is bounded_below by A10, Def5;
then rng (seq1 ^\ k1) is bounded_below by Def3;
then consider LB being real number such that
A19: LB is LowerBound of rng (seq1 ^\ k1) by XXREAL_2:def_9;
LB is LowerBound of rng (seq1 ^\ k) by A17, A19, XXREAL_2:5;
then rng (seq1 ^\ k) is bounded_below by XXREAL_2:def_9;
then seq1 ^\ k is bounded_below by Def3;
then seq1 ^\ k is bounded by A18, Def5;
then reconsider rseq1 = seq1 ^\ k as Real_Sequence by Th11;
seq2 ^\ k2 is bounded_below by A12, Def5;
then rng (seq2 ^\ k2) is bounded_below by Def3;
then consider LB being real number such that
A20: LB is LowerBound of rng (seq2 ^\ k2) by XXREAL_2:def_9;
A21: lim seq1 = lim (seq1 ^\ k) by A4, Th20;
seq2 ^\ k2 is bounded_above by A12, Def5;
then rng (seq2 ^\ k2) is bounded_above by Def4;
then consider UB being real number such that
A22: UB is UpperBound of rng (seq2 ^\ k2) by XXREAL_2:def_10;
A23: dom (seq2 ^\ k2) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_y_being_set_st_y_in_rng_(seq2_^\_k)_holds_
y_in_rng_(seq2_^\_k2)
reconsider k3 = k - k2 as Element of NAT by INT_1:5, XXREAL_0:25;
let y be set ; ::_thesis: ( y in rng (seq2 ^\ k) implies y in rng (seq2 ^\ k2) )
assume y in rng (seq2 ^\ k) ; ::_thesis: y in rng (seq2 ^\ k2)
then consider n being set such that
A24: n in dom (seq2 ^\ k) and
A25: (seq2 ^\ k) . n = y by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A24;
y = seq2 . (k + n) by A25, NAT_1:def_3;
then y = seq2 . (k2 + (k3 + n)) ;
then y = (seq2 ^\ k2) . (k3 + n) by NAT_1:def_3;
hence y in rng (seq2 ^\ k2) by A23, FUNCT_1:def_3; ::_thesis: verum
end;
then A26: rng (seq2 ^\ k) c= rng (seq2 ^\ k2) by TARSKI:def_3;
then UB is UpperBound of rng (seq2 ^\ k) by A22, XXREAL_2:6;
then rng (seq2 ^\ k) is bounded_above by XXREAL_2:def_10;
then A27: seq2 ^\ k is bounded_above by Def4;
LB is LowerBound of rng (seq2 ^\ k) by A20, A26, XXREAL_2:5;
then rng (seq2 ^\ k) is bounded_below by XXREAL_2:def_9;
then seq2 ^\ k is bounded_below by Def3;
then seq2 ^\ k is bounded by A27, Def5;
then reconsider rseq2 = seq2 ^\ k as Real_Sequence by Th11;
A28: seq2 ^\ k is convergent_to_finite_number by A9, Th20;
then A29: rseq2 is convergent by Th15;
A30: for n being Element of NAT holds rseq1 . n <= rseq2 . n
proof
let n be Element of NAT ; ::_thesis: rseq1 . n <= rseq2 . n
A31: (seq2 ^\ k) . n = seq2 . (k + n) by NAT_1:def_3;
(seq1 ^\ k) . n = seq1 . (k + n) by NAT_1:def_3;
hence rseq1 . n <= rseq2 . n by A3, A31; ::_thesis: verum
end;
A32: seq1 ^\ k is convergent_to_finite_number by A4, Th20;
then A33: lim (seq1 ^\ k) = lim rseq1 by Th15;
A34: lim (seq2 ^\ k) = lim rseq2 by A28, Th15;
rseq1 is convergent by A32, Th15;
hence lim seq1 <= lim seq2 by A29, A33, A34, A30, A21, A13, SEQ_2:18; ::_thesis: verum
end;
supposeA35: seq2 is convergent_to_+infty ; ::_thesis: lim seq1 <= lim seq2
then seq2 is convergent by MESFUNC5:def_11;
then lim seq2 = +infty by A35, MESFUNC5:def_12;
hence lim seq1 <= lim seq2 by XXREAL_0:3; ::_thesis: verum
end;
end;
end;
supposeA36: seq1 is convergent_to_+infty ; ::_thesis: lim seq1 <= lim seq2
now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_
ex_n_being_Nat_st_
for_m_being_Nat_st_n_<=_m_holds_
g_<=_seq2_._m
let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= seq2 . m )
assume 0 < g ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= seq2 . m
then consider n being Nat such that
A37: for m being Nat st n <= m holds
g <= seq1 . m by A36, MESFUNC5:def_9;
now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_
g_<=_seq2_._m
let m be Nat; ::_thesis: ( n <= m implies g <= seq2 . m )
m is Element of NAT by ORDINAL1:def_12;
then A38: seq1 . m <= seq2 . m by A3;
assume n <= m ; ::_thesis: g <= seq2 . m
then g <= seq1 . m by A37;
hence g <= seq2 . m by A38, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
g <= seq2 . m ; ::_thesis: verum
end;
then A39: seq2 is convergent_to_+infty by MESFUNC5:def_9;
then seq2 is convergent by MESFUNC5:def_11;
then lim seq2 = +infty by A39, MESFUNC5:def_12;
hence lim seq1 <= lim seq2 by XXREAL_0:3; ::_thesis: verum
end;
supposeA40: seq1 is convergent_to_-infty ; ::_thesis: lim seq1 <= lim seq2
then seq1 is convergent by MESFUNC5:def_11;
then lim seq1 = -infty by A40, MESFUNC5:def_12;
hence lim seq1 <= lim seq2 by XXREAL_0:5; ::_thesis: verum
end;
end;
end;
theorem :: RINFSUP2:39
for seq being ExtREAL_sequence holds lim_inf seq <= lim_sup seq
proof
let seq be ExtREAL_sequence; ::_thesis: lim_inf seq <= lim_sup seq
A1: lim (superior_realsequence seq) = lim_sup seq by Th36;
A2: inferior_realsequence seq is convergent by Th37;
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_realsequence_seq)_._n_<=_(superior_realsequence_seq)_._n
let n be Element of NAT ; ::_thesis: (inferior_realsequence seq) . n <= (superior_realsequence seq) . n
A4: seq . n <= (superior_realsequence seq) . n by Th8;
(inferior_realsequence seq) . n <= seq . n by Th8;
hence (inferior_realsequence seq) . n <= (superior_realsequence seq) . n by A4, XXREAL_0:2; ::_thesis: verum
end;
A5: lim (inferior_realsequence seq) = lim_inf seq by Th37;
superior_realsequence seq is convergent by Th36;
hence lim_inf seq <= lim_sup seq by A1, A2, A5, A3, Th38; ::_thesis: verum
end;
Lm5: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = +infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( lim_inf seq = lim_sup seq & lim_inf seq = +infty implies ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) )
assume that
A1: lim_inf seq = lim_sup seq and
A2: lim_inf seq = +infty ; ::_thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
A3: inferior_realsequence seq is convergent_to_+infty by A2, Th35;
now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_
ex_n_being_Nat_st_
for_m_being_Nat_st_n_<=_m_holds_
g_<=_seq_._m
let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m )
assume 0 < g ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m
then consider n being Nat such that
A4: for m being Nat st n <= m holds
g <= (inferior_realsequence seq) . m by A3, MESFUNC5:def_9;
now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_
g_<=_seq_._m
let m be Nat; ::_thesis: ( n <= m implies g <= seq . m )
m is Element of NAT by ORDINAL1:def_12;
then A5: (inferior_realsequence seq) . m <= seq . m by Th8;
assume n <= m ; ::_thesis: g <= seq . m
then g <= (inferior_realsequence seq) . m by A4;
hence g <= seq . m by A5, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m ; ::_thesis: verum
end;
then A6: seq is convergent_to_+infty by MESFUNC5:def_9;
then seq is convergent by MESFUNC5:def_11;
hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, A2, A6, MESFUNC5:def_12; ::_thesis: verum
end;
Lm6: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = -infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( lim_inf seq = lim_sup seq & lim_inf seq = -infty implies ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) )
assume that
A1: lim_inf seq = lim_sup seq and
A2: lim_inf seq = -infty ; ::_thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
A3: superior_realsequence seq is convergent_to_-infty by A1, A2, Th34;
now__::_thesis:_for_g_being_real_number_st_g_<_0_holds_
ex_n_being_Nat_st_
for_m_being_Nat_st_n_<=_m_holds_
seq_._m_<=_g
let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g )
assume g < 0 ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g
then consider n being Nat such that
A4: for m being Nat st n <= m holds
(superior_realsequence seq) . m <= g by A3, MESFUNC5:def_10;
now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_
seq_._m_<=_g
let m be Nat; ::_thesis: ( n <= m implies seq . m <= g )
m is Element of NAT by ORDINAL1:def_12;
then A5: seq . m <= (superior_realsequence seq) . m by Th8;
assume n <= m ; ::_thesis: seq . m <= g
then (superior_realsequence seq) . m <= g by A4;
hence seq . m <= g by A5, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g ; ::_thesis: verum
end;
then A6: seq is convergent_to_-infty by MESFUNC5:def_10;
then seq is convergent by MESFUNC5:def_11;
hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, A2, A6, MESFUNC5:def_12; ::_thesis: verum
end;
Lm7: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq in REAL holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( lim_inf seq = lim_sup seq & lim_inf seq in REAL implies ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) )
assume that
A1: lim_inf seq = lim_sup seq and
A2: lim_inf seq in REAL ; ::_thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
consider k being Element of NAT such that
A3: seq ^\ k is bounded by A1, A2, Th18;
reconsider rseq0 = seq ^\ k as Real_Sequence by A3, Th11;
seq ^\ k is bounded_below by A3, Def5;
then A4: rseq0 is V65() by Th13;
seq ^\ k is bounded_above by A3, Def5;
then A5: rseq0 is V64() by Th12;
then lim_sup rseq0 = lim_sup (seq ^\ k) by A4, Th9;
then A6: lim_sup rseq0 = lim_sup seq by Th28;
lim_inf rseq0 = lim_inf (seq ^\ k) by A5, A4, Th10;
then A7: lim_inf rseq0 = lim_inf seq by Th29;
then A8: rseq0 is convergent by A1, A5, A4, A6, RINFSUP1:88;
then A9: lim rseq0 = lim_inf seq by A7, RINFSUP1:89;
A10: seq ^\ k is convergent by A8, Th14;
A11: lim rseq0 = lim (seq ^\ k) by A8, Th14;
lim rseq0 = lim_sup seq by A6, A8, RINFSUP1:89;
hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by A9, A11, A10, Th17; ::_thesis: verum
end;
theorem Th40: :: RINFSUP2:40
for seq being ExtREAL_sequence holds
( seq is convergent iff lim_inf seq = lim_sup seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent iff lim_inf seq = lim_sup seq )
set a = lim_inf seq;
thus ( seq is convergent implies lim_inf seq = lim_sup seq ) ::_thesis: ( lim_inf seq = lim_sup seq implies seq is convergent )
proof
assume A1: seq is convergent ; ::_thesis: lim_inf seq = lim_sup seq
percases ( seq is convergent_to_finite_number or seq is convergent_to_-infty or seq is convergent_to_+infty ) by A1, MESFUNC5:def_11;
supposeA2: seq is convergent_to_finite_number ; ::_thesis: lim_inf seq = lim_sup seq
then consider k being Element of NAT such that
A3: seq ^\ k is bounded by Th19;
reconsider rseq0 = seq ^\ k as Real_Sequence by A3, Th11;
seq ^\ k is convergent_to_finite_number by A2, Th20;
then A4: rseq0 is convergent by Th15;
then A5: rseq0 is bounded ;
then lim_sup rseq0 = lim_sup (seq ^\ k) by Th9;
then A6: lim_sup rseq0 = lim_sup seq by Th28;
lim_inf rseq0 = lim_inf (seq ^\ k) by A5, Th10;
then lim_inf rseq0 = lim_inf seq by Th29;
hence lim_inf seq = lim_sup seq by A4, A6, RINFSUP1:88; ::_thesis: verum
end;
supposeA7: seq is convergent_to_-infty ; ::_thesis: lim_inf seq = lim_sup seq
now__::_thesis:_for_g_being_real_number_st_g_<_0_holds_
ex_n_being_Nat_st_
for_m_being_Nat_st_n_<=_m_holds_
(inferior_realsequence_seq)_._m_<=_g
let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g )
assume g < 0 ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g
then consider n being Nat such that
A8: for m being Nat st n <= m holds
seq . m <= g by A7, MESFUNC5:def_10;
now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_
(inferior_realsequence_seq)_._m_<=_g
let m be Nat; ::_thesis: ( n <= m implies (inferior_realsequence seq) . m <= g )
m is Element of NAT by ORDINAL1:def_12;
then A9: (inferior_realsequence seq) . m <= seq . m by Th8;
assume n <= m ; ::_thesis: (inferior_realsequence seq) . m <= g
then seq . m <= g by A8;
hence (inferior_realsequence seq) . m <= g by A9, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g ; ::_thesis: verum
end;
then A10: inferior_realsequence seq is convergent_to_-infty by MESFUNC5:def_10;
then inferior_realsequence seq is convergent by MESFUNC5:def_11;
then lim (inferior_realsequence seq) = -infty by A10, MESFUNC5:def_12;
then A11: lim_inf seq = -infty by Th37;
A12: superior_realsequence seq is convergent_to_-infty
proof
set iseq = superior_realsequence seq;
assume not superior_realsequence seq is convergent_to_-infty ; ::_thesis: contradiction
then consider g being real number such that
A13: g < 0 and
A14: for n being Nat ex m being Nat st
( n <= m & g < (superior_realsequence seq) . m ) by MESFUNC5:def_10;
consider N being Nat such that
A15: for m being Nat st N <= m holds
seq . m <= g by A7, A13, MESFUNC5:def_10;
now__::_thesis:_for_m_being_Nat_st_N_<=_m_holds_
(superior_realsequence_seq)_._m_<=_g
let m be Nat; ::_thesis: ( N <= m implies (superior_realsequence seq) . m <= g )
m is Element of NAT by ORDINAL1:def_12;
then consider Y being non empty Subset of ExtREAL such that
A16: Y = { (seq . k) where k is Element of NAT : m <= k } and
A17: (superior_realsequence seq) . m = sup Y by Def7;
assume A18: N <= m ; ::_thesis: (superior_realsequence seq) . m <= g
now__::_thesis:_for_x_being_ext-real_number_st_x_in_Y_holds_
x_<=_g
let x be ext-real number ; ::_thesis: ( x in Y implies x <= g )
assume x in Y ; ::_thesis: x <= g
then consider k being Element of NAT such that
A19: x = seq . k and
A20: m <= k by A16;
N <= k by A18, A20, XXREAL_0:2;
hence x <= g by A15, A19; ::_thesis: verum
end;
then g is UpperBound of Y by XXREAL_2:def_1;
hence (superior_realsequence seq) . m <= g by A17, XXREAL_2:def_3; ::_thesis: verum
end;
hence contradiction by A14; ::_thesis: verum
end;
then superior_realsequence seq is convergent by MESFUNC5:def_11;
then lim (superior_realsequence seq) = -infty by A12, MESFUNC5:def_12;
hence lim_inf seq = lim_sup seq by A11, Th36; ::_thesis: verum
end;
supposeA21: seq is convergent_to_+infty ; ::_thesis: lim_inf seq = lim_sup seq
now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_
ex_n_being_Nat_st_
for_m_being_Nat_st_n_<=_m_holds_
g_<=_(superior_realsequence_seq)_._m
let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m )
assume 0 < g ; ::_thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m
then consider n being Nat such that
A22: for m being Nat st n <= m holds
g <= seq . m by A21, MESFUNC5:def_9;
now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_
g_<=_(superior_realsequence_seq)_._m
let m be Nat; ::_thesis: ( n <= m implies g <= (superior_realsequence seq) . m )
m is Element of NAT by ORDINAL1:def_12;
then A23: seq . m <= (superior_realsequence seq) . m by Th8;
assume n <= m ; ::_thesis: g <= (superior_realsequence seq) . m
then g <= seq . m by A22;
hence g <= (superior_realsequence seq) . m by A23, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m ; ::_thesis: verum
end;
then A24: superior_realsequence seq is convergent_to_+infty by MESFUNC5:def_9;
then superior_realsequence seq is convergent by MESFUNC5:def_11;
then lim (superior_realsequence seq) = +infty by A24, MESFUNC5:def_12;
then A25: lim_sup seq = +infty by Th36;
A26: inferior_realsequence seq is convergent_to_+infty
proof
set iseq = inferior_realsequence seq;
assume not inferior_realsequence seq is convergent_to_+infty ; ::_thesis: contradiction
then consider g being real number such that
A27: 0 < g and
A28: for n being Nat ex m being Nat st
( n <= m & (inferior_realsequence seq) . m < g ) by MESFUNC5:def_9;
consider N being Nat such that
A29: for m being Nat st N <= m holds
g <= seq . m by A21, A27, MESFUNC5:def_9;
now__::_thesis:_for_m_being_Nat_st_N_<=_m_holds_
g_<=_(inferior_realsequence_seq)_._m
let m be Nat; ::_thesis: ( N <= m implies g <= (inferior_realsequence seq) . m )
m is Element of NAT by ORDINAL1:def_12;
then consider Y being non empty Subset of ExtREAL such that
A30: Y = { (seq . k) where k is Element of NAT : m <= k } and
A31: (inferior_realsequence seq) . m = inf Y by Def6;
assume A32: N <= m ; ::_thesis: g <= (inferior_realsequence seq) . m
now__::_thesis:_for_x_being_ext-real_number_st_x_in_Y_holds_
g_<=_x
let x be ext-real number ; ::_thesis: ( x in Y implies g <= x )
assume x in Y ; ::_thesis: g <= x
then consider k being Element of NAT such that
A33: x = seq . k and
A34: m <= k by A30;
N <= k by A32, A34, XXREAL_0:2;
hence g <= x by A29, A33; ::_thesis: verum
end;
then g is LowerBound of Y by XXREAL_2:def_2;
hence g <= (inferior_realsequence seq) . m by A31, XXREAL_2:def_4; ::_thesis: verum
end;
hence contradiction by A28; ::_thesis: verum
end;
then inferior_realsequence seq is convergent by MESFUNC5:def_11;
then lim (inferior_realsequence seq) = +infty by A26, MESFUNC5:def_12;
hence lim_inf seq = lim_sup seq by A25, Th37; ::_thesis: verum
end;
end;
end;
assume A35: lim_inf seq = lim_sup seq ; ::_thesis: seq is convergent
percases ( lim_inf seq in REAL or lim_inf seq = +infty or lim_inf seq = -infty ) by XXREAL_0:14;
suppose lim_inf seq in REAL ; ::_thesis: seq is convergent
hence seq is convergent by A35, Lm7; ::_thesis: verum
end;
suppose lim_inf seq = +infty ; ::_thesis: seq is convergent
hence seq is convergent by A35, Lm5; ::_thesis: verum
end;
suppose lim_inf seq = -infty ; ::_thesis: seq is convergent
hence seq is convergent by A35, Lm6; ::_thesis: verum
end;
end;
end;
theorem :: RINFSUP2:41
for seq being ExtREAL_sequence st seq is convergent holds
( lim seq = lim_inf seq & lim seq = lim_sup seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent implies ( lim seq = lim_inf seq & lim seq = lim_sup seq ) )
set a = lim_inf seq;
assume seq is convergent ; ::_thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )
then A1: lim_inf seq = lim_sup seq by Th40;
percases ( lim_inf seq in REAL or lim_inf seq = +infty or lim_inf seq = -infty ) by XXREAL_0:14;
suppose lim_inf seq in REAL ; ::_thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )
hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm7; ::_thesis: verum
end;
suppose lim_inf seq = +infty ; ::_thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )
hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm5; ::_thesis: verum
end;
suppose lim_inf seq = -infty ; ::_thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )
hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm6; ::_thesis: verum
end;
end;
end;