:: The Limit of a Real Function at a Point :: by Jaros{\l}aw Kotowicz :: :: Received September 5, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1, RELAT_1, TARSKI, VALUED_1, XBOOLE_0, LIMFUNC1, FUNCT_1, COMPLEX1, SEQ_2, ORDINAL2, XXREAL_1, FUNCT_2, LIMFUNC2, NAT_1, VALUED_0, XXREAL_2, ORDINAL4, LIMFUNC3; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, VALUED_0, VALUED_1, SEQ_1, PARTFUN1, COMSEQ_2, SEQ_2, RCOMP_1, RFUNCT_1, LIMFUNC1, LIMFUNC2, RECDEF_1; constructors REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, PARTFUN1, RFUNCT_1, RFUNCT_2, LIMFUNC1, LIMFUNC2, VALUED_1, RECDEF_1, RELSET_1, COMSEQ_2, NUMBERS; registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, SEQ_4; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve r,r1,r2,g,g1,g2,x0,t for Real; reserve n,k,m for Element of 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<|.x0-seq.n.| & |.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 00 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:19 (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:20 (ex r st f|].x0-r,x0.[ is non-decreasing & f|].x0,x0+r.[ is non-increasing & not f|].x0-r,x0.[ is bounded_above & not f|].x0,x0+r.[ is bounded_above) & (for r1,r2 st r1 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; theorem :: LIMFUNC3:28 f is_convergent_in x0 implies (lim(f,x0)=g iff for g1 st 00 implies f^ is_convergent_in x0 & lim(f^,x0)=(lim(f,x0))"; theorem :: LIMFUNC3:36 f is_convergent_in x0 implies abs(f) is_convergent_in x0 & lim(abs(f), x0)=|.lim(f,x0).|; theorem :: LIMFUNC3:37 f is_convergent_in x0 & lim(f,x0)<>0 & (for r1,r2 st r10 & f.g2<>0) implies f^ is_convergent_in x0 & lim(f^,x0)=(lim(f,x0))"; theorem :: LIMFUNC3:38 f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1,r2 st r10 & (for r1,r2 st r10 & f.g2<>0) implies f^ is_convergent_in x0 & lim(f^, x0)=0; theorem :: LIMFUNC3:45 f is_convergent_in x0 & lim(f,x0)=0 & (for r1,r2 st r10 & f.g2<>0) & (ex r st 00 & f.g2<>0) & (ex r st 0