:: One-Side Limits of a Real Function at a Point :: by Jaros{\l}aw Kotowicz :: :: Received August 20, 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, SEQ_2, ORDINAL2, FUNCT_1, LIMFUNC1, FUNCT_2, XXREAL_1, COMPLEX1, XXREAL_2, NAT_1, VALUED_0, ORDINAL4, LIMFUNC2, ASYMPT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, RELSET_1, RCOMP_1, PARTFUN1, RFUNCT_1, LIMFUNC1, XXREAL_0; constructors FUNCOP_1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, PARTFUN1, VALUED_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1; registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, SEQ_4, SEQ_1, SEQ_2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve r,r1,r2,g,g1,g2,x0,t 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 & r0 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:22 (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:23 (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:24 (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:25 (ex r st f|].x0-r,x0.[ is non-decreasing& not f|].x0-r,x0.[ is bounded_above) & (for r st r 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; theorem :: LIMFUNC2:41 f is_left_convergent_in x0 implies (lim_left(f,x0)=g iff for g1 st 0< g1 ex r st r0 implies f^ is_left_convergent_in x0 & lim_left(f^,x0)=(lim_left(f,x0))"; theorem :: LIMFUNC2:48 f is_left_convergent_in x0 implies abs(f) is_left_convergent_in x0 & lim_left(abs(f),x0)=|.lim_left(f,x0).|; theorem :: LIMFUNC2:49 f is_left_convergent_in x0 & lim_left(f,x0)<>0 & (for r st r0) implies f^ is_left_convergent_in x0 & lim_left(f^,x0)=(lim_left(f,x0))"; theorem :: LIMFUNC2:50 f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & (for r st r 0 & (for r st r0 implies f^ is_right_convergent_in x0 & lim_right(f^,x0)=(lim_right(f,x0))"; theorem :: LIMFUNC2:57 f is_right_convergent_in x0 implies abs(f) is_right_convergent_in x0 & lim_right(abs(f),x0)=|.lim_right(f,x0).|; theorem :: LIMFUNC2:58 f is_right_convergent_in x0 & lim_right(f,x0)<>0 & (for r st x0< r ex g st g0) implies f^ is_right_convergent_in x0 & lim_right(f^,x0)=(lim_right(f,x0))"; theorem :: LIMFUNC2:59 f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r st x00 & (for r st x00) implies f^ is_left_convergent_in x0 & lim_left(f^,x0)=0; theorem :: LIMFUNC2:70 (f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) & (for r st x00) implies f^ is_right_convergent_in x0 & lim_right(f^,x0)=0; theorem :: LIMFUNC2:71 f is_left_convergent_in x0 & lim_left(f,x0)=0 & (ex r st 00) & (ex r st 00) & (ex r st 00) & (ex r st 00) & (ex r st 0