environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, SEQ_2, XREAL_0, COMPLEX1, XCMPLX_0, XXREAL_2, FINSET_1, MEMBERED, MESFUNC9, BHSP_3, SEQ_1, VALUED_1, DBLSEQ_1, FUNCOP_1, BINOP_1, BINOP_2, REAL_1;
notations HIDDEN, ZFMISC_1, SUBSET_1, ORDINAL1, XXREAL_2, RELAT_1, PARTFUN1, RELSET_1, FUNCT_1, FUNCT_2, NUMBERS, BINOP_1, XCMPLX_0, TARSKI, XBOOLE_0, FUNCOP_1, FUNCT_3, FINSEQOP, MEMBERED, COMPLEX1, XXREAL_0, XREAL_0, SEQ_1, NAT_1, MESFUNC9, VALUED_1, SEQ_2, FINSET_1, BINOP_2;
definitions ;
theorems TARSKI, XREAL_0, NAT_1, FUNCT_1, XXREAL_0, ZFMISC_1, XREAL_1, FUNCT_2, RELAT_1, MESFUNC9, ORDINAL1, HEINE, NUMBERS, XCMPLX_1, VALUED_1, ABSVALUE, COMPLEX1, MEMBERED, XXREAL_2, RINFSUP1, SEQM_3, SEQ_2, SEQ_4, FUNCOP_1, FINSEQOP, XBOOLE_1, BINOP_2;
schemes FUNCT_2, FUNCT_3, FRAENKEL, ASYMPT_0;
registrations ORDINAL1, XXREAL_0, XREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0, FINSET_1, SUBSET_1, MEMBERED, VALUED_0, XXREAL_2, RELSET_1, MEASURE6, SEQ_4, FUNCT_1, FUNCT_2, VALUED_1, BINOP_2, NAT_1, SEQ_2, SEQ_1;
constructors HIDDEN, TOPMETR, NAT_D, MESFUNC9, SEQ_2, COMSEQ_2, SEQ_4, REAL_1, FINSEQOP, FUNCT_3, BINOP_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities BINOP_1;
expansions MEASURE6;
LM111:
for r being Element of REAL holds
( [:NAT,NAT:] --> r is P-convergent & [:NAT,NAT:] --> r is convergent_in_cod1 & [:NAT,NAT:] --> r is convergent_in_cod2 )
LM112:
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is bounded_above holds
( Rseq is P-convergent & Rseq is convergent_in_cod1 & Rseq is convergent_in_cod2 )
LM113:
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-increasing & Rseq is bounded_below holds
( Rseq is P-convergent & Rseq is convergent_in_cod1 & Rseq is convergent_in_cod2 )
lmADD:
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds
( dom (Rseq1 + Rseq2) = [:NAT,NAT:] & dom (Rseq1 - Rseq2) = [:NAT,NAT:] & ( for n, m being Nat holds (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m)) ) & ( for n, m being Nat holds (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) ) )
lm55a:
for Rseq being Function of [:NAT,NAT:],REAL
for a being Real st ( for n, m being Nat holds Rseq . (n,m) = a ) holds
( Rseq is P-convergent & P-lim Rseq = a )
lem01:
for seq being V113() sequence of NAT
for n being Nat holds n <= seq . n
LM114:
for Rseq being Function of [:NAT,NAT:],REAL
for Rseq1 being subsequence of Rseq st Rseq is P-convergent holds
( Rseq1 is P-convergent & P-lim Rseq1 = P-lim Rseq )
th63d:
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is convergent_in_cod1 holds
for Rseq1 being subsequence of Rseq holds Rseq1 is convergent_in_cod1
th63c:
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is convergent_in_cod2 holds
for Rseq1 being subsequence of Rseq holds Rseq1 is convergent_in_cod2