Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### The One-Side Limits of a Real Function at a Point

by
Jaroslaw Kotowicz

Received August 20, 1990

MML identifier: LIMFUNC2
[ Mizar article, MML identifier index ]

```environ

vocabulary SEQ_1, PARTFUN1, ARYTM, ARYTM_1, RELAT_1, BOOLE, ARYTM_3, SEQ_2,
ORDINAL2, FUNCT_1, SEQM_3, LIMFUNC1, RCOMP_1, ABSVALUE, RFUNCT_1,
RFUNCT_2, FINSEQ_1, LATTICES, LIMFUNC2;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, RELSET_1, RCOMP_1,
PARTFUN1, RFUNCT_1, RFUNCT_2, LIMFUNC1;
constructors REAL_1, NAT_1, ABSVALUE, SEQ_2, SEQM_3, PROB_1, RCOMP_1,
RFUNCT_1, RFUNCT_2, LIMFUNC1, PARTFUN1, MEMBERED, XBOOLE_0;
clusters RELSET_1, XREAL_0, SEQ_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve r,r1,r2,g,g1,g2,x0 for Real;
reserve n,k for Nat;
reserve seq for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;

theorem :: LIMFUNC2:1
seq is convergent & r<lim seq implies ex n st for k st n<=k holds r<seq.k;

theorem :: LIMFUNC2:2
seq is convergent & lim seq<r implies ex n st for k st n<=k holds seq.k<r;

theorem :: LIMFUNC2:3
0<r2 & ].r1-r2,r1.[ c= dom f implies
for r st r<r1 ex g st r<g & g<r1 & g in dom f;

theorem :: LIMFUNC2:4
0<r2 & ].r1,r1+r2.[ c= dom f implies
for r st r1<r ex g st g<r & r1<g & g in dom f;

theorem :: LIMFUNC2:5
(for n holds x0-1/(n+1)<seq.n & seq.n<x0 & seq.n in dom f) implies
seq is convergent & lim seq=x0 & rng seq c= dom f &
rng seq c= dom f /\ left_open_halfline(x0);

theorem :: LIMFUNC2:6
(for n holds x0<seq.n & seq.n<x0+1/(n+1) & seq.n in dom f) implies
seq is convergent & lim seq=x0 & rng seq c= dom f &
rng seq c= dom f /\ right_open_halfline(x0);

definition let f,x0;
pred f is_left_convergent_in x0 means
:: LIMFUNC2:def 1
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
ex g st for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ left_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=g;
pred f is_left_divergent_to+infty_in x0 means
:: LIMFUNC2:def 2
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ left_open_halfline(x0) holds f*seq is divergent_to+infty;
pred f is_left_divergent_to-infty_in x0 means
:: LIMFUNC2:def 3
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ left_open_halfline(x0) holds f*seq is divergent_to-infty;
pred f is_right_convergent_in x0 means
:: LIMFUNC2:def 4
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
ex g st for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ right_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=g;
pred f is_right_divergent_to+infty_in x0 means
:: LIMFUNC2:def 5
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\
right_open_halfline(x0) holds f*seq is divergent_to+infty;
pred f is_right_divergent_to-infty_in x0 means
:: LIMFUNC2:def 6
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\
right_open_halfline(x0) holds f*seq is divergent_to-infty;
end;

canceled 6;

theorem :: LIMFUNC2:13
f is_left_convergent_in x0 iff
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
ex g st for g1 st 0<g1 ex r st r<x0 &
for r1 st r<r1 & r1<x0 & r1 in dom f holds
abs(f.r1-g)<g1;

theorem :: LIMFUNC2:14
f is_left_divergent_to+infty_in x0 iff
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds g1<f.r1;

theorem :: LIMFUNC2:15
f is_left_divergent_to-infty_in x0 iff
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds f.r1<g1;

theorem :: LIMFUNC2:16
f is_right_convergent_in x0 iff
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
ex g st for g1 st 0<g1
ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds
abs(f.r1-g)<g1;

theorem :: LIMFUNC2:17
f is_right_divergent_to+infty_in x0 iff
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds g1<f.r1;

theorem :: LIMFUNC2:18
f is_right_divergent_to-infty_in x0 iff
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1;

theorem :: LIMFUNC2:19
f1 is_left_divergent_to+infty_in x0 & f2 is_left_divergent_to+infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f1 /\ dom f2) implies
f1+f2 is_left_divergent_to+infty_in x0 & f1(#)
f2 is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:20
f1 is_left_divergent_to-infty_in x0 & f2 is_left_divergent_to-infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f1 /\ dom f2) implies
f1+f2 is_left_divergent_to-infty_in x0 &
f1(#)f2 is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:21
f1 is_right_divergent_to+infty_in x0 & f2 is_right_divergent_to+infty_in x0
&
(for r st x0<r ex g st g<r & x0<g & g in dom f1 /\ dom f2) implies
f1+f2 is_right_divergent_to+infty_in x0 &
f1(#)f2 is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:22
f1 is_right_divergent_to-infty_in x0 & f2 is_right_divergent_to-infty_in x0
&
(for r st x0<r ex g st g<r & x0<g & g in dom f1 /\ dom f2) implies
f1+f2 is_right_divergent_to-infty_in x0 &
f1(#)f2 is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:23
f1 is_left_divergent_to+infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1+f2)) &
(ex r st 0<r & f2 is_bounded_below_on ].x0-r,x0.[) implies
f1+f2 is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:24
f1 is_left_divergent_to+infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2)) &
(ex r,r1 st 0<r & 0<r1 & for g st g in dom f2 /\ ].x0-r,x0.[ holds r1<=
f2.g) implies
f1(#)f2 is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:25
f1 is_right_divergent_to+infty_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1+f2)) &
(ex r st 0<r & f2 is_bounded_below_on ].x0,x0+r.[) implies
f1+f2 is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:26
f1 is_right_divergent_to+infty_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2)) &
(ex r,r1 st 0<r & 0<r1 & for g st g in dom f2 /\ ].x0,x0+r.[ holds r1<=
f2.g) implies
f1(#)f2 is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:27
(f is_left_divergent_to+infty_in x0 & r>0 implies
r(#)f is_left_divergent_to+infty_in x0 ) &
(f is_left_divergent_to+infty_in x0 & r<0 implies
r(#)f is_left_divergent_to-infty_in x0 ) &
(f is_left_divergent_to-infty_in x0 & r>0 implies
r(#)f is_left_divergent_to-infty_in x0 ) &
(f is_left_divergent_to-infty_in x0 & r<0 implies
r(#)f is_left_divergent_to+infty_in x0 );

theorem :: LIMFUNC2:28
(f is_right_divergent_to+infty_in x0 & r>0 implies
r(#)f is_right_divergent_to+infty_in x0 ) &
(f is_right_divergent_to+infty_in x0 & r<0 implies
r(#)f is_right_divergent_to-infty_in x0 ) &
(f is_right_divergent_to-infty_in x0 & r>0 implies
r(#)f is_right_divergent_to-infty_in x0 ) &
(f is_right_divergent_to-infty_in x0 & r<0 implies
r(#)f is_right_divergent_to+infty_in x0);

theorem :: LIMFUNC2:29
(f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0)
implies abs(f) is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:30
(f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0)
implies abs(f) is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:31
(ex r st 0<r & f is_non_decreasing_on ].x0-r,x0.[ &
not f is_bounded_above_on ].x0-r,x0.[) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies
f is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:32
(ex r st 0<r & f is_increasing_on ].x0-r,x0.[ &
not f is_bounded_above_on ].x0-r,x0.[) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies
f is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:33
(ex r st 0<r & f is_non_increasing_on ].x0-r,x0.[ &
not f is_bounded_below_on ].x0-r,x0.[) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies
f is_left_divergent_to-infty_in x0;

theorem :: LIMFUNC2:34
(ex r st 0<r & f is_decreasing_on ].x0-r,x0.[ &
not f is_bounded_below_on ].x0-r,x0.[) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies
f is_left_divergent_to-infty_in x0;

theorem :: LIMFUNC2:35
(ex r st 0<r & f is_non_increasing_on ].x0,x0+r.[ &
not f is_bounded_above_on ].x0,x0+r.[) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) implies
f is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:36
(ex r st 0<r & f is_decreasing_on ].x0,x0+r.[ &
not f is_bounded_above_on ].x0,x0+r.[) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) implies
f is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:37
(ex r st 0<r & f is_non_decreasing_on ].x0,x0+r.[ &
not f is_bounded_below_on ].x0,x0+r.[) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) implies
f is_right_divergent_to-infty_in x0;

theorem :: LIMFUNC2:38
(ex r st 0<r & f is_increasing_on ].x0,x0+r.[ &
not f is_bounded_below_on ].x0,x0+r.[) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) implies
f is_right_divergent_to-infty_in x0;

theorem :: LIMFUNC2:39
f1 is_left_divergent_to+infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f)
& (ex r st 0<r & dom f /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
for g st g in dom f /\ ].x0-r,x0.[ holds f1.g<=f.g) implies
f is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:40
f1 is_left_divergent_to-infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f)
& (ex r st 0<r & dom f /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
for g st g in dom f /\ ].x0-r,x0.[ holds f.g<=f1.g) implies
f is_left_divergent_to-infty_in x0;

theorem :: LIMFUNC2:41
f1 is_right_divergent_to+infty_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
(ex r st 0<r & dom f /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[ &
for g st g in dom f /\ ].x0,x0+r.[ holds f1.g<=f.g) implies
f is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:42
f1 is_right_divergent_to-infty_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
(ex r st 0<r & dom f /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[ &
for g st g in dom f /\ ].x0,x0+r.[ holds f.g<=f1.g) implies
f is_right_divergent_to-infty_in x0;

theorem :: LIMFUNC2:43
f1 is_left_divergent_to+infty_in x0 & (ex r st 0<r &
].x0-r,x0.[ c= dom f /\ dom f1 & for g st g in ].x0-r,x0.[ holds f1.g<=
f.g) implies
f is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:44
f1 is_left_divergent_to-infty_in x0 & (ex r st 0<r &
].x0-r,x0.[ c= dom f /\ dom f1 & for g st g in ].x0-r,x0.[ holds f.g<=
f1.g) implies
f is_left_divergent_to-infty_in x0;

theorem :: LIMFUNC2:45
f1 is_right_divergent_to+infty_in x0 & (ex r st 0<r &
].x0,x0+r.[ c= dom f /\ dom f1 & for g st g in ].x0,x0+r.[ holds f1.g<=
f.g) implies
f is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:46
f1 is_right_divergent_to-infty_in x0 & (ex r st 0<r &
].x0,x0+r.[ c= dom f /\ dom f1 & for g st g in ].x0,x0+r.[ holds f.g<=
f1.g) implies
f is_right_divergent_to-infty_in x0;

definition let f,x0;
assume  f is_left_convergent_in x0;
func lim_left(f,x0)->Real means
:: LIMFUNC2:def 7
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ left_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=it;
end;

definition let f,x0;
assume  f is_right_convergent_in x0;
func lim_right(f,x0)->Real means
:: LIMFUNC2:def 8
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ right_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=it;
end;

canceled 2;

theorem :: LIMFUNC2:49
f is_left_convergent_in x0 implies
(lim_left(f,x0)=g iff for g1 st 0<g1 ex r st r<x0 &
for r1 st r<r1 & r1<x0 & r1 in dom f holds abs(f.r1-g)<g1);

theorem :: LIMFUNC2:50
f is_right_convergent_in x0 implies
(lim_right(f,x0)=g iff for g1 st 0<g1 ex r st x0<r &
for r1 st r1<r & x0<r1 & r1 in dom f holds abs(f.r1-g)<g1);

theorem :: LIMFUNC2:51
f is_left_convergent_in x0 implies r(#)f is_left_convergent_in x0 &
lim_left(r(#)f,x0)=r*(lim_left(f,x0));

theorem :: LIMFUNC2:52
f is_left_convergent_in x0 implies -f is_left_convergent_in x0 &
lim_left(-f,x0)=-(lim_left(f,x0));

theorem :: LIMFUNC2:53
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1+f2)) implies
f1+f2 is_left_convergent_in x0 &
lim_left(f1+f2,x0)=lim_left(f1,x0)+lim_left(f2,x0);

theorem :: LIMFUNC2:54
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1-f2)) implies
f1-f2 is_left_convergent_in x0 &
lim_left(f1-f2,x0)=(lim_left(f1,x0))-(lim_left(f2,x0));

theorem :: LIMFUNC2:55
f is_left_convergent_in x0 & f"{0}={} & lim_left(f,x0)<>0 implies
f^ is_left_convergent_in x0 & lim_left(f^,x0)=(lim_left(f,x0))";

theorem :: LIMFUNC2:56
f is_left_convergent_in x0 implies abs(f) is_left_convergent_in x0 &
lim_left(abs(f),x0)=abs(lim_left(f,x0));

theorem :: LIMFUNC2:57
f is_left_convergent_in x0 & lim_left(f,x0)<>0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) implies
f^ is_left_convergent_in x0 & lim_left(f^,x0)=(lim_left(f,x0))";

theorem :: LIMFUNC2:58
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2)) implies
f1(#)f2 is_left_convergent_in x0 &
lim_left(f1(#)f2,x0)=(lim_left(f1,x0))*(lim_left(f2,x0));

theorem :: LIMFUNC2:59
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left(f2,x0)<>
0
& (for r st r<x0 ex g st r<g & g<x0 & g in dom(f1/f2)) implies
f1/f2 is_left_convergent_in x0 &
lim_left(f1/f2,x0)=(lim_left(f1,x0))/(lim_left(f2,x0));

theorem :: LIMFUNC2:60
f is_right_convergent_in x0 implies r(#)f is_right_convergent_in x0 &
lim_right(r(#)f,x0)=r*(lim_right(f,x0));

theorem :: LIMFUNC2:61
f is_right_convergent_in x0 implies -f is_right_convergent_in x0 &
lim_right(-f,x0)=-(lim_right(f,x0));

theorem :: LIMFUNC2:62
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1+f2)) implies
f1+f2 is_right_convergent_in x0 &
lim_right(f1+f2,x0)=(lim_right(f1,x0))+(lim_right(f2,x0));

theorem :: LIMFUNC2:63
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1-f2)) implies
f1-f2 is_right_convergent_in x0 &
lim_right(f1-f2,x0)=(lim_right(f1,x0))-(lim_right(f2,x0));

theorem :: LIMFUNC2:64
f is_right_convergent_in x0 & f"{0}={} & lim_right(f,x0)<>0 implies
f^ is_right_convergent_in x0 & lim_right(f^,x0)=(lim_right(f,x0))";

theorem :: LIMFUNC2:65
f is_right_convergent_in x0 implies abs(f) is_right_convergent_in x0 &
lim_right(abs(f),x0)=abs(lim_right(f,x0));

theorem :: LIMFUNC2:66
f is_right_convergent_in x0 & lim_right(f,x0)<>0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0) implies
f^ is_right_convergent_in x0 & lim_right(f^,x0)=(lim_right(f,x0))";

theorem :: LIMFUNC2:67
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2)) implies
f1(#)f2 is_right_convergent_in x0 &
lim_right(f1(#)f2,x0)=(lim_right(f1,x0))*(lim_right(f2,x0));

theorem :: LIMFUNC2:68
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f2,x0)<>0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1/f2)) implies
f1/f2 is_right_convergent_in x0 &
lim_right(f1/f2,x0)=(lim_right(f1,x0))/(lim_right(f2,x0));

theorem :: LIMFUNC2:69
f1 is_left_convergent_in x0 & lim_left(f1,x0)=0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2)) &
(ex r st 0<r & f2 is_bounded_on ].x0-r,x0.[) implies
f1(#)f2 is_left_convergent_in x0 & lim_left(f1(#)f2,x0)=0;

theorem :: LIMFUNC2:70
f1 is_right_convergent_in x0 & lim_right(f1,x0)=0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2)) &
(ex r st 0<r & f2 is_bounded_on ].x0,x0+r.[) implies
f1(#)f2 is_right_convergent_in x0 & lim_right(f1(#)f2,x0)=0;

theorem :: LIMFUNC2:71
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
lim_left(f1,x0)=lim_left(f2,x0) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f)
& (ex r st 0<r & (for g st g in dom f /\ ].x0-r,x0.[ holds
f1.g<=f.g & f.g<=f2.g) &
((dom f1 /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[ &
dom f /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[) or
(dom f2 /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
dom f /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[))) implies
f is_left_convergent_in x0 & lim_left(f,x0)=lim_left(f1,x0);

theorem :: LIMFUNC2:72
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
lim_left(f1,x0)=lim_left(f2,x0) & (ex r st 0<r &
].x0-r,x0.[ c= dom f1 /\ dom f2 /\ dom f &
for g st g in ].x0-r,x0.[ holds f1.g<=f.g & f.g<=f2.g) implies
f is_left_convergent_in x0 & lim_left(f,x0)=lim_left(f1,x0);

theorem :: LIMFUNC2:73
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f1,x0)=lim_right(f2,x0) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
(ex r st 0<r & (for g st g in dom f /\ ].x0,x0+r.[ holds
f1.g<=f.g & f.g<=f2.g) &
((dom f1 /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[ &
dom f /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[) or
(dom f2 /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[ &
dom f /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[))) implies
f is_right_convergent_in x0 & lim_right(f,x0)=lim_right(f1,x0);

theorem :: LIMFUNC2:74
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f1,x0)=lim_right(f2,x0) &
(ex r st 0<r & ].x0,x0+r.[ c= dom f1 /\ dom f2 /\ dom f &
for g st g in ].x0,x0+r.[ holds f1.g<=f.g & f.g<=f2.g) implies
f is_right_convergent_in x0 & lim_right(f,x0)=lim_right(f1,x0);

theorem :: LIMFUNC2:75
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & (ex r st 0<r &
((dom f1 /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[ &
for g st g in dom f1 /\ ].x0-r,x0.[ holds f1.g<=f2.g) or
(dom f2 /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
for g st g in dom f2 /\ ].x0-r,x0.[ holds f1.g<=f2.g))) implies
lim_left(f1,x0)<=lim_left(f2,x0);

theorem :: LIMFUNC2:76
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & (ex r st 0<r &
((dom f1 /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[ &
for g st g in dom f1 /\ ].x0,x0+r.[ holds f1.g<=f2.g) or
(dom f2 /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[ &
for g st g in dom f2 /\ ].x0,x0+r.[ holds f1.g<=f2.g))) implies
lim_right(f1,x0)<=lim_right(f2,x0);

theorem :: LIMFUNC2:77
(f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) implies
f^ is_left_convergent_in x0 & lim_left(f^,x0)=0;

theorem :: LIMFUNC2:78
(f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0)
&
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0) implies
f^ is_right_convergent_in x0 & lim_right(f^,x0)=0;

theorem :: LIMFUNC2:79
f is_left_convergent_in x0 & lim_left(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ ].x0-r,x0.[ holds 0<f.g) implies
f^ is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:80
f is_left_convergent_in x0 & lim_left(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ ].x0-r,x0.[ holds f.g<0) implies
f^ is_left_divergent_to-infty_in x0;

theorem :: LIMFUNC2:81
f is_right_convergent_in x0 & lim_right(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ ].x0,x0+r.[ holds 0<f.g) implies
f^ is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:82
f is_right_convergent_in x0 & lim_right(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ ].x0,x0+r.[ holds f.g<0) implies
f^ is_right_divergent_to-infty_in x0;

theorem :: LIMFUNC2:83
f is_left_convergent_in x0 & lim_left(f,x0)=0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) &
(ex r st 0<r & for g st g in dom f /\ ].x0-r,x0.[ holds 0<=f.g) implies
f^ is_left_divergent_to+infty_in x0;

theorem :: LIMFUNC2:84
f is_left_convergent_in x0 & lim_left(f,x0)=0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) &
(ex r st 0<r & for g st g in dom f /\ ].x0-r,x0.[ holds f.g<=0) implies
f^ is_left_divergent_to-infty_in x0;

theorem :: LIMFUNC2:85
f is_right_convergent_in x0 & lim_right(f,x0)=0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0) &
(ex r st 0<r & for g st g in dom f /\ ].x0,x0+r.[ holds 0<=f.g) implies
f^ is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC2:86
f is_right_convergent_in x0 & lim_right(f,x0)=0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0) &
(ex r st 0<r & for g st g in dom f /\ ].x0,x0+r.[ holds f.g<=0) implies
f^ is_right_divergent_to-infty_in x0;
```

Back to top