:: by Hiroshi Yamazaki , Noboru Endou , Yasunari Shidama and Hiroyuki Okazaki

::

:: Received August 28, 2007

:: Copyright (c) 2007-2017 Association of Mizar Users

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 )

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 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;

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 )

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 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;

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;

coherence

sup (rng seq) is Element of ExtREAL ;

coherence

inf (rng seq) is Element of ExtREAL ;

end;
coherence

sup (rng seq) is Element of ExtREAL ;

coherence

inf (rng seq) is Element of ExtREAL ;

:: deftheorem defines sup RINFSUP2:def 1 :

for seq being ExtREAL_sequence holds sup seq = sup (rng seq);

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);

for seq being ExtREAL_sequence holds inf seq = inf (rng seq);

:: deftheorem defines bounded_below RINFSUP2:def 3 :

for seq being ExtREAL_sequence holds

( seq is bounded_below iff rng seq is bounded_below );

for seq being ExtREAL_sequence holds

( seq is bounded_below iff rng seq is bounded_below );

:: deftheorem defines bounded_above RINFSUP2:def 4 :

for seq being ExtREAL_sequence holds

( seq is bounded_above iff rng seq is bounded_above );

for seq being ExtREAL_sequence holds

( seq is bounded_above iff rng seq is bounded_above );

:: deftheorem defines bounded RINFSUP2:def 5 :

for seq being ExtREAL_sequence holds

( seq is bounded iff ( seq is bounded_above & seq is bounded_below ) );

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 Nat holds { (seq . k) where k is Nat : n <= k } is non empty Subset of ExtREAL

for n being Nat holds { (seq . k) where k is Nat : n <= k } is non empty Subset of ExtREAL

proof end;

definition

let seq be ExtREAL_sequence;

ex b_{1} being ExtREAL_sequence st

for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b_{1} . n = inf Y )

for b_{1}, b_{2} being ExtREAL_sequence st ( for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b_{1} . n = inf Y ) ) & ( for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b_{2} . n = inf Y ) ) holds

b_{1} = b_{2}

end;
func inferior_realsequence seq -> ExtREAL_sequence means :Def6: :: RINFSUP2:def 6

for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & it . n = inf Y );

existence for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & it . n = inf Y );

ex b

for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b

proof end;

uniqueness for b

( Y = { (seq . k) where k is Nat : n <= k } & b

( Y = { (seq . k) where k is Nat : n <= k } & b

b

proof end;

:: deftheorem Def6 defines inferior_realsequence RINFSUP2:def 6 :

for seq, b_{2} being ExtREAL_sequence holds

( b_{2} = inferior_realsequence seq iff for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b_{2} . n = inf Y ) );

for seq, b

( b

( Y = { (seq . k) where k is Nat : n <= k } & b

definition

let seq be ExtREAL_sequence;

ex b_{1} being ExtREAL_sequence st

for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b_{1} . n = sup Y )

for b_{1}, b_{2} being ExtREAL_sequence st ( for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b_{1} . n = sup Y ) ) & ( for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b_{2} . n = sup Y ) ) holds

b_{1} = b_{2}

end;
func superior_realsequence seq -> ExtREAL_sequence means :Def7: :: RINFSUP2:def 7

for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & it . n = sup Y );

existence for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & it . n = sup Y );

ex b

for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b

proof end;

uniqueness for b

( Y = { (seq . k) where k is Nat : n <= k } & b

( Y = { (seq . k) where k is Nat : n <= k } & b

b

proof end;

:: deftheorem Def7 defines superior_realsequence RINFSUP2:def 7 :

for seq, b_{2} being ExtREAL_sequence holds

( b_{2} = superior_realsequence seq iff for n being Nat ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & b_{2} . n = sup Y ) );

for seq, b

( b

( Y = { (seq . k) where k is Nat : n <= k } & b

theorem :: RINFSUP2:6

theorem Th7: :: RINFSUP2:7

for seq being ExtREAL_sequence holds

( ( seq is increasing implies for n, m being Nat st m < n holds

seq . m < seq . n ) & ( ( for n, m being Nat st m < n holds

seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Nat st m < n holds

seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

( ( seq is increasing implies for n, m being Nat st m < n holds

seq . m < seq . n ) & ( ( for n, m being Nat st m < n holds

seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Nat st m < n holds

seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

proof end;

theorem Th8: :: RINFSUP2:8

for n being Nat

for seq being ExtREAL_sequence holds

( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )

for seq being ExtREAL_sequence holds

( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )

proof end;

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

proof end;

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

proof end;

registration

let seq be ExtREAL_sequence;

coherence

superior_realsequence seq is non-increasing by Lm1;

coherence

inferior_realsequence seq is non-decreasing by Lm2;

end;
coherence

superior_realsequence seq is non-increasing by Lm1;

coherence

inferior_realsequence seq is non-decreasing by Lm2;

definition

let seq be ExtREAL_sequence;

coherence

inf (superior_realsequence seq) is Element of ExtREAL ;

coherence

sup (inferior_realsequence seq) is Element of ExtREAL ;

end;
coherence

inf (superior_realsequence seq) is Element of ExtREAL ;

coherence

sup (inferior_realsequence seq) is Element of ExtREAL ;

:: deftheorem defines lim_sup RINFSUP2:def 8 :

for seq being ExtREAL_sequence holds lim_sup seq = inf (superior_realsequence seq);

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);

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 )

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 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 )

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 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 V70() )

for rseq being Real_Sequence st seq = rseq holds

( seq is bounded_above iff rseq is V70() )

proof 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 V71() )

for rseq being Real_Sequence st seq = rseq holds

( seq is bounded_below iff rseq is V71() )

proof 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 )

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 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 )

for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds

( rseq is convergent & lim seq = lim rseq )

proof end;

theorem Th16: :: RINFSUP2:16

for k being 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) )

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 end;

theorem Th17: :: RINFSUP2:17

for k being Nat

for seq being ExtREAL_sequence st seq ^\ k is convergent holds

( seq is convergent & lim seq = lim (seq ^\ k) )

for seq being ExtREAL_sequence st seq ^\ k is convergent holds

( seq is convergent & lim seq = lim (seq ^\ k) )

proof 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 Nat st seq ^\ k is bounded

ex k being Nat st seq ^\ k is bounded

proof end;

theorem Th19: :: RINFSUP2:19

for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds

ex k being Nat st seq ^\ k is bounded

ex k being Nat st seq ^\ k is bounded

proof end;

theorem Th20: :: RINFSUP2:20

for k being 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) )

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 end;

theorem :: RINFSUP2:21

for k being Nat

for seq being ExtREAL_sequence st seq is convergent holds

( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )

for seq being ExtREAL_sequence st seq is convergent holds

( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )

proof end;

theorem :: RINFSUP2:22

for k being 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 ) )

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 end;

theorem Th25: :: RINFSUP2:25

for k being Nat

for seq being ExtREAL_sequence st seq is non-increasing holds

( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )

for seq being ExtREAL_sequence st seq is non-increasing holds

( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )

proof end;

theorem Th26: :: RINFSUP2:26

for k being Nat

for seq being ExtREAL_sequence st seq is non-decreasing holds

( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) )

for seq being ExtREAL_sequence st seq is non-decreasing holds

( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) )

proof end;

theorem :: RINFSUP2:27

for n being Nat

for seq being ExtREAL_sequence holds

( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )

for seq being ExtREAL_sequence holds

( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )

proof 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 )

for j being Element of NAT holds

( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq )

proof 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 )

for j being Element of NAT holds

( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )

proof 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 )

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 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 )

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

seq is convergent_to_+infty

proof 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

seq is convergent_to_-infty

proof 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 )

( seq is convergent_to_-infty & lim seq = -infty )

proof 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 )

( seq is convergent_to_+infty & lim seq = +infty )

proof end;

theorem Th36: :: RINFSUP2:36

for seq being ExtREAL_sequence st seq is non-increasing holds

( seq is convergent & lim seq = inf seq )

( seq is convergent & lim seq = inf seq )

proof end;

theorem Th37: :: RINFSUP2:37

for seq being ExtREAL_sequence st seq is non-decreasing holds

( seq is convergent & lim seq = sup seq )

( seq is convergent & lim seq = sup seq )

proof end;

theorem Th38: :: RINFSUP2:38

for seq1, seq2 being ExtREAL_sequence st seq1 is convergent & seq2 is convergent & ( for n being Nat holds seq1 . n <= seq2 . n ) holds

lim seq1 <= lim seq2

lim seq1 <= lim seq2

proof 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 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 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 end;

theorem :: RINFSUP2:41

for seq being ExtREAL_sequence st seq is convergent holds

( lim seq = lim_inf seq & lim seq = lim_sup seq )

( lim seq = lim_inf seq & lim seq = lim_sup seq )

proof end;