:: 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