:: The Limit of a Real Function at a Point :: by Jaros{\l}aw Kotowicz :: :: Received September 5, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for g, r, r1 being real number st 0 < g & r <= r1 holds ( r - g < r1 & r < r1 + g ) proofend; Lm2: for seq being Real_Sequence for f1, f2 being PartFunc of REAL,REAL for X being set st rng seq c= (dom (f1 (#) f2)) \ X holds ( rng seq c= dom (f1 (#) f2) & dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 & rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X ) proofend; Lm3: for r being Real for n being Element of NAT holds ( r - (1 / (n + 1)) < r & r < r + (1 / (n + 1)) ) proofend; Lm4: for seq being Real_Sequence for f1, f2 being PartFunc of REAL,REAL for X being set st rng seq c= (dom (f1 + f2)) \ X holds ( rng seq c= dom (f1 + f2) & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 & rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X ) proofend; theorem Th1: :: LIMFUNC3:1 for x0 being Real for seq being Real_Sequence for f being PartFunc of REAL,REAL st ( rng seq c= (dom f) /\ (left_open_halfline x0) or rng seq c= (dom f) /\ (right_open_halfline x0) ) holds rng seq c= (dom f) \ {x0} proofend; theorem Th2: :: LIMFUNC3:2 for x0 being Real for seq being Real_Sequence for f being PartFunc of REAL,REAL st ( for n being Element of NAT holds ( 0 < abs (x0 - (seq . n)) & abs (x0 - (seq . n)) < 1 / (n + 1) & seq . n in dom f ) ) holds ( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) \ {x0} ) proofend; theorem Th3: :: LIMFUNC3:3 for x0 being Real for seq being Real_Sequence for f being PartFunc of REAL,REAL st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds for r being Real st 0 < r holds ex n being Element of NAT st for k being Element of NAT st n <= k holds ( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f ) proofend; theorem Th4: :: LIMFUNC3:4 for r, x0 being Real st 0 < r holds ].(x0 - r),(x0 + r).[ \ {x0} = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ proofend; theorem Th5: :: LIMFUNC3:5 for r2, x0 being Real for f being PartFunc of REAL,REAL st 0 < r2 & ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ c= dom f holds for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) proofend; theorem Th6: :: LIMFUNC3:6 for x0 being Real for seq being Real_Sequence for f being PartFunc of REAL,REAL st ( for n being Element of NAT holds ( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) holds ( seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} ) proofend; theorem Th7: :: LIMFUNC3:7 for x0, g being Real for seq being Real_Sequence st seq is convergent & lim seq = x0 & 0 < g holds ex k being Element of NAT st for n being Element of NAT st k <= n holds ( x0 - g < seq . n & seq . n < x0 + g ) proofend; theorem Th8: :: LIMFUNC3:8 for x0 being Real for f being PartFunc of REAL,REAL holds ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) iff ( ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom f ) ) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom f ) ) ) ) proofend; definition let f be PartFunc of REAL,REAL; let x0 be Real; predf is_convergent_in x0 means :Def1: :: LIMFUNC3:def 1 ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds ( f /* seq is convergent & lim (f /* seq) = g ) ); predf is_divergent_to+infty_in x0 means :Def2: :: LIMFUNC3:def 2 ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds f /* seq is divergent_to+infty ) ); predf is_divergent_to-infty_in x0 means :Def3: :: LIMFUNC3:def 3 ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds f /* seq is divergent_to-infty ) ); end; :: deftheorem Def1 defines is_convergent_in LIMFUNC3:def_1_:_ for f being PartFunc of REAL,REAL for x0 being Real holds ( f is_convergent_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds ( f /* seq is convergent & lim (f /* seq) = g ) ) ); :: deftheorem Def2 defines is_divergent_to+infty_in LIMFUNC3:def_2_:_ for f being PartFunc of REAL,REAL for x0 being Real holds ( f is_divergent_to+infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds f /* seq is divergent_to+infty ) ) ); :: deftheorem Def3 defines is_divergent_to-infty_in LIMFUNC3:def_3_:_ for f being PartFunc of REAL,REAL for x0 being Real holds ( f is_divergent_to-infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds f /* seq is divergent_to-infty ) ) ); theorem :: LIMFUNC3:9 for x0 being Real for f being PartFunc of REAL,REAL holds ( f is_convergent_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st for g1 being Real st 0 < g1 holds ex g2 being Real st ( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds abs ((f . r1) - g) < g1 ) ) ) ) proofend; theorem :: LIMFUNC3:10 for x0 being Real for f being PartFunc of REAL,REAL holds ( f is_divergent_to+infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for g1 being Real ex g2 being Real st ( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds g1 < f . r1 ) ) ) ) ) proofend; theorem :: LIMFUNC3:11 for x0 being Real for f being PartFunc of REAL,REAL holds ( f is_divergent_to-infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for g1 being Real ex g2 being Real st ( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds f . r1 < g1 ) ) ) ) ) proofend; theorem Th12: :: LIMFUNC3:12 for x0 being Real for f being PartFunc of REAL,REAL holds ( f is_divergent_to+infty_in x0 iff ( f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0 ) ) proofend; theorem Th13: :: LIMFUNC3:13 for x0 being Real for f being PartFunc of REAL,REAL holds ( f is_divergent_to-infty_in x0 iff ( f is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0 ) ) proofend; theorem :: LIMFUNC3:14 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & f2 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in (dom f1) /\ (dom f2) & g2 < r2 & x0 < g2 & g2 in (dom f1) /\ (dom f2) ) ) holds ( f1 + f2 is_divergent_to+infty_in x0 & f1 (#) f2 is_divergent_to+infty_in x0 ) proofend; theorem :: LIMFUNC3:15 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & f2 is_divergent_to-infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in (dom f1) /\ (dom f2) & g2 < r2 & x0 < g2 & g2 in (dom f1) /\ (dom f2) ) ) holds ( f1 + f2 is_divergent_to-infty_in x0 & f1 (#) f2 is_divergent_to+infty_in x0 ) proofend; theorem :: LIMFUNC3:16 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) ) ) & ex r being Real st ( 0 < r & f2 | (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is bounded_below ) holds f1 + f2 is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC3:17 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) ) & ex r, r1 being Real st ( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds r1 <= f2 . g ) ) holds f1 (#) f2 is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC3:18 for x0, r being Real for f being PartFunc of REAL,REAL holds ( ( 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 ) ) proofend; theorem :: LIMFUNC3:19 for x0 being Real for f being PartFunc of REAL,REAL st ( f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0 ) holds abs f is_divergent_to+infty_in x0 proofend; theorem Th20: :: LIMFUNC3:20 for x0 being Real for f being PartFunc of REAL,REAL st ex r being Real 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 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds f is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC3:21 for x0 being Real for f being PartFunc of REAL,REAL st ex r being Real st ( 0 < r & f | ].(x0 - r),x0.[ is increasing & f | ].x0,(x0 + r).[ is decreasing & not f | ].(x0 - r),x0.[ is bounded_above & not f | ].x0,(x0 + r).[ is bounded_above ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds f is_divergent_to+infty_in x0 by Th20; theorem Th22: :: LIMFUNC3:22 for x0 being Real for f being PartFunc of REAL,REAL st ex r being Real st ( f | ].(x0 - r),x0.[ is non-increasing & f | ].x0,(x0 + r).[ is non-decreasing & not f | ].(x0 - r),x0.[ is bounded_below & not f | ].x0,(x0 + r).[ is bounded_below ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds f is_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC3:23 for x0 being Real for f being PartFunc of REAL,REAL st ex r being Real st ( 0 < r & f | ].(x0 - r),x0.[ is decreasing & f | ].x0,(x0 + r).[ is increasing & not f | ].(x0 - r),x0.[ is bounded_below & not f | ].x0,(x0 + r).[ is bounded_below ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds f is_divergent_to-infty_in x0 by Th22; theorem Th24: :: LIMFUNC3:24 for x0 being Real for f1, f being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st ( 0 < r & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds f1 . g <= f . g ) ) holds f is_divergent_to+infty_in x0 proofend; theorem Th25: :: LIMFUNC3:25 for x0 being Real for f1, f being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st ( 0 < r & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds f . g <= f1 . g ) ) holds f is_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC3:26 for x0 being Real for f1, f being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & ex r being Real st ( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds f1 . g <= f . g ) ) holds f is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC3:27 for x0 being Real for f1, f being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & ex r being Real st ( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds f . g <= f1 . g ) ) holds f is_divergent_to-infty_in x0 proofend; definition let f be PartFunc of REAL,REAL; let x0 be Real; assume A1: f is_convergent_in x0 ; func lim (f,x0) -> Real means :Def4: :: LIMFUNC3:def 4 for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds ( f /* seq is convergent & lim (f /* seq) = it ); existence ex b1 being Real st for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds ( f /* seq is convergent & lim (f /* seq) = b1 ) by A1, Def1; uniqueness for b1, b2 being Real st ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds ( f /* seq is convergent & lim (f /* seq) = b1 ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds ( f /* seq is convergent & lim (f /* seq) = b2 ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines lim LIMFUNC3:def_4_:_ for f being PartFunc of REAL,REAL for x0 being Real st f is_convergent_in x0 holds for b3 being Real holds ( b3 = lim (f,x0) iff for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds ( f /* seq is convergent & lim (f /* seq) = b3 ) ); theorem :: LIMFUNC3:28 for x0, g being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 holds ( lim (f,x0) = g iff for g1 being Real st 0 < g1 holds ex g2 being Real st ( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds abs ((f . r1) - g) < g1 ) ) ) proofend; theorem Th29: :: LIMFUNC3:29 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 holds ( 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) ) proofend; theorem :: LIMFUNC3:30 for x0 being Real for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left (f,x0) = lim_right (f,x0) holds ( f is_convergent_in x0 & lim (f,x0) = lim_left (f,x0) & lim (f,x0) = lim_right (f,x0) ) proofend; theorem Th31: :: LIMFUNC3:31 for x0, r being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 holds ( r (#) f is_convergent_in x0 & lim ((r (#) f),x0) = r * (lim (f,x0)) ) proofend; theorem Th32: :: LIMFUNC3:32 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 holds ( - f is_convergent_in x0 & lim ((- f),x0) = - (lim (f,x0)) ) proofend; theorem Th33: :: LIMFUNC3:33 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) ) ) holds ( f1 + f2 is_convergent_in x0 & lim ((f1 + f2),x0) = (lim (f1,x0)) + (lim (f2,x0)) ) proofend; theorem :: LIMFUNC3:34 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f1 - f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 - f2) ) ) holds ( f1 - f2 is_convergent_in x0 & lim ((f1 - f2),x0) = (lim (f1,x0)) - (lim (f2,x0)) ) proofend; theorem :: LIMFUNC3:35 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 & f " {0} = {} & lim (f,x0) <> 0 holds ( f ^ is_convergent_in x0 & lim ((f ^),x0) = (lim (f,x0)) " ) proofend; theorem :: LIMFUNC3:36 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 holds ( abs f is_convergent_in x0 & lim ((abs f),x0) = abs (lim (f,x0)) ) proofend; theorem Th37: :: LIMFUNC3:37 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 & lim (f,x0) <> 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ) holds ( f ^ is_convergent_in x0 & lim ((f ^),x0) = (lim (f,x0)) " ) proofend; theorem Th38: :: LIMFUNC3:38 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) ) holds ( f1 (#) f2 is_convergent_in x0 & lim ((f1 (#) f2),x0) = (lim (f1,x0)) * (lim (f2,x0)) ) proofend; theorem :: LIMFUNC3:39 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f2,x0) <> 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f1 / f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 / f2) ) ) holds ( f1 / f2 is_convergent_in x0 & lim ((f1 / f2),x0) = (lim (f1,x0)) / (lim (f2,x0)) ) proofend; theorem :: LIMFUNC3:40 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & lim (f1,x0) = 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) ) & ex r being Real st ( 0 < r & f2 | (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is bounded ) holds ( f1 (#) f2 is_convergent_in x0 & lim ((f1 (#) f2),x0) = 0 ) proofend; theorem Th41: :: LIMFUNC3:41 for x0 being Real for f1, f2, f being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f1,x0) = lim (f2,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st ( 0 < r & ( for g being Real 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).[) ) ) ) holds ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) proofend; theorem :: LIMFUNC3:42 for x0 being Real for f1, f2, f being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f1,x0) = lim (f2,x0) & ex r being Real st ( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds ( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) proofend; theorem :: LIMFUNC3:43 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & ex r being Real st ( 0 < r & ( ( (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real 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 being Real st g in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds f1 . g <= f2 . g ) ) ) ) holds lim (f1,x0) <= lim (f2,x0) proofend; theorem :: LIMFUNC3:44 for x0 being Real for f being PartFunc of REAL,REAL st ( f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0 ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ) holds ( f ^ is_convergent_in x0 & lim ((f ^),x0) = 0 ) proofend; theorem :: LIMFUNC3:45 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 & lim (f,x0) = 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real 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 being Real st ( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds 0 <= f . g ) ) holds f ^ is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC3:46 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 & lim (f,x0) = 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real 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 being Real st ( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds f . g <= 0 ) ) holds f ^ is_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC3:47 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 & lim (f,x0) = 0 & ex r being Real st ( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds 0 < f . g ) ) holds f ^ is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC3:48 for x0 being Real for f being PartFunc of REAL,REAL st f is_convergent_in x0 & lim (f,x0) = 0 & ex r being Real st ( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds f . g < 0 ) ) holds f ^ is_divergent_to-infty_in x0 proofend;