The abstract of the Mizar article:

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;