:: 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
].-infty,r.] is Subset of REAL
proof end;
func right_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 2
[.r,+infty.[;
coherence
[.r,+infty.[ is Subset of REAL
proof end;
func right_open_halfline r -> Subset of REAL equals :: LIMFUNC1:def 3
].r,+infty.[;
coherence
].r,+infty.[ is Subset of REAL
proof end;
end;

:: deftheorem defines left_closed_halfline LIMFUNC1:def 1 :
for r being real number holds left_closed_halfline r = ].-infty,r.];

:: deftheorem defines right_closed_halfline LIMFUNC1:def 2 :
for r being real number holds right_closed_halfline r = [.r,+infty.[;

:: deftheorem defines right_open_halfline LIMFUNC1:def 3 :
for r being real number holds right_open_halfline r = ].r,+infty.[;

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 :
for seq being Real_Sequence holds
( seq is divergent_to+infty iff for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < seq . m );

:: deftheorem Def5 defines divergent_to-infty LIMFUNC1:def 5 :
for seq being Real_Sequence holds
( seq is divergent_to-infty iff for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m < r );

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 :
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 seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g ) ) );

:: deftheorem Def7 defines divergent_in+infty_to+infty LIMFUNC1:def 7 :
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 seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f /* seq is divergent_to+infty ) ) );

:: deftheorem Def8 defines divergent_in+infty_to-infty LIMFUNC1:def 8 :
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 seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f /* seq is divergent_to-infty ) ) );

:: deftheorem Def9 defines convergent_in-infty LIMFUNC1:def 9 :
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 seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g ) ) );

:: deftheorem Def10 defines divergent_in-infty_to+infty LIMFUNC1:def 10 :
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 seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
f /* seq is divergent_to+infty ) ) );

:: deftheorem Def11 defines divergent_in-infty_to-infty LIMFUNC1:def 11 :
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 seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
f /* seq is divergent_to-infty ) ) );

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
ex b1 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) = b1 )
by A1, Def6;
uniqueness
for b1, b2 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) = b1 ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines lim_in+infty LIMFUNC1:def 12 :
for f being PartFunc of REAL,REAL st f is convergent_in+infty holds
for b2 being Real holds
( b2 = lim_in+infty f iff for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b2 ) );

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
ex b1 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) = b1 )
by A1, Def9;
uniqueness
for b1, b2 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) = b1 ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines lim_in-infty LIMFUNC1:def 13 :
for f being PartFunc of REAL,REAL st f is convergent_in-infty holds
for b2 being Real holds
( b2 = lim_in-infty f iff for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b2 ) );

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
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
( r < g & g in dom f ) ) & ex r being Real st
( ( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (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 :: 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;