:: The Limit of a Real Function at Infinity. Halflines. :: Real Sequence Divergent to Infinity :: 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, SUBSET_1, SEQ_1, PARTFUN1, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1, RELAT_1, TARSKI, XBOOLE_0, VALUED_1, PROB_1, XXREAL_1, VALUED_0, XXREAL_2, FUNCT_1, SEQ_2, ORDINAL2, COMPLEX1, REAL_1, NAT_1, SQUARE_1, SEQM_3, FUNCT_2, ORDINAL4, LIMFUNC1, ASYMPT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_1, COMPLEX1, REAL_1, SQUARE_1, NAT_1, RELSET_1, PARTFUN1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQM_3, PROB_1, FUNCT_3, RFUNCT_1, RECDEF_1; constructors PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1; registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, XXREAL_1, VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, SQUARE_1, NAT_1, SEQ_1, FUNCT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve r,r1,g for Real, n,m,k for Nat, seq,seq1, seq2 for Real_Sequence, f,f1,f2 for PartFunc of REAL,REAL, x for set; notation let r be Real; synonym left_open_halfline r for halfline r; end; definition let r be Real; func left_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 1 ].-infty,r.]; func right_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 2 [.r,+infty.[; func right_open_halfline r -> Subset of REAL equals :: LIMFUNC1:def 3 ].r,+infty.[; end; theorem :: LIMFUNC1:1 (seq is non-decreasing implies seq is bounded_below) & (seq is non-increasing implies seq is bounded_above); theorem :: LIMFUNC1:2 seq is non-zero & seq is convergent & lim seq=0 & seq is non-decreasing implies for n holds seq.n<0; theorem :: LIMFUNC1:3 seq is non-zero & seq is convergent & lim seq=0 & seq is non-increasing implies for n holds 00 implies r(#)seq is divergent_to+infty) & (seq is divergent_to+infty & r<0 implies r(#)seq is divergent_to-infty) & ( r=0 implies rng (r(#)seq)={0} & r(#) seq is constant) ; theorem :: LIMFUNC1:14 (seq is divergent_to-infty & r>0 implies r(#)seq is divergent_to-infty) & (seq is divergent_to-infty & r<0 implies r(#)seq is divergent_to+infty) & ( r=0 implies rng (r(#)seq)={0} & r(#) seq is constant) ; theorem :: LIMFUNC1:15 (seq is divergent_to+infty implies -seq is divergent_to-infty) & (seq is divergent_to-infty implies -seq is divergent_to+infty); theorem :: LIMFUNC1:16 seq is bounded_below & seq1 is divergent_to-infty implies seq-seq1 is divergent_to+infty; theorem :: LIMFUNC1:17 seq is bounded_above & seq1 is divergent_to+infty implies seq-seq1 is divergent_to-infty; theorem :: LIMFUNC1:18 seq is divergent_to+infty & seq1 is convergent implies seq+seq1 is divergent_to+infty; theorem :: LIMFUNC1:19 seq is divergent_to-infty & seq1 is convergent implies seq+seq1 is divergent_to-infty; theorem :: LIMFUNC1:20 (for n holds seq.n=n) implies seq is divergent_to+infty; theorem :: LIMFUNC1:21 (for n holds seq.n=-n) implies seq is divergent_to-infty; theorem :: LIMFUNC1:22 seq1 is divergent_to+infty & (ex r st r>0 & for n holds seq2.n>= r) implies seq1(#)seq2 is divergent_to+infty; theorem :: LIMFUNC1:23 seq1 is divergent_to-infty & (ex r st 0=r) implies seq1(#)seq2 is divergent_to-infty; theorem :: LIMFUNC1:24 seq1 is divergent_to-infty & seq2 is divergent_to-infty implies seq1(#)seq2 is divergent_to+infty; theorem :: LIMFUNC1:25 (seq is divergent_to+infty or seq is divergent_to-infty) implies abs(seq) is divergent_to+infty; theorem :: LIMFUNC1:26 seq is divergent_to+infty & seq1 is subsequence of seq implies seq1 is divergent_to+infty; theorem :: LIMFUNC1:27 seq is divergent_to-infty & seq1 is subsequence of seq implies seq1 is divergent_to-infty; theorem :: LIMFUNC1:28 seq1 is divergent_to+infty & seq2 is convergent & 00 implies r(#)f is divergent_in+infty_to+infty) & (f is divergent_in+infty_to+infty & r<0 implies r(#)f is divergent_in+infty_to-infty) & (f is divergent_in+infty_to-infty & r>0 implies r(#)f is divergent_in+infty_to-infty) & (f is divergent_in+infty_to-infty & r<0 implies r(#)f is divergent_in+infty_to+infty) ; theorem :: LIMFUNC1:59 (f is divergent_in-infty_to+infty & r>0 implies r(#)f is divergent_in-infty_to+infty) & (f is divergent_in-infty_to+infty & r<0 implies r(#)f is divergent_in-infty_to-infty) & (f is divergent_in-infty_to-infty & r>0 implies r(#)f is divergent_in-infty_to-infty) & (f is divergent_in-infty_to-infty & r<0 implies r(#)f is divergent_in-infty_to+infty) ; theorem :: LIMFUNC1:60 (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty) implies abs(f) is divergent_in+infty_to+infty; theorem :: LIMFUNC1:61 (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty) implies abs(f) is divergent_in-infty_to+infty; theorem :: LIMFUNC1:62 (ex r st f|right_open_halfline r is non-decreasing & not f| right_open_halfline r is bounded_above) & (for r ex g st r Real means :: LIMFUNC1:def 12 for seq st seq is divergent_to+infty & rng seq c= dom f holds f/*seq is convergent & lim(f/*seq)= it; end; definition let f; assume f is convergent_in-infty; func lim_in-infty f -> Real means :: LIMFUNC1:def 13 for seq st seq is divergent_to-infty & rng seq c= dom f holds f/*seq is convergent & lim(f/*seq)= it; end; theorem :: LIMFUNC1:78 f is convergent_in-infty implies (lim_in-infty f=g iff for g1 st 00 implies f^ is convergent_in+infty & lim_in+infty(f^)=(lim_in+infty f)"; theorem :: LIMFUNC1:85 f is convergent_in+infty implies abs(f) is convergent_in+infty & lim_in+infty abs(f)=|.lim_in+infty f.|; theorem :: LIMFUNC1:86 f is convergent_in+infty & lim_in+infty f<>0 & (for r ex g st r 0) implies f^ is convergent_in+infty & lim_in+infty(f^)= (lim_in+infty f)"; theorem :: LIMFUNC1:87 f1 is convergent_in+infty & f2 is convergent_in+infty & (for r ex g st r 0 & (for r ex g st r0 implies f^ is convergent_in-infty & lim_in-infty(f^)=(lim_in-infty f)"; theorem :: LIMFUNC1:94 f is convergent_in-infty implies abs(f) is convergent_in-infty & lim_in-infty abs(f)=|.lim_in-infty f.|; theorem :: LIMFUNC1:95 f is convergent_in-infty & lim_in-infty f<>0 & (for r ex g st g 0) implies f^ is convergent_in-infty & lim_in-infty(f^)= (lim_in-infty f)"; theorem :: LIMFUNC1:96 f1 is convergent_in-infty & f2 is convergent_in-infty & (for r ex g st g 0 & (for r ex g st g0) implies f^ is convergent_in+infty & lim_in+infty(f^)=0; theorem :: LIMFUNC1:107 (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty) & (for r ex g st g0) implies f^ is convergent_in-infty & lim_in-infty(f^)=0; theorem :: LIMFUNC1:108 f is convergent_in+infty & lim_in+infty f=0 & (for r ex g st r0) & (ex r st for g st g in dom f /\ right_open_halfline(r) holds 0<=f.g) implies f^ is divergent_in+infty_to+infty; theorem :: LIMFUNC1:109 f is convergent_in+infty & lim_in+infty f=0 & (for r ex g st r0) & (ex r st for g st g in dom f /\ right_open_halfline(r) holds f.g<=0) implies f^ is divergent_in+infty_to-infty; theorem :: LIMFUNC1:110 f is convergent_in-infty & lim_in-infty f=0 & (for r ex g st g0) & (ex r st for g st g in dom f /\ left_open_halfline(r) holds 0<=f.g) implies f^ is divergent_in-infty_to+infty; theorem :: LIMFUNC1:111 f is convergent_in-infty & lim_in-infty f=0 & (for r ex g st g0) & (ex r st for g st g in dom f /\ left_open_halfline(r) holds f.g<=0) implies f^ is divergent_in-infty_to-infty; theorem :: LIMFUNC1:112 f is convergent_in+infty & lim_in+infty f=0 & (ex r st for g st g in dom f /\ right_open_halfline(r) holds 0