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

### The Limit of a Real Function at a Point

by
Jaroslaw Kotowicz

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;
```