LIMFUNC1: The Limit of a Real Function at Infinity. Halflines. Real Sequence Divergent to Infinity

:: The Limit of a Real Function at Infinity. Halflines. Real Sequence Divergent to Infinity
:: by Jaros{\l}aw Kotowicz
::
:: Received August 20, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users

begin

Lm1: for g, r, r1 being real number st 0 < g & r <= r1 holds
( r - g < r1 & r < r1 + g )

proof end;

Lm2: for seq being Real_Sequence
for f1, f2 being PartFunc of REAL,REAL st rng seq c= dom (f1 + f2) holds
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )

proof end;

Lm3: for seq being Real_Sequence
for f1, f2 being PartFunc of REAL,REAL st rng seq c= dom (f1 (#) f2) holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )

proof end;

notation

let r be real number ;
synonym left_open_halfline r for halfline r;

end;

definition

let r be real number ;

func left_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 1
].-infty,r.];

coherence

proof end;

func right_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 2
[.r,+infty.[;

coherence

proof end;

func right_open_halfline r -> Subset of REAL equals :: LIMFUNC1:def 3
].r,+infty.[;

coherence

proof end;

end;

:: deftheorem defines left_closed_halfline LIMFUNC1:def 1 :

:: deftheorem defines right_closed_halfline LIMFUNC1:def 2 :

:: deftheorem defines right_open_halfline LIMFUNC1:def 3 :

theorem :: LIMFUNC1:1

for seq being Real_Sequence holds
( ( seq is non-decreasing implies seq is bounded_below ) & ( seq is non-increasing implies seq is bounded_above ) )

proof end;

theorem Th2: :: LIMFUNC1:2

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

proof end;

theorem Th3: :: LIMFUNC1:3

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

proof end;

theorem Th4: :: LIMFUNC1:4

for seq being Real_Sequence st seq is convergent & 0 < lim seq holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
0 < seq . m

proof end;

theorem Th5: :: LIMFUNC1:5

for seq being Real_Sequence st seq is convergent & 0 < lim seq holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(lim seq) / 2 < seq . m

proof end;

definition

let seq be Real_Sequence;

attr seq is divergent_to+infty means :Def4: :: LIMFUNC1:def 4
for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < seq . m;

attr seq is divergent_to-infty means :Def5: :: LIMFUNC1:def 5
for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m < r;

end;

:: deftheorem Def4 defines divergent_to+infty LIMFUNC1:def 4 :

:: deftheorem Def5 defines divergent_to-infty LIMFUNC1:def 5 :

theorem :: LIMFUNC1:6

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq ^\ m is non-zero

proof end;

theorem Th7: :: LIMFUNC1:7

for k being Element of NAT
for seq being Real_Sequence holds
( ( seq ^\ k is divergent_to+infty implies seq is divergent_to+infty ) & ( seq ^\ k is divergent_to-infty implies seq is divergent_to-infty ) )

proof end;

theorem Th8: :: LIMFUNC1:8

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds
seq1 + seq2 is divergent_to+infty

proof end;

theorem Th9: :: LIMFUNC1:9

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is bounded_below holds
seq1 + seq2 is divergent_to+infty

proof end;

theorem Th10: :: LIMFUNC1:10

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds
seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th11: :: LIMFUNC1:11

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds
seq1 + seq2 is divergent_to-infty

proof end;

theorem Th12: :: LIMFUNC1:12

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is bounded_above holds
seq1 + seq2 is divergent_to-infty

proof end;

theorem Th13: :: LIMFUNC1:13

for seq being Real_Sequence
for r being Real holds
( ( seq is divergent_to+infty & r > 0 implies r (#) seq is divergent_to+infty ) & ( seq is divergent_to+infty & r < 0 implies r (#) seq is divergent_to-infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )

proof end;

theorem Th14: :: LIMFUNC1:14

for seq being Real_Sequence
for r being Real holds
( ( seq is divergent_to-infty & r > 0 implies r (#) seq is divergent_to-infty ) & ( seq is divergent_to-infty & r < 0 implies r (#) seq is divergent_to+infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )

proof end;

theorem :: LIMFUNC1:15

for seq being Real_Sequence holds
( ( seq is divergent_to+infty implies - seq is divergent_to-infty ) & ( seq is divergent_to-infty implies - seq is divergent_to+infty ) )

proof end;

theorem :: LIMFUNC1:16

for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is divergent_to-infty holds
seq - seq1 is divergent_to+infty

proof end;

theorem :: LIMFUNC1:17

for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is divergent_to+infty holds
seq - seq1 is divergent_to-infty

proof end;

theorem :: LIMFUNC1:18

for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is convergent holds
seq + seq1 is divergent_to+infty by Th9;

theorem :: LIMFUNC1:19

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is convergent holds
seq + seq1 is divergent_to-infty by Th12;

theorem Th20: :: LIMFUNC1:20

for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = n ) holds
seq is divergent_to+infty

proof end;

set s1 = incl NAT;

Lm4: for n being Element of NAT holds (incl NAT) . n = n
by FUNCT_1:18;

theorem Th21: :: LIMFUNC1:21

for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = - n ) holds
seq is divergent_to-infty

proof end;

theorem Th22: :: LIMFUNC1:22

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & ex r being Real st
( r > 0 & ( for n being Element of NAT holds seq2 . n >= r ) ) holds
seq1 (#) seq2 is divergent_to+infty

proof end;

theorem :: LIMFUNC1:23

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & ex r being Real st
( 0 < r & ( for n being Element of NAT holds seq2 . n >= r ) ) holds
seq1 (#) seq2 is divergent_to-infty

proof end;

theorem Th24: :: LIMFUNC1:24

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds
seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th25: :: LIMFUNC1:25

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
abs seq is divergent_to+infty

proof end;

theorem Th26: :: LIMFUNC1:26

for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is subsequence of seq holds
seq1 is divergent_to+infty

proof end;

theorem Th27: :: LIMFUNC1:27

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is subsequence of seq holds
seq1 is divergent_to-infty

proof end;

theorem :: LIMFUNC1:28

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is convergent & 0 < lim seq2 holds
seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th29: :: LIMFUNC1:29

for seq being Real_Sequence st seq is non-decreasing & not seq is bounded_above holds
seq is divergent_to+infty

proof end;

theorem Th30: :: LIMFUNC1:30

for seq being Real_Sequence st seq is non-increasing & not seq is bounded_below holds
seq is divergent_to-infty

proof end;

theorem :: LIMFUNC1:31

for seq being Real_Sequence st seq is increasing & not seq is bounded_above holds
seq is divergent_to+infty by Th29;

theorem :: LIMFUNC1:32

for seq being Real_Sequence st seq is decreasing & not seq is bounded_below holds
seq is divergent_to-infty by Th30;

theorem :: LIMFUNC1:33

for seq being Real_Sequence holds
( not seq is monotone or seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

proof end;

theorem Th34: :: LIMFUNC1:34

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
( seq " is convergent & lim (seq ") = 0 )

proof end;

theorem Th35: :: LIMFUNC1:35

for seq being Real_Sequence st seq is convergent & lim seq = 0 & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
0 < seq . n holds
seq " is divergent_to+infty

proof end;

theorem Th36: :: LIMFUNC1:36

for seq being Real_Sequence st seq is convergent & lim seq = 0 & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq . n < 0 holds
seq " is divergent_to-infty

proof end;

theorem Th37: :: LIMFUNC1:37

for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing holds
seq " is divergent_to-infty

proof end;

theorem Th38: :: LIMFUNC1:38

for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing holds
seq " is divergent_to+infty

proof end;

theorem :: LIMFUNC1:39

for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is increasing holds
seq " is divergent_to-infty by Th37;

theorem :: LIMFUNC1:40

for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is decreasing holds
seq " is divergent_to+infty by Th38;

theorem :: LIMFUNC1:41

for seq1, seq2 being Real_Sequence st seq1 is bounded & ( seq2 is divergent_to+infty or seq2 is divergent_to-infty ) holds
( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 )

proof end;

theorem Th42: :: LIMFUNC1:42

for seq, seq1 being Real_Sequence st seq is divergent_to+infty & ( for n being Element of NAT holds seq . n <= seq1 . n ) holds
seq1 is divergent_to+infty

proof end;

theorem Th43: :: LIMFUNC1:43

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & ( for n being Element of NAT holds seq1 . n <= seq . n ) holds
seq1 is divergent_to-infty

proof end;

definition

let f be PartFunc of REAL,REAL;

attr f is convergent_in+infty means :Def6: :: LIMFUNC1:def 6
( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex g being Real st
for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g ) );

attr f is divergent_in+infty_to+infty means :Def7: :: LIMFUNC1:def 7
( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f /* seq is divergent_to+infty ) );

attr f is divergent_in+infty_to-infty means :Def8: :: LIMFUNC1:def 8
( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f /* seq is divergent_to-infty ) );

attr f is convergent_in-infty means :Def9: :: LIMFUNC1:def 9
( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex g being Real st
for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g ) );

attr f is divergent_in-infty_to+infty means :Def10: :: LIMFUNC1:def 10
( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
f /* seq is divergent_to+infty ) );

attr f is divergent_in-infty_to-infty means :Def11: :: LIMFUNC1:def 11
( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
f /* seq is divergent_to-infty ) );

end;

:: deftheorem Def6 defines convergent_in+infty LIMFUNC1:def 6 :

:: deftheorem Def7 defines divergent_in+infty_to+infty LIMFUNC1:def 7 :

:: deftheorem Def8 defines divergent_in+infty_to-infty LIMFUNC1:def 8 :

:: deftheorem Def9 defines convergent_in-infty LIMFUNC1:def 9 :

:: deftheorem Def10 defines divergent_in-infty_to+infty LIMFUNC1:def 10 :

:: deftheorem Def11 defines divergent_in-infty_to-infty LIMFUNC1:def 11 :

theorem :: LIMFUNC1:44

for f being PartFunc of REAL,REAL holds
( f is convergent_in+infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) )

proof end;

theorem :: LIMFUNC1:45

for f being PartFunc of REAL,REAL holds
( f is convergent_in-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 ) )

proof end;

theorem :: LIMFUNC1:46

for f being PartFunc of REAL,REAL holds
( f is divergent_in+infty_to+infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
g < f . r1 ) ) )

proof end;

theorem :: LIMFUNC1:47

for f being PartFunc of REAL,REAL holds
( f is divergent_in+infty_to-infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
f . r1 < g ) ) )

proof end;

theorem :: LIMFUNC1:48

for f being PartFunc of REAL,REAL holds
( f is divergent_in-infty_to+infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
g < f . r1 ) ) )

proof end;

theorem :: LIMFUNC1:49

for f being PartFunc of REAL,REAL holds
( f is divergent_in-infty_to-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g ) ) )

proof end;

theorem :: LIMFUNC1:50

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in+infty_to+infty & f1 (#) f2 is divergent_in+infty_to+infty )

proof end;

theorem :: LIMFUNC1:51

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in+infty_to-infty & f1 (#) f2 is divergent_in+infty_to+infty )

proof end;

theorem :: LIMFUNC1:52

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & f2 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in-infty_to+infty & f1 (#) f2 is divergent_in-infty_to+infty )

proof end;

theorem :: LIMFUNC1:53

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in-infty_to-infty & f1 (#) f2 is divergent_in-infty_to+infty )

proof end;

theorem :: LIMFUNC1:54

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (right_open_halfline r) is bounded_below holds
f1 + f2 is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:55

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & ( for g being Real st g in (dom f2) /\ (right_open_halfline r1) holds
r <= f2 . g ) ) holds
f1 (#) f2 is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:56

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded_below holds
f1 + f2 is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:57

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & ( for g being Real st g in (dom f2) /\ (left_open_halfline r1) holds
r <= f2 . g ) ) holds
f1 (#) f2 is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:58

for f being PartFunc of REAL,REAL
for r being Real holds
( ( f is divergent_in+infty_to+infty & r > 0 implies r (#) f is divergent_in+infty_to+infty ) & ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty ) )

proof end;

theorem :: LIMFUNC1:59

for f being PartFunc of REAL,REAL
for r being Real holds
( ( f is divergent_in-infty_to+infty & r > 0 implies r (#) f is divergent_in-infty_to+infty ) & ( f is divergent_in-infty_to+infty & r < 0 implies r (#) f is divergent_in-infty_to-infty ) & ( f is divergent_in-infty_to-infty & r > 0 implies r (#) f is divergent_in-infty_to-infty ) & ( f is divergent_in-infty_to-infty & r < 0 implies r (#) f is divergent_in-infty_to+infty ) )

proof end;

theorem :: LIMFUNC1:60

for f being PartFunc of REAL,REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) holds
abs f is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:61

for f being PartFunc of REAL,REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) holds
abs f is divergent_in-infty_to+infty

proof end;

theorem Th62: :: LIMFUNC1:62

for f being PartFunc of REAL,REAL st ex r being Real st
( f | (right_open_halfline r) is non-decreasing & not f | (right_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:63

for f being PartFunc of REAL,REAL st ex r being Real st
( f | (right_open_halfline r) is increasing & not f | (right_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to+infty by Th62;

theorem Th64: :: LIMFUNC1:64

for f being PartFunc of REAL,REAL st ex r being Real st
( f | (right_open_halfline r) is non-increasing & not f | (right_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to-infty

proof end;

theorem :: LIMFUNC1:65

for f being PartFunc of REAL,REAL st ex r being Real st
( f | (right_open_halfline r) is decreasing & not f | (right_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to-infty by Th64;

theorem Th66: :: LIMFUNC1:66

for f being PartFunc of REAL,REAL st ex r being Real st
( f | (left_open_halfline r) is non-increasing & not f | (left_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:67

for f being PartFunc of REAL,REAL st ex r being Real st
( f | (left_open_halfline r) is decreasing & not f | (left_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to+infty by Th66;

theorem Th68: :: LIMFUNC1:68

for f being PartFunc of REAL,REAL st ex r being Real st
( f | (left_open_halfline r) is non-decreasing & not f | (left_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to-infty

proof end;

theorem :: LIMFUNC1:69

for f being PartFunc of REAL,REAL st ex r being Real st
( f | (left_open_halfline r) is increasing & not f | (left_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to-infty by Th68;

theorem Th70: :: LIMFUNC1:70

for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f1 . g <= f . g ) ) holds
f is divergent_in+infty_to+infty

proof end;

theorem Th71: :: LIMFUNC1:71

for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g <= f1 . g ) ) holds
f is divergent_in+infty_to-infty

proof end;

theorem Th72: :: LIMFUNC1:72

for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex r being Real st
( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f1 . g <= f . g ) ) holds
f is divergent_in-infty_to+infty

proof end;

theorem Th73: :: LIMFUNC1:73

for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex r being Real st
( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g <= f1 . g ) ) holds
f is divergent_in-infty_to-infty

proof end;

theorem :: LIMFUNC1:74

for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ex r being Real st
( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds
f1 . g <= f . g ) ) holds
f is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:75

for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & ex r being Real st
( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds
f . g <= f1 . g ) ) holds
f is divergent_in+infty_to-infty

proof end;

theorem :: LIMFUNC1:76

for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ex r being Real st
( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds
f1 . g <= f . g ) ) holds
f is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:77

for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & ex r being Real st
( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds
f . g <= f1 . g ) ) holds
f is divergent_in-infty_to-infty

proof end;

definition

let f be PartFunc of REAL,REAL;
assume A1: f is convergent_in+infty ;

func lim_in+infty f -> Real means :Def12: :: LIMFUNC1:def 12
for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = it );

existence by A1, Def6;
uniqueness

proof end;

end;

:: deftheorem Def12 defines lim_in+infty LIMFUNC1:def 12 :

definition

let f be PartFunc of REAL,REAL;
assume A1: f is convergent_in-infty ;

func lim_in-infty f -> Real means :Def13: :: LIMFUNC1:def 13
for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = it );

existence by A1, Def9;
uniqueness

proof end;

end;

:: deftheorem Def13 defines lim_in-infty LIMFUNC1:def 13 :

theorem :: LIMFUNC1:78

for f being PartFunc of REAL,REAL
for g being Real st f is convergent_in-infty holds
( lim_in-infty f = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 )

proof end;

theorem :: LIMFUNC1:79

for f being PartFunc of REAL,REAL
for g being Real st f is convergent_in+infty holds
( lim_in+infty f = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 )

proof end;

theorem Th80: :: LIMFUNC1:80

for f being PartFunc of REAL,REAL
for r being Real st f is convergent_in+infty holds
( r (#) f is convergent_in+infty & lim_in+infty (r (#) f) = r * (lim_in+infty f) )

proof end;

theorem Th81: :: LIMFUNC1:81

for f being PartFunc of REAL,REAL st f is convergent_in+infty holds
( - f is convergent_in+infty & lim_in+infty (- f) = - (lim_in+infty f) )

proof end;

theorem Th82: :: LIMFUNC1:82

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) ) ) holds
( f1 + f2 is convergent_in+infty & lim_in+infty (f1 + f2) = (lim_in+infty f1) + (lim_in+infty f2) )

proof end;

theorem :: LIMFUNC1:83

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 - f2) ) ) holds
( f1 - f2 is convergent_in+infty & lim_in+infty (f1 - f2) = (lim_in+infty f1) - (lim_in+infty f2) )

proof end;

theorem :: LIMFUNC1:84

for f being PartFunc of REAL,REAL st f is convergent_in+infty & f " {0} = {} & lim_in+infty f <> 0 holds
( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " )

proof end;

theorem :: LIMFUNC1:85

for f being PartFunc of REAL,REAL st f is convergent_in+infty holds
( abs f is convergent_in+infty & lim_in+infty (abs f) = abs (lim_in+infty f) )

proof end;

theorem Th86: :: LIMFUNC1:86

for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f <> 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " )

proof end;

theorem Th87: :: LIMFUNC1:87

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) holds
( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = (lim_in+infty f1) * (lim_in+infty f2) )

proof end;

theorem :: LIMFUNC1:88

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2 <> 0 & ( for r being Real ex g being Real st
( r < g & g in dom (f1 / f2) ) ) holds
( f1 / f2 is convergent_in+infty & lim_in+infty (f1 / f2) = (lim_in+infty f1) / (lim_in+infty f2) )

proof end;

theorem Th89: :: LIMFUNC1:89

for f being PartFunc of REAL,REAL
for r being Real st f is convergent_in-infty holds
( r (#) f is convergent_in-infty & lim_in-infty (r (#) f) = r * (lim_in-infty f) )

proof end;

theorem Th90: :: LIMFUNC1:90

for f being PartFunc of REAL,REAL st f is convergent_in-infty holds
( - f is convergent_in-infty & lim_in-infty (- f) = - (lim_in-infty f) )

proof end;

theorem Th91: :: LIMFUNC1:91

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) ) ) holds
( f1 + f2 is convergent_in-infty & lim_in-infty (f1 + f2) = (lim_in-infty f1) + (lim_in-infty f2) )

proof end;

theorem :: LIMFUNC1:92

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 - f2) ) ) holds
( f1 - f2 is convergent_in-infty & lim_in-infty (f1 - f2) = (lim_in-infty f1) - (lim_in-infty f2) )

proof end;

theorem :: LIMFUNC1:93

for f being PartFunc of REAL,REAL st f is convergent_in-infty & f " {0} = {} & lim_in-infty f <> 0 holds
( f ^ is convergent_in-infty & lim_in-infty (f ^) = (lim_in-infty f) " )

proof end;

theorem :: LIMFUNC1:94

for f being PartFunc of REAL,REAL st f is convergent_in-infty holds
( abs f is convergent_in-infty & lim_in-infty (abs f) = abs (lim_in-infty f) )

proof end;

theorem Th95: :: LIMFUNC1:95

for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f <> 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in-infty & lim_in-infty (f ^) = (lim_in-infty f) " )

proof end;

theorem Th96: :: LIMFUNC1:96

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) holds
( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = (lim_in-infty f1) * (lim_in-infty f2) )

proof end;

theorem :: LIMFUNC1:97

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f2 <> 0 & ( for r being Real ex g being Real st
( g < r & g in dom (f1 / f2) ) ) holds
( f1 / f2 is convergent_in-infty & lim_in-infty (f1 / f2) = (lim_in-infty f1) / (lim_in-infty f2) )

proof end;

theorem :: LIMFUNC1:98

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & lim_in+infty f1 = 0 & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 | (right_open_halfline r) is bounded holds
( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = 0 )

proof end;

theorem :: LIMFUNC1:99

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & lim_in-infty f1 = 0 & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded holds
( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 )

proof end;

theorem Th100: :: LIMFUNC1:100

proof end;

theorem :: LIMFUNC1:101

for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ex r being Real st
( right_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in right_open_halfline r holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )

proof end;

theorem Th102: :: LIMFUNC1:102

for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex r being Real st
( ( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )

proof end;

theorem :: LIMFUNC1:103

for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 & ex r being Real st
( left_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in left_open_halfline r holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )

proof end;

theorem :: LIMFUNC1:104

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ex r being Real st
( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & ( for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f2) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) ) holds
lim_in+infty f1 <= lim_in+infty f2

proof end;

theorem :: LIMFUNC1:105

for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ex r being Real st
( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) holds
lim_in-infty f1 <= lim_in-infty f2

proof end;

theorem :: LIMFUNC1:106

for f being PartFunc of REAL,REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in+infty & lim_in+infty (f ^) = 0 )

proof end;

theorem :: LIMFUNC1:107

for f being PartFunc of REAL,REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in-infty & lim_in-infty (f ^) = 0 )

proof end;

theorem :: LIMFUNC1:108

for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
0 <= f . g holds
f ^ is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:109

for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g <= 0 holds
f ^ is divergent_in+infty_to-infty

proof end;

theorem :: LIMFUNC1:110

for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
0 <= f . g holds
f ^ is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:111

for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g <= 0 holds
f ^ is divergent_in-infty_to-infty

proof end;

theorem :: LIMFUNC1:112

for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
0 < f . g holds
f ^ is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:113

for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g < 0 holds
f ^ is divergent_in+infty_to-infty

proof end;

theorem :: LIMFUNC1:114

for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
0 < f . g holds
f ^ is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:115

for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g < 0 holds
f ^ is divergent_in-infty_to-infty

proof end;