The abstract of the Mizar article:

The Limit of a Real Function at a Point

by

Jaroslaw Kotowicz

Received September 5, 1990

MML identifier: LIMFUNC3

[ Mizar article, MML identifier index ]

environ

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


begin

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

theorem :: LIMFUNC3:1
(rng seq c= dom f /\ left_open_halfline(x0) or
rng seq c= dom f /\ right_open_halfline(x0)) implies rng seq c= dom f \ {x0};

theorem :: LIMFUNC3:2
(for n holds 0<abs(x0-seq.n) & abs(x0-seq.n)<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 \ {x0};

theorem :: LIMFUNC3:3
seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} implies
for r st 0<r ex n st
  for k st n<=k holds 0<abs(x0-seq.k) & abs(x0-seq.k)<r & seq.k in dom f;

theorem :: LIMFUNC3:4
0<r implies ].x0-r,x0+r.[ \ {x0} = ].x0-r,x0.[ \/ ].x0,x0+r.[;

theorem :: LIMFUNC3:5
0<r2 & ].x0-r2,x0.[ \/ ].x0,x0+r2.[ c= dom f implies
for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f;

theorem :: LIMFUNC3:6
(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 \ {x0};

theorem :: LIMFUNC3:7
seq is convergent & lim seq=x0 & 0<g implies
ex k st for n st k<=n holds x0-g<seq.n & seq.n<x0+g;

theorem :: LIMFUNC3:8
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) iff
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
(for r st x0<r ex g st g<r & x0<g & g in dom f);

definition let f,x0;
pred f is_convergent_in x0 means
:: LIMFUNC3:def 1
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
ex g st for seq st seq is convergent & lim seq=x0 &
  rng seq c= dom f \ {x0} holds f*seq is convergent & lim(f*seq)=g;
pred f is_divergent_to+infty_in x0 means
:: LIMFUNC3:def 2
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
for seq st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds
  f*seq is divergent_to+infty;
pred f is_divergent_to-infty_in x0 means
:: LIMFUNC3:def 3
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
for seq st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds
  f*seq is divergent_to-infty;
end;

canceled 3;

theorem :: LIMFUNC3:12
  f is_convergent_in x0 iff
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
ex g st for g1 st 0<g1 ex g2 st 0<g2 &
  for r1 st 0<abs(x0-r1) & abs(x0-r1)<g2 & r1 in dom f holds abs(f.r1-g)<g1;

theorem :: LIMFUNC3:13
  f is_divergent_to+infty_in x0 iff
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
for g1 ex g2 st 0<g2 &
  for r1 st 0<abs(x0-r1) & abs(x0-r1)<g2 & r1 in dom f holds g1<f.r1;

theorem :: LIMFUNC3:14
  f is_divergent_to-infty_in x0 iff
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
for g1 ex g2 st 0<g2 &
  for r1 st 0<abs(x0-r1) & abs(x0-r1)<g2 & r1 in dom f holds f.r1<g1;

theorem :: LIMFUNC3:15
f is_divergent_to+infty_in x0 iff f is_left_divergent_to+infty_in x0 &
f is_right_divergent_to+infty_in x0;

theorem :: LIMFUNC3:16
f is_divergent_to-infty_in x0 iff f is_left_divergent_to-infty_in x0 &
f is_right_divergent_to-infty_in x0;

theorem :: LIMFUNC3:17
  f1 is_divergent_to+infty_in x0 & f2 is_divergent_to+infty_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f1 /\ dom f2 &
  g2<r2 & x0<g2 & g2 in dom f1 /\ dom f2)
implies f1+f2 is_divergent_to+infty_in x0 & f1(#)f2 is_divergent_to+infty_in x0
;

theorem :: LIMFUNC3:18
  f1 is_divergent_to-infty_in x0 & f2 is_divergent_to-infty_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f1 /\ dom f2 &
  g2<r2 & x0<g2 & g2 in dom f1 /\ dom f2)
implies f1+f2 is_divergent_to-infty_in x0 & f1(#)
f2 is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:19
  f1 is_divergent_to+infty_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom(f1+f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2)) &
(ex r st 0<r & f2 is_bounded_below_on ].x0-r,x0.[ \/ ].x0,x0+r.[) implies
f1+f2 is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:20
  f1 is_divergent_to+infty_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2)) &
(ex r,r1 st 0<r & 0<r1 &
  for g st g in dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds r1<=f2.g) implies
f1(#)f2 is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:21
  (f is_divergent_to+infty_in x0 & r>0 implies r(#)
f is_divergent_to+infty_in x0)&
(f is_divergent_to+infty_in x0 & r<0 implies r(#)
f is_divergent_to-infty_in x0)&
(f is_divergent_to-infty_in x0 & r>0 implies r(#)
f is_divergent_to-infty_in x0)&
(f is_divergent_to-infty_in x0 & r<0 implies r(#)f is_divergent_to+infty_in x0)
;

theorem :: LIMFUNC3:22
  (f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0) implies
abs(f) is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:23
(ex r st 0<r & f is_non_decreasing_on ].x0-r,x0.[ &
  f is_non_increasing_on ].x0,x0+r.[ &
  not f is_bounded_above_on ].x0-r,x0.[ &
  not f is_bounded_above_on ].x0,x0+r.[) &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies
f is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:24
  (ex r st 0<r & f is_increasing_on ].x0-r,x0.[ &
  f is_decreasing_on ].x0,x0+r.[ &
  not f is_bounded_above_on ].x0-r,x0.[ &
  not f is_bounded_above_on ].x0,x0+r.[) &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies
f is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:25
(ex r st 0<r & f is_non_increasing_on ].x0-r,x0.[ &
  f is_non_decreasing_on ].x0,x0+r.[ &
  not f is_bounded_below_on ].x0-r,x0.[ &
  not f is_bounded_below_on ].x0,x0+r.[) &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies
f is_divergent_to-infty_in x0;

theorem :: LIMFUNC3:26
  (ex r st 0<r & f is_decreasing_on ].x0-r,x0.[ &
  f is_increasing_on ].x0,x0+r.[ &
  not f is_bounded_below_on ].x0-r,x0.[ &
  not f is_bounded_below_on ].x0,x0+r.[) &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies
f is_divergent_to-infty_in x0;

theorem :: LIMFUNC3:27
f1 is_divergent_to+infty_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
(ex r st 0<r & dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c=
  dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) &
  for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<=f.g) implies
f is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:28
f1 is_divergent_to-infty_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
(ex r st 0<r & dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c=
  dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) &
  for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f.g<=f1.g) implies
f is_divergent_to-infty_in x0;

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

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

definition let f,x0;
assume  f is_convergent_in x0;
func lim(f,x0)->Real means
:: LIMFUNC3:def 4
for seq st seq is convergent & lim seq=x0 &
 rng seq c= dom f \ {x0} holds f*seq is convergent & lim(f*seq)=it;
end;

canceled;

theorem :: LIMFUNC3:32
  f is_convergent_in x0 implies
(lim(f,x0)=g iff for g1 st 0<g1 ex g2 st 0<g2 &
  for r1 st 0<abs(x0-r1) & abs(x0-r1)<g2 & r1 in dom f holds abs(f.r1-g)<g1);

theorem :: LIMFUNC3:33
f is_convergent_in x0 implies f is_left_convergent_in x0 &
f is_right_convergent_in x0 & lim_left(f,x0)=lim_right(f,x0) &
lim(f,x0)=lim_left(f,x0) & lim(f,x0)=lim_right(f,x0);

theorem :: LIMFUNC3:34
  f is_left_convergent_in x0 & f is_right_convergent_in x0 &
lim_left(f,x0)=lim_right(f,x0) implies
f is_convergent_in x0 & lim(f,x0)=lim_left(f,x0) & lim(f,x0)=lim_right(f,x0);

theorem :: LIMFUNC3:35
f is_convergent_in x0 implies r(#)f is_convergent_in x0 &
lim(r(#)f,x0)=r*(lim(f,x0));

theorem :: LIMFUNC3:36
f is_convergent_in x0 implies -f is_convergent_in x0 & lim(-f,x0)=-(lim(f,x0));

theorem :: LIMFUNC3:37
f1 is_convergent_in x0 & f2 is_convergent_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom(f1+f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2)) implies
f1+f2 is_convergent_in x0 & lim(f1+f2,x0)=lim(f1,x0)+lim(f2,x0);

theorem :: LIMFUNC3:38
  f1 is_convergent_in x0 & f2 is_convergent_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom(f1-f2) & g2<r2 & x0<g2 & g2 in dom(f1-f2)) implies
f1-f2 is_convergent_in x0 & lim(f1-f2,x0)=(lim(f1,x0))-(lim(f2,x0));

theorem :: LIMFUNC3:39
  f is_convergent_in x0 & f"{0}={} & lim(f,x0)<>0 implies
f^ is_convergent_in x0 & lim(f^,x0)=(lim(f,x0))";

theorem :: LIMFUNC3:40
  f is_convergent_in x0 implies abs(f) is_convergent_in x0 &
lim(abs(f),x0)=abs(lim(f,x0));

theorem :: LIMFUNC3:41
f is_convergent_in x0 & lim(f,x0)<>0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 &
  x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0)
implies f^ is_convergent_in x0 & lim(f^,x0)=(lim(f,x0))";

theorem :: LIMFUNC3:42
f1 is_convergent_in x0 & f2 is_convergent_in x0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)
f2)) implies
f1(#)f2 is_convergent_in x0 & lim(f1(#)f2,x0)=(lim(f1,x0))*(lim(f2,x0));

theorem :: LIMFUNC3:43
  f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim(f2,x0)<>0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom(f1/f2) & g2<r2 & x0<g2 & g2 in dom(f1/f2)) implies
f1/f2 is_convergent_in x0 & lim(f1/f2,x0)=(lim(f1,x0))/(lim(f2,x0));

theorem :: LIMFUNC3:44
  f1 is_convergent_in x0 & lim(f1,x0)=0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2)) &
(ex r st 0<r & f2 is_bounded_on ].x0-r,x0.[ \/ ].x0,x0+r.[) implies
f1(#)f2 is_convergent_in x0 & lim(f1(#)f2,x0)=0;

theorem :: LIMFUNC3:45
f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim(f1,x0)=lim(f2,x0) &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) &
(ex r st 0<r &
 (for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds
  f1.g<=f.g & f.g<=f2.g) &
  ((dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c=
     dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) &
    dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c=
     dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)) or
   (dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c=
     dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) &
    dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c=
     dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)))) implies
f is_convergent_in x0 & lim(f,x0)=lim(f1,x0);

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

theorem :: LIMFUNC3:47
  f1 is_convergent_in x0 & f2 is_convergent_in x0 &
(ex r st 0<r &
 ((dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f2 /\ (].x0-r,x0.[ \/
 ].x0,x0+r.[)
   & for g st g in dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<=f2.g) or
  (dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/
 ].x0,x0+r.[)
   & for g st g in dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<=
f2.g))) implies
lim(f1,x0)<=lim(f2,x0);

theorem :: LIMFUNC3:48
  (f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0) &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f &
  g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0)
implies f^ is_convergent_in x0 & lim(f^,x0)=0;

theorem :: LIMFUNC3:49
  f is_convergent_in x0 & lim(f,x0)=0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f & g2<r2 &
  x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0) &
(ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/
 ].x0,x0+r.[) holds 0<=f.g)
implies f^ is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:50
  f is_convergent_in x0 & lim(f,x0)=0 &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
  r1<g1 & g1<x0 & g1 in dom f &
  g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0) &
(ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/
 ].x0,x0+r.[) holds f.g<=0)
implies f^ is_divergent_to-infty_in x0;

theorem :: LIMFUNC3:51
  f is_convergent_in x0 & lim(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds 0<f.g)
implies f^ is_divergent_to+infty_in x0;

theorem :: LIMFUNC3:52
  f is_convergent_in x0 & lim(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f.g<0)
implies f^ is_divergent_to-infty_in x0;