:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura

::

:: Received April 29, 2005

:: Copyright (c) 2005-2012 Association of Mizar Users

begin

Lm1: for r1, r2, s being real number st 0 < s & r1 <= r2 holds

( r1 < r2 + s & r1 - s < r2 )

proof end;

:: deftheorem defines upper_bound RINFSUP1:def 1 :

for seq being Real_Sequence holds upper_bound seq = upper_bound (rng seq);

for seq being Real_Sequence holds upper_bound seq = upper_bound (rng seq);

:: deftheorem defines lower_bound RINFSUP1:def 2 :

for seq being Real_Sequence holds lower_bound seq = lower_bound (rng seq);

for seq being Real_Sequence holds lower_bound seq = lower_bound (rng seq);

theorem Th7: :: RINFSUP1:7

for r being real number

for seq being Real_Sequence st seq is V88() holds

( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds

ex k being Element of NAT st r - s < seq . k ) ) )

for seq being Real_Sequence st seq is V88() holds

( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds

ex k being Element of NAT st r - s < seq . k ) ) )

proof end;

theorem Th8: :: RINFSUP1:8

for r being real number

for seq being Real_Sequence st seq is V89() holds

( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds

ex k being Element of NAT st seq . k < r + s ) ) )

for seq being Real_Sequence st seq is V89() holds

( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds

ex k being Element of NAT st seq . k < r + s ) ) )

proof end;

theorem Th9: :: RINFSUP1:9

for r being real number

for seq being Real_Sequence holds

( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() & upper_bound seq <= r ) )

for seq being Real_Sequence holds

( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() & upper_bound seq <= r ) )

proof end;

theorem Th10: :: RINFSUP1:10

for r being real number

for seq being Real_Sequence holds

( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() & r <= lower_bound seq ) )

for seq being Real_Sequence holds

( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() & r <= lower_bound seq ) )

proof end;

theorem Th15: :: RINFSUP1:15

for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds

lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2)

lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2)

proof end;

theorem Th16: :: RINFSUP1:16

for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds

upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)

upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)

proof end;

definition

let f be Real_Sequence;

( f is nonnegative iff for n being Element of NAT holds f . n >= 0 )

end;
redefine attr f is nonnegative-yielding means :Def3: :: RINFSUP1:def 3

for n being Element of NAT holds f . n >= 0 ;

compatibility for n being Element of NAT holds f . n >= 0 ;

( f is nonnegative iff for n being Element of NAT holds f . n >= 0 )

proof end;

:: deftheorem Def3 defines nonnegative RINFSUP1:def 3 :

for f being Real_Sequence holds

( f is nonnegative iff for n being Element of NAT holds f . n >= 0 );

for f being Real_Sequence holds

( f is nonnegative iff for n being Element of NAT holds f . n >= 0 );

theorem Th17: :: RINFSUP1:17

for k being Element of NAT

for seq being Real_Sequence st seq is nonnegative holds

seq ^\ k is nonnegative

for seq being Real_Sequence st seq is nonnegative holds

seq ^\ k is nonnegative

proof end;

theorem Th20: :: RINFSUP1:20

for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds

( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) )

( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) )

proof end;

theorem Th21: :: RINFSUP1:21

for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds

( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) )

( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) )

proof end;

theorem :: RINFSUP1:22

theorem :: RINFSUP1:23

theorem :: RINFSUP1:26

theorem :: RINFSUP1:27

theorem :: RINFSUP1:28

theorem Th29: :: RINFSUP1:29

for seq being Real_Sequence

for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL

for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL

proof end;

theorem Th30: :: RINFSUP1:30

for k being Element of NAT

for seq being Real_Sequence holds rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n }

for seq being Real_Sequence holds rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n }

proof end;

theorem Th31: :: RINFSUP1:31

for seq being Real_Sequence st seq is V88() holds

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

R is bounded_above

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

R is bounded_above

proof end;

theorem Th32: :: RINFSUP1:32

for seq being Real_Sequence st seq is V89() holds

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

R is bounded_below

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

R is bounded_below

proof end;

theorem Th33: :: RINFSUP1:33

for seq being Real_Sequence st seq is bounded holds

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

R is real-bounded

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

R is real-bounded

proof end;

theorem Th34: :: RINFSUP1:34

for seq being Real_Sequence st seq is V48() holds

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

lower_bound R = seq . n

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

lower_bound R = seq . n

proof end;

theorem Th35: :: RINFSUP1:35

for seq being Real_Sequence st seq is V49() holds

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

upper_bound R = seq . n

for n being Element of NAT

for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds

upper_bound R = seq . n

proof end;

definition

let seq be Real_Sequence;

ex b_{1} being Real_Sequence st

for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b_{1} . n = lower_bound Y

for b_{1}, b_{2} being Real_Sequence st ( for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b_{1} . n = lower_bound Y ) & ( for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b_{2} . n = lower_bound Y ) holds

b_{1} = b_{2}

end;
func inferior_realsequence seq -> Real_Sequence means :Def4: :: RINFSUP1:def 4

for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

it . n = lower_bound Y;

existence for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

it . n = lower_bound Y;

ex b

for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b

proof end;

uniqueness for b

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b

b

proof end;

:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def 4 :

for seq, b_{2} being Real_Sequence holds

( b_{2} = inferior_realsequence seq iff for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b_{2} . n = lower_bound Y );

for seq, b

( b

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b

definition

let seq be Real_Sequence;

ex b_{1} being Real_Sequence st

for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b_{1} . n = upper_bound Y

for b_{1}, b_{2} being Real_Sequence st ( for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b_{1} . n = upper_bound Y ) & ( for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b_{2} . n = upper_bound Y ) holds

b_{1} = b_{2}

end;
func superior_realsequence seq -> Real_Sequence means :Def5: :: RINFSUP1:def 5

for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

it . n = upper_bound Y;

existence for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

it . n = upper_bound Y;

ex b

for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b

proof end;

uniqueness for b

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b

b

proof end;

:: deftheorem Def5 defines superior_realsequence RINFSUP1:def 5 :

for seq, b_{2} being Real_Sequence holds

( b_{2} = superior_realsequence seq iff for n being Element of NAT

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b_{2} . n = upper_bound Y );

for seq, b

( b

for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds

b

theorem Th36: :: RINFSUP1:36

for n being Element of NAT

for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n)

for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n)

proof end;

theorem Th37: :: RINFSUP1:37

for n being Element of NAT

for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n)

for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n)

proof end;

theorem Th40: :: RINFSUP1:40

for n being Element of NAT

for r being real number

for seq being Real_Sequence st seq is V89() holds

( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds

ex k being Element of NAT st seq . (n + k) < r + s ) ) )

for r being real number

for seq being Real_Sequence st seq is V89() holds

( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds

ex k being Element of NAT st seq . (n + k) < r + s ) ) )

proof end;

theorem Th41: :: RINFSUP1:41

for n being Element of NAT

for r being real number

for seq being Real_Sequence st seq is V88() holds

( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds

ex k being Element of NAT st r - s < seq . (n + k) ) ) )

for r being real number

for seq being Real_Sequence st seq is V88() holds

( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds

ex k being Element of NAT st r - s < seq . (n + k) ) ) )

proof end;

theorem Th42: :: RINFSUP1:42

for n being Element of NAT

for r being real number

for seq being Real_Sequence st seq is V89() holds

( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )

for r being real number

for seq being Real_Sequence st seq is V89() holds

( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )

proof end;

theorem Th43: :: RINFSUP1:43

for n being Element of NAT

for r being real number

for seq being Real_Sequence st seq is V89() holds

( ( for m being Element of NAT st n <= m holds

r <= seq . m ) iff r <= (inferior_realsequence seq) . n )

for r being real number

for seq being Real_Sequence st seq is V89() holds

( ( for m being Element of NAT st n <= m holds

r <= seq . m ) iff r <= (inferior_realsequence seq) . n )

proof end;

theorem Th44: :: RINFSUP1:44

for n being Element of NAT

for r being real number

for seq being Real_Sequence st seq is V88() holds

( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )

for r being real number

for seq being Real_Sequence st seq is V88() holds

( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )

proof end;

theorem Th45: :: RINFSUP1:45

for n being Element of NAT

for r being real number

for seq being Real_Sequence st seq is V88() holds

( ( for m being Element of NAT st n <= m holds

seq . m <= r ) iff (superior_realsequence seq) . n <= r )

for r being real number

for seq being Real_Sequence st seq is V88() holds

( ( for m being Element of NAT st n <= m holds

seq . m <= r ) iff (superior_realsequence seq) . n <= r )

proof end;

theorem Th46: :: RINFSUP1:46

for n being Element of NAT

for seq being Real_Sequence st seq is V89() holds

(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))

for seq being Real_Sequence st seq is V89() holds

(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))

proof end;

theorem Th47: :: RINFSUP1:47

for n being Element of NAT

for seq being Real_Sequence st seq is V88() holds

(superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))

for seq being Real_Sequence st seq is V88() holds

(superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))

proof end;

theorem Th48: :: RINFSUP1:48

for n being Element of NAT

for seq being Real_Sequence st seq is V89() holds

(inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)

for seq being Real_Sequence st seq is V89() holds

(inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)

proof end;

theorem Th49: :: RINFSUP1:49

for n being Element of NAT

for seq being Real_Sequence st seq is V88() holds

(superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n

for seq being Real_Sequence st seq is V88() holds

(superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n

proof end;

theorem :: RINFSUP1:52

for n being Element of NAT

for seq being Real_Sequence st seq is bounded holds

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

for seq being Real_Sequence st seq is bounded holds

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

proof end;

theorem Th53: :: RINFSUP1:53

for n being Element of NAT

for seq being Real_Sequence st seq is bounded holds

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

for seq being Real_Sequence st seq is bounded holds

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

proof end;

theorem Th54: :: RINFSUP1:54

for n being Element of NAT

for seq being Real_Sequence st seq is bounded holds

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

for seq being Real_Sequence st seq is bounded holds

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

proof end;

theorem Th55: :: RINFSUP1:55

for seq being Real_Sequence st seq is bounded holds

upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)

upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)

proof end;

theorem Th56: :: RINFSUP1:56

for seq being Real_Sequence st seq is bounded holds

( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )

( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )

proof end;

theorem Th57: :: RINFSUP1:57

for seq being Real_Sequence st seq is bounded holds

( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) )

( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) )

proof end;

theorem Th58: :: RINFSUP1:58

for seq being Real_Sequence st seq is bounded holds

( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) )

( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) )

proof end;

theorem Th59: :: RINFSUP1:59

for n being Element of NAT

for seq being Real_Sequence st seq is V89() holds

(inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)

for seq being Real_Sequence st seq is V89() holds

(inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)

proof end;

theorem Th60: :: RINFSUP1:60

for n being Element of NAT

for seq being Real_Sequence st seq is V88() holds

(superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)

for seq being Real_Sequence st seq is V88() holds

(superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)

proof end;

theorem Th61: :: RINFSUP1:61

for seq being Real_Sequence st seq is V89() holds

inferior_realsequence seq = - (superior_realsequence (- seq))

inferior_realsequence seq = - (superior_realsequence (- seq))

proof end;

theorem Th62: :: RINFSUP1:62

for seq being Real_Sequence st seq is V88() holds

superior_realsequence seq = - (inferior_realsequence (- seq))

superior_realsequence seq = - (inferior_realsequence (- seq))

proof end;

theorem :: RINFSUP1:63

for n being Element of NAT

for seq being Real_Sequence st seq is V48() holds

seq . n <= (inferior_realsequence seq) . (n + 1)

for seq being Real_Sequence st seq is V48() holds

seq . n <= (inferior_realsequence seq) . (n + 1)

proof end;

Lm2: for n being Element of NAT

for seq being Real_Sequence st seq is V48() holds

(inferior_realsequence seq) . n = seq . n

proof end;

theorem Th65: :: RINFSUP1:65

for n being Element of NAT

for seq being Real_Sequence st seq is V48() & seq is V88() holds

seq . n <= (superior_realsequence seq) . (n + 1)

for seq being Real_Sequence st seq is V48() & seq is V88() holds

seq . n <= (superior_realsequence seq) . (n + 1)

proof end;

theorem Th66: :: RINFSUP1:66

for n being Element of NAT

for seq being Real_Sequence st seq is V48() & seq is V88() holds

(superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)

for seq being Real_Sequence st seq is V48() & seq is V88() holds

(superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)

proof end;

theorem Th67: :: RINFSUP1:67

for n being Element of NAT

for seq being Real_Sequence st seq is V48() & seq is V88() holds

( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )

for seq being Real_Sequence st seq is V48() & seq is V88() holds

( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )

proof end;

theorem :: RINFSUP1:68

for seq being Real_Sequence st seq is V48() & seq is V88() holds

lower_bound (superior_realsequence seq) = upper_bound seq

lower_bound (superior_realsequence seq) = upper_bound seq

proof end;

theorem :: RINFSUP1:69

for n being Element of NAT

for seq being Real_Sequence st seq is V49() holds

(superior_realsequence seq) . (n + 1) <= seq . n

for seq being Real_Sequence st seq is V49() holds

(superior_realsequence seq) . (n + 1) <= seq . n

proof end;

Lm3: for n being Element of NAT

for seq being Real_Sequence st seq is V49() holds

(superior_realsequence seq) . n = seq . n

proof end;

theorem Th71: :: RINFSUP1:71

for n being Element of NAT

for seq being Real_Sequence st seq is V49() & seq is V89() holds

(inferior_realsequence seq) . (n + 1) <= seq . n

for seq being Real_Sequence st seq is V49() & seq is V89() holds

(inferior_realsequence seq) . (n + 1) <= seq . n

proof end;

theorem Th72: :: RINFSUP1:72

for n being Element of NAT

for seq being Real_Sequence st seq is V49() & seq is V89() holds

(inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)

for seq being Real_Sequence st seq is V49() & seq is V89() holds

(inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)

proof end;

theorem Th73: :: RINFSUP1:73

for n being Element of NAT

for seq being Real_Sequence st seq is V49() & seq is V89() holds

( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )

for seq being Real_Sequence st seq is V49() & seq is V89() holds

( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )

proof end;

theorem :: RINFSUP1:74

for seq being Real_Sequence st seq is V49() & seq is V89() holds

upper_bound (inferior_realsequence seq) = lower_bound seq

upper_bound (inferior_realsequence seq) = lower_bound seq

proof end;

theorem Th75: :: RINFSUP1:75

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds

( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) )

( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) )

proof end;

theorem :: RINFSUP1:76

for n being Element of NAT

for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds

(inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)

for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds

(inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)

proof end;

theorem :: RINFSUP1:77

for n being Element of NAT

for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds

(superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)

for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds

(superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)

proof end;

theorem :: RINFSUP1:78

for n being Element of NAT

for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds

(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)

for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds

(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)

proof end;

theorem Th79: :: RINFSUP1:79

for n being Element of NAT

for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds

(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)

for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds

(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)

proof end;

theorem Th80: :: RINFSUP1:80

for n being Element of NAT

for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds

(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)

for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds

(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)

proof end;

definition

let seq be Real_Sequence;

lower_bound (superior_realsequence seq) is Element of REAL ;

end;
func lim_sup seq -> Element of REAL equals :: RINFSUP1:def 6

lower_bound (superior_realsequence seq);

coherence lower_bound (superior_realsequence seq);

lower_bound (superior_realsequence seq) is Element of REAL ;

:: deftheorem defines lim_sup RINFSUP1:def 6 :

for seq being Real_Sequence holds lim_sup seq = lower_bound (superior_realsequence seq);

for seq being Real_Sequence holds lim_sup seq = lower_bound (superior_realsequence seq);

definition

let seq be Real_Sequence;

upper_bound (inferior_realsequence seq) is Element of REAL ;

end;
func lim_inf seq -> Element of REAL equals :: RINFSUP1:def 7

upper_bound (inferior_realsequence seq);

coherence upper_bound (inferior_realsequence seq);

upper_bound (inferior_realsequence seq) is Element of REAL ;

:: deftheorem defines lim_inf RINFSUP1:def 7 :

for seq being Real_Sequence holds lim_inf seq = upper_bound (inferior_realsequence seq);

for seq being Real_Sequence holds lim_inf seq = upper_bound (inferior_realsequence seq);

theorem Th81: :: RINFSUP1:81

for r being real number

for seq being Real_Sequence st seq is bounded holds

( lim_inf seq <= r iff for s being real number st 0 < s holds

for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s )

for seq being Real_Sequence st seq is bounded holds

( lim_inf seq <= r iff for s being real number st 0 < s holds

for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s )

proof end;

theorem Th82: :: RINFSUP1:82

for r being real number

for seq being Real_Sequence st seq is bounded holds

( r <= lim_inf seq iff for s being real number st 0 < s holds

ex n being Element of NAT st

for k being Element of NAT holds r - s < seq . (n + k) )

for seq being Real_Sequence st seq is bounded holds

( r <= lim_inf seq iff for s being real number st 0 < s holds

ex n being Element of NAT st

for k being Element of NAT holds r - s < seq . (n + k) )

proof end;

theorem :: RINFSUP1:83

for r being real number

for seq being Real_Sequence st seq is bounded holds

( r = lim_inf seq iff for s being real number st 0 < s holds

( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st

for k being Element of NAT holds r - s < seq . (n + k) ) )

for seq being Real_Sequence st seq is bounded holds

( r = lim_inf seq iff for s being real number st 0 < s holds

( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st

for k being Element of NAT holds r - s < seq . (n + k) ) )

proof end;

theorem Th84: :: RINFSUP1:84

for r being real number

for seq being Real_Sequence st seq is bounded holds

( r <= lim_sup seq iff for s being real number st 0 < s holds

for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s )

for seq being Real_Sequence st seq is bounded holds

( r <= lim_sup seq iff for s being real number st 0 < s holds

for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s )

proof end;

theorem Th85: :: RINFSUP1:85

for r being real number

for seq being Real_Sequence st seq is bounded holds

( lim_sup seq <= r iff for s being real number st 0 < s holds

ex n being Element of NAT st

for k being Element of NAT holds seq . (n + k) < r + s )

for seq being Real_Sequence st seq is bounded holds

( lim_sup seq <= r iff for s being real number st 0 < s holds

ex n being Element of NAT st

for k being Element of NAT holds seq . (n + k) < r + s )

proof end;

theorem :: RINFSUP1:86

for r being real number

for seq being Real_Sequence st seq is bounded holds

( r = lim_sup seq iff for s being real number st 0 < s holds

( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st

for k being Element of NAT holds seq . (n + k) < r + s ) )

for seq being Real_Sequence st seq is bounded holds

( r = lim_sup seq iff for s being real number st 0 < s holds

( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st

for k being Element of NAT holds seq . (n + k) < r + s ) )

proof end;

theorem :: RINFSUP1:87

theorem Th88: :: RINFSUP1:88

for seq being Real_Sequence holds

( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent )

( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent )

proof end;

theorem :: RINFSUP1:89

for seq being Real_Sequence st seq is convergent holds

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

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

proof end;

theorem Th90: :: RINFSUP1:90

for seq being Real_Sequence st seq is bounded holds

( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) )

( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) )

proof end;

theorem :: RINFSUP1:91

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds

( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )

( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )

proof end;

theorem :: RINFSUP1:92

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds

( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) )

( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) )

proof end;

theorem :: RINFSUP1:93

for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds

( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )

( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )

proof end;