:: The Limit of a Composition of Real Functions :: 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 REAL_1, PARTFUN1, NUMBERS, CARD_1, ARYTM_3, ARYTM_1, SEQ_1, RELAT_1, TARSKI, FUNCT_2, SUBSET_1, FUNCT_1, XBOOLE_0, LIMFUNC1, LIMFUNC2, SEQ_2, ORDINAL2, XXREAL_1, XXREAL_0, NAT_1, LIMFUNC3, VALUED_0; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, SEQ_1, SEQ_2, VALUED_0, RCOMP_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, LIMFUNC1, LIMFUNC2, LIMFUNC3; constructors PARTFUN1, REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_2, LIMFUNC1, LIMFUNC2, LIMFUNC3, MEMBERED, RELSET_1, COMSEQ_2; registrations RELSET_1, VALUED_0, ORDINAL1, NUMBERS, XBOOLE_0, SEQ_4, FUNCT_2, XREAL_0, NAT_1; requirements SUBSET, ARITHM, NUMERALS; begin reserve r,r1,r2,g,g1,g2,x0 for Real; reserve f1,f2 for PartFunc of REAL,REAL; theorem :: LIMFUNC4:1 for s be Real_Sequence,X be set st rng s c= dom(f2*f1) /\ X holds rng s c= dom(f2*f1) & rng s c= X & rng s c= dom f1 & rng s c= dom f1 /\ X & rng (f1/*s) c= dom f2; theorem :: LIMFUNC4:2 for s be Real_Sequence,X be set st rng s c= dom(f2*f1) \ X holds rng s c= dom(f2*f1) & rng s c= dom f1 & rng s c= dom f1 \ X & rng(f1/*s) c= dom f2; theorem :: LIMFUNC4:3 f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & (for r ex g st rlim(f1,x0)) implies f2*f1 is_divergent_to+infty_in x0; theorem :: LIMFUNC4:40 f1 is_convergent_in x0 & f2 is_divergent_to-infty_in lim(f1,x0) & (for r1,r2 st r1lim(f1,x0)) implies f2*f1 is_divergent_to-infty_in x0; theorem :: LIMFUNC4:41 f1 is_convergent_in x0 & f2 is_right_divergent_to+infty_in lim(f1,x0) & (for r1,r2 st r1lim(f1,x0)) implies f2*f1 is_divergent_to+infty_in x0; theorem :: LIMFUNC4:42 f1 is_convergent_in x0 & f2 is_right_divergent_to-infty_in lim(f1,x0) & (for r1,r2 st r1lim(f1,x0)) implies f2*f1 is_divergent_to-infty_in x0; theorem :: LIMFUNC4:43 f1 is_right_convergent_in x0 & f2 is_divergent_to+infty_in lim_right( f1,x0 ) & (for r st x0lim_right(f1,x0)) implies f2*f1 is_right_divergent_to+infty_in x0; theorem :: LIMFUNC4:44 f1 is_right_convergent_in x0 & f2 is_divergent_to-infty_in lim_right( f1,x0 ) & (for r st x0lim_right(f1,x0)) implies f2*f1 is_right_divergent_to-infty_in x0; theorem :: LIMFUNC4:45 f1 is convergent_in+infty & f2 is_divergent_to+infty_in lim_in+infty f1 & (for r ex g st rlim_in+infty f1) implies f2*f1 is divergent_in+infty_to+infty; theorem :: LIMFUNC4:46 f1 is convergent_in+infty & f2 is_divergent_to-infty_in lim_in+infty f1 & (for r ex g st rlim_in+infty f1) implies f2*f1 is divergent_in+infty_to-infty; theorem :: LIMFUNC4:47 f1 is convergent_in-infty & f2 is_divergent_to+infty_in lim_in-infty f1 & (for r ex g st glim_in-infty f1) implies f2*f1 is divergent_in-infty_to+infty; theorem :: LIMFUNC4:48 f1 is convergent_in-infty & f2 is_divergent_to-infty_in lim_in-infty f1 & (for r ex g st glim_in-infty f1) implies f2*f1 is divergent_in-infty_to-infty; theorem :: LIMFUNC4:49 f1 is_convergent_in x0 & f2 is_left_divergent_to+infty_in lim(f1,x0) & (for r1,r2 st r1lim_left(f1,x0)) implies f2*f1 is_left_divergent_to+infty_in x0; theorem :: LIMFUNC4:52 f1 is_left_convergent_in x0 & f2 is_divergent_to-infty_in lim_left(f1, x0) & (for r st rlim_left(f1,x0)) implies f2*f1 is_left_divergent_to-infty_in x0; theorem :: LIMFUNC4:53 f1 is divergent_in+infty_to+infty & f2 is convergent_in+infty & (for r ex g st rlim_in+infty f1) implies f2*f1 is convergent_in+infty & lim_in+infty(f2*f1)=lim(f2,lim_in+infty f1); theorem :: LIMFUNC4:72 f1 is convergent_in-infty & f2 is_convergent_in lim_in-infty f1 & (for r ex g st glim_in-infty f1) implies f2*f1 is convergent_in-infty & lim_in-infty(f2*f1)=lim(f2,lim_in-infty f1); theorem :: LIMFUNC4:73 f1 is_convergent_in x0 & f2 is_left_convergent_in lim(f1,x0) & (for r1 ,r2 st r1lim_left(f1,x0)) implies f2*f1 is_left_convergent_in x0 & lim_left(f2*f1,x0)=lim(f2,lim_left(f1,x0)); theorem :: LIMFUNC4:75 f1 is_convergent_in x0 & f2 is_right_convergent_in lim(f1,x0) & (for r1,r2 st r1lim_right(f1,x0)) implies f2*f1 is_right_convergent_in x0 & lim_right(f2*f1,x0)=lim(f2,lim_right(f1,x0)); theorem :: LIMFUNC4:77 f1 is_convergent_in x0 & f2 is_convergent_in lim(f1,x0) & (for r1,r2 st r1lim(f1,x0)) implies f2*f1 is_convergent_in x0 & lim(f2*f1, x0)=lim(f2,lim(f1,x0));