:: Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990 Association of Mizar Users

theorem :: SEQ_4:1

canceled;

theorem :: SEQ_4:2

canceled;

theorem :: SEQ_4:3

canceled;

theorem :: SEQ_4:4

canceled;

theorem :: SEQ_4:5

canceled;

theorem :: SEQ_4:6

canceled;

theorem :: SEQ_4:7

canceled;

theorem Th8: :: SEQ_4:8

for X, Y being Subset of REAL st ( for r, p being real number st r in X & p in Y holds
r < p ) holds
ex g being real number st
for r, p being real number st r in X & p in Y holds
( r <= g & g <= p )

proof end;

theorem Th9: :: SEQ_4:9

for p being real number
for X being Subset of REAL st 0 < p & ex r being real number st r in X & ( for r being real number st r in X holds
r + p in X ) holds
for g being real number ex r being real number st
( r in X & g < r )

proof end;

theorem Th10: :: SEQ_4:10

for r being real number ex n being Element of NAT st r < n

proof end;

definition

let X be real-membered set ;
redefine attr X is bounded_above means :Def1: :: SEQ_4:def 1
ex p being real number st
for r being real number st r in X holds
r <= p;
compatibility
( X is bounded_above iff ex p being real number st
for r being real number st r in X holds
r <= p )

proof end;

redefine attr X is bounded_below means :Def2: :: SEQ_4:def 2
ex p being real number st
for r being real number st r in X holds
p <= r;
compatibility
( X is bounded_below iff ex p being real number st
for r being real number st r in X holds
p <= r )

proof end;

end;

:: deftheorem Def1 defines bounded_above SEQ_4:def 1 :

for X being real-membered set holds
( X is bounded_above iff ex p being real number st
for r being real number st r in X holds
r <= p );

:: deftheorem Def2 defines bounded_below SEQ_4:def 2 :

for X being real-membered set holds
( X is bounded_below iff ex p being real number st
for r being real number st r in X holds
p <= r );

theorem :: SEQ_4:11

canceled;

theorem :: SEQ_4:12

canceled;

theorem :: SEQ_4:13

canceled;

theorem :: SEQ_4:14

for X being Subset of REAL holds
( X is bounded iff ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) )

proof end;

definition

let r be real number ;
:: original: {
redefine func {r} -> Subset of REAL ;
coherence
{r} is Subset of REAL

proof end;

end;

theorem :: SEQ_4:15

canceled;

theorem Th16: :: SEQ_4:16

for X being real-membered set st not X is empty & X is bounded_above holds
ex g being real number st
( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) )

proof end;

theorem Th17: :: SEQ_4:17

for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
r <= g1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) ) & ( for r being real number st r in X holds
r <= g2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ) holds
g1 = g2

proof end;

theorem Th18: :: SEQ_4:18

for X being real-membered set st not X is empty & X is bounded_below holds
ex g being real number st
( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) )

proof end;

theorem Th19: :: SEQ_4:19

for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
g1 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g1 + s ) ) & ( for r being real number st r in X holds
g2 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g2 + s ) ) holds
g1 = g2

proof end;

definition

canceled;
let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_above ) ;
func upper_bound X -> real number means :Def4: :: SEQ_4:def 4
( ( for r being real number st r in X holds
r <= it ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & it - s < r ) ) );
existence
ex b₁ being real number st
( ( for r being real number st r in X holds
r <= b₁ ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & b₁ - s < r ) ) ) by A1, Th16;
uniqueness
for b₁, b₂ being real number st ( for r being real number st r in X holds
r <= b₁ ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & b₁ - s < r ) ) & ( for r being real number st r in X holds
r <= b₂ ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & b₂ - s < r ) ) holds
b₁ = b₂ by Th17;

end;

:: deftheorem SEQ_4:def 3 :

canceled;

:: deftheorem Def4 defines upper_bound SEQ_4:def 4 :

for X being real-membered set st not X is empty & X is bounded_above holds
for b₂ being real number holds
( b₂ = upper_bound X iff ( ( for r being real number st r in X holds
r <= b₂ ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & b₂ - s < r ) ) ) );

definition

let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_below ) ;
func lower_bound X -> real number means :Def5: :: SEQ_4:def 5
( ( for r being real number st r in X holds
it <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < it + s ) ) );
existence
ex b₁ being real number st
( ( for r being real number st r in X holds
b₁ <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < b₁ + s ) ) ) by A1, Th18;
uniqueness
for b₁, b₂ being real number st ( for r being real number st r in X holds
b₁ <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < b₁ + s ) ) & ( for r being real number st r in X holds
b₂ <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < b₂ + s ) ) holds
b₁ = b₂ by Th19;

end;

:: deftheorem Def5 defines lower_bound SEQ_4:def 5 :

for X being real-membered set st not X is empty & X is bounded_below holds
for b₂ being real number holds
( b₂ = lower_bound X iff ( ( for r being real number st r in X holds
b₂ <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < b₂ + s ) ) ) );

Lm61: for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X

proof end;

Lm63: for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X

proof end;

registration

let X be non empty real-membered bounded_below set ;
identify lower_bound X with inf X;
compatibility
lower_bound X = inf X

proof end;

end;

registration

let X be non empty real-membered bounded_above set ;
identify upper_bound X with sup X;
compatibility
upper_bound X = sup X

proof end;

end;

definition

let X be Subset of REAL ;
:: original: upper_bound
redefine func upper_bound X -> Real;
coherence
upper_bound X is Real by XREAL_0:def 1;
:: original: lower_bound
redefine func lower_bound X -> Real;
coherence
lower_bound X is Real by XREAL_0:def 1;

end;

theorem :: SEQ_4:20

canceled;

theorem :: SEQ_4:21

canceled;

theorem Th22: :: SEQ_4:22

for r being real number holds
( lower_bound {r} = r & upper_bound {r} = r ) by XXREAL_2:11, XXREAL_2:13;

theorem Th23: :: SEQ_4:23

for r being real number holds lower_bound {r} = upper_bound {r}

proof end;

theorem :: SEQ_4:24

for X being Subset of REAL st X is bounded & not X is empty holds
lower_bound X <= upper_bound X

proof end;

theorem :: SEQ_4:25

for X being Subset of REAL st X is bounded & not X is empty holds
( ex r, p being real number st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )

proof end;

theorem Th26: :: SEQ_4:26

for seq being Real_Sequence st seq is convergent holds
abs seq is convergent

proof end;

theorem :: SEQ_4:27

for seq being Real_Sequence st seq is convergent holds
lim (abs seq) = abs (lim seq)

proof end;

theorem :: SEQ_4:28

for seq being Real_Sequence st abs seq is convergent & lim (abs seq) = 0 holds
( seq is convergent & lim seq = 0 )

proof end;

theorem Th29: :: SEQ_4:29

for seq1, seq being Real_Sequence st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent

proof end;

theorem Th30: :: SEQ_4:30

for seq1, seq being Real_Sequence st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq

proof end;

theorem Th31: :: SEQ_4:31

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent

proof end;

theorem :: SEQ_4:32

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
lim seq = lim seq1

proof end;

registration

cluster V8() -> convergent Element of K21(K22(NAT ,REAL ));
coherence
for b₁ being Real_Sequence st b₁ is V8() holds
b₁ is convergent

proof end;

end;

registration

cluster V8() Element of K21(K22(NAT ,REAL ));
existence
not for b₁ being Real_Sequence holds b₁ is V8()

proof end;

end;

registration

let seq be convergent Real_Sequence;
let k be Element of NAT ;
cluster seq ^\ k -> convergent Real_Sequence;
coherence
for b₁ being Real_Sequence st b₁ = seq ^\ k holds
b₁ is convergent by Th29;

end;

theorem Th33: :: SEQ_4:33

for k being Element of NAT
for seq being Real_Sequence st seq is convergent holds
lim (seq ^\ k) = lim seq by Th30;

theorem :: SEQ_4:34

canceled;

theorem Th35: :: SEQ_4:35

for k being Element of NAT
for seq being Real_Sequence st seq ^\ k is convergent holds
seq is convergent

proof end;

theorem :: SEQ_4:36

for k being Element of NAT
for seq being Real_Sequence st seq ^\ k is convergent holds
lim seq = lim (seq ^\ k)

proof end;

theorem Th37: :: SEQ_4:37

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Element of NAT st seq ^\ k is non-zero

proof end;

theorem :: SEQ_4:38

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero )

proof end;

theorem :: SEQ_4:39

canceled;

theorem Th40: :: SEQ_4:40

for r being real number
for seq being Real_Sequence st ( ( seq is V8() & r in rng seq ) or ( seq is V8() & ex n being Element of NAT st seq . n = r ) ) holds
lim seq = r

proof end;

theorem :: SEQ_4:41

for seq being Real_Sequence st seq is V8() holds
for n being Element of NAT holds lim seq = seq . n by Th40;

theorem :: SEQ_4:42

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
for seq1 being Real_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 " ) = (lim seq) "

proof end;

theorem Th43: :: SEQ_4:43

for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
seq is convergent

proof end;

theorem Th44: :: SEQ_4:44

for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
lim seq = 0

proof end;

theorem :: SEQ_4:45

for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = 1 / (n + 1) ) holds
( seq is convergent & lim seq = 0 ) by Th43, Th44;

theorem :: SEQ_4:46

for r, g being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / (n + r) ) holds
( seq is convergent & lim seq = 0 )

proof end;

theorem Th47: :: SEQ_4:47

for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
seq is convergent

proof end;

theorem Th48: :: SEQ_4:48

for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0

proof end;

theorem :: SEQ_4:49

for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = 1 / ((n * n) + 1) ) holds
( seq is convergent & lim seq = 0 ) by Th47, Th48;

theorem :: SEQ_4:50

for r, g being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / ((n * n) + r) ) holds
( seq is convergent & lim seq = 0 )

proof end;

registration

cluster non-decreasing bounded_above -> convergent Element of K21(K22(NAT ,REAL ));
coherence
for b₁ being Real_Sequence st b₁ is non-decreasing & b₁ is bounded_above holds
b₁ is convergent

proof end;

end;

registration

cluster non-increasing bounded_below -> convergent Element of K21(K22(NAT ,REAL ));
coherence
for b₁ being Real_Sequence st b₁ is non-increasing & b₁ is bounded_below holds
b₁ is convergent

proof end;

end;

registration

cluster bounded monotone -> convergent Element of K21(K22(NAT ,REAL ));
coherence
for b₁ being Real_Sequence st b₁ is monotone & b₁ is bounded holds
b₁ is convergent

proof end;

end;

theorem :: SEQ_4:51

canceled;

theorem :: SEQ_4:52

canceled;

theorem Th53: :: SEQ_4:53

for seq being Real_Sequence st seq is monotone & seq is bounded holds
seq is convergent ;

theorem :: SEQ_4:54

for seq being Real_Sequence st seq is bounded_above & seq is non-decreasing holds
for n being Element of NAT holds seq . n <= lim seq

proof end;

theorem :: SEQ_4:55

for seq being Real_Sequence st seq is bounded_below & seq is non-increasing holds
for n being Element of NAT holds lim seq <= seq . n

proof end;

theorem Th56: :: SEQ_4:56

for seq being Real_Sequence ex Nseq being V33() sequence of NAT st seq * Nseq is monotone

proof end;

theorem Th57: :: SEQ_4:57

for seq being Real_Sequence st seq is bounded holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )

proof end;

theorem :: SEQ_4:58

for seq being Real_Sequence holds
( seq is convergent iff for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s )

proof end;

theorem :: SEQ_4:59

for seq, seq1 being Real_Sequence st seq is V8() & seq1 is convergent holds
( lim (seq + seq1) = (seq . 0 ) + (lim seq1) & lim (seq - seq1) = (seq . 0 ) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0 ) & lim (seq (#) seq1) = (seq . 0 ) * (lim seq1) )

proof end;

theorem Th60: :: SEQ_4:60

for X being non empty real-membered set
for t being real number st ( for s being real number st s in X holds
s >= t ) holds
lower_bound X >= t

proof end;

theorem :: SEQ_4:61

for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X by Lm61;

theorem Th62: :: SEQ_4:62

for X being non empty real-membered set
for r, t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t

proof end;

theorem :: SEQ_4:63

for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X by Lm63;

theorem :: SEQ_4:64

for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_below holds
lower_bound Y <= lower_bound X

proof end;

theorem :: SEQ_4:65

for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_above holds
upper_bound X <= upper_bound Y

proof end;

definition

let A be non empty natural-membered set ;
:: original: inf
redefine func min A -> Element of NAT ;
coherence
inf A is Element of NAT by ORDINAL1:def 13;

end;

scheme :: SEQ_4:sch 1
MinPred{ F₁( Element of NAT ) -> Element of NAT , P₁[ set ] } :

ex k being Element of NAT st
( P₁[k] & ( for n being Element of NAT st P₁[n] holds
k <= n ) )

provided

A1: for k being Element of NAT holds
( F₁((k + 1)) < F₁(k) or P₁[k] )

proof end;