:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received August 31, 2013

:: Copyright (c) 2013-2019 Association of Mizar Users

:: Convergence in the Pringsheim sense

:: deftheorem defines P-convergent DBLSEQ_1:def 1 :

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is P-convergent iff ex p being Real st

for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - p).| < e );

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is P-convergent iff ex p being Real st

for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - p).| < e );

definition

let Rseq be Function of [:NAT,NAT:],REAL;

assume A1: Rseq is P-convergent ;

ex b_{1} being Real st

for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - b_{1}).| < e
by A1;

uniqueness

for b_{1}, b_{2} being Real st ( for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - b_{1}).| < e ) & ( for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - b_{2}).| < e ) holds

b_{1} = b_{2}

end;
assume A1: Rseq is P-convergent ;

func P-lim Rseq -> Real means :def6: :: DBLSEQ_1:def 2

for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - it).| < e;

existence for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - it).| < e;

ex b

for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - b

uniqueness

for b

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - b

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - b

b

proof end;

:: deftheorem def6 defines P-lim DBLSEQ_1:def 2 :

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent holds

for b_{2} being Real holds

( b_{2} = P-lim Rseq iff for e being Real st 0 < e holds

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - b_{2}).| < e );

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent holds

for b

( b

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - b

definition

let Rseq be Function of [:NAT,NAT:],REAL;

end;
attr Rseq is convergent_in_cod1 means :: DBLSEQ_1:def 3

for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent ;

for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent ;

attr Rseq is convergent_in_cod2 means :: DBLSEQ_1:def 4

for n being Element of NAT holds ProjMap1 (Rseq,n) is convergent ;

for n being Element of NAT holds ProjMap1 (Rseq,n) is convergent ;

:: deftheorem defines convergent_in_cod1 DBLSEQ_1:def 3 :

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is convergent_in_cod1 iff for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent );

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is convergent_in_cod1 iff for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent );

:: deftheorem defines convergent_in_cod2 DBLSEQ_1:def 4 :

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is convergent_in_cod2 iff for n being Element of NAT holds ProjMap1 (Rseq,n) is convergent );

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is convergent_in_cod2 iff for n being Element of NAT holds ProjMap1 (Rseq,n) is convergent );

definition

let Rseq be Function of [:NAT,NAT:],REAL;

ex b_{1} being Function of NAT,REAL st

for m being Element of NAT holds b_{1} . m = lim (ProjMap2 (Rseq,m))

for b_{1}, b_{2} being Function of NAT,REAL st ( for m being Element of NAT holds b_{1} . m = lim (ProjMap2 (Rseq,m)) ) & ( for m being Element of NAT holds b_{2} . m = lim (ProjMap2 (Rseq,m)) ) holds

b_{1} = b_{2}

end;
func lim_in_cod1 Rseq -> Function of NAT,REAL means :def32: :: DBLSEQ_1:def 5

for m being Element of NAT holds it . m = lim (ProjMap2 (Rseq,m));

existence for m being Element of NAT holds it . m = lim (ProjMap2 (Rseq,m));

ex b

for m being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem def32 defines lim_in_cod1 DBLSEQ_1:def 5 :

for Rseq being Function of [:NAT,NAT:],REAL

for b_{2} being Function of NAT,REAL holds

( b_{2} = lim_in_cod1 Rseq iff for m being Element of NAT holds b_{2} . m = lim (ProjMap2 (Rseq,m)) );

for Rseq being Function of [:NAT,NAT:],REAL

for b

( b

definition

let Rseq be Function of [:NAT,NAT:],REAL;

ex b_{1} being Function of NAT,REAL st

for n being Element of NAT holds b_{1} . n = lim (ProjMap1 (Rseq,n))

for b_{1}, b_{2} being Function of NAT,REAL st ( for n being Element of NAT holds b_{1} . n = lim (ProjMap1 (Rseq,n)) ) & ( for n being Element of NAT holds b_{2} . n = lim (ProjMap1 (Rseq,n)) ) holds

b_{1} = b_{2}

end;
func lim_in_cod2 Rseq -> Function of NAT,REAL means :def33: :: DBLSEQ_1:def 6

for n being Element of NAT holds it . n = lim (ProjMap1 (Rseq,n));

existence for n being Element of NAT holds it . n = lim (ProjMap1 (Rseq,n));

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem def33 defines lim_in_cod2 DBLSEQ_1:def 6 :

for Rseq being Function of [:NAT,NAT:],REAL

for b_{2} being Function of NAT,REAL holds

( b_{2} = lim_in_cod2 Rseq iff for n being Element of NAT holds b_{2} . n = lim (ProjMap1 (Rseq,n)) );

for Rseq being Function of [:NAT,NAT:],REAL

for b

( b

definition

let Rseq be Function of [:NAT,NAT:],REAL;

assume a2: lim_in_cod1 Rseq is convergent ;

ex b_{1} being Real st

for e being Real st 0 < e holds

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - b_{1}).| < e
by a2, SEQ_2:def 6;

uniqueness

for b_{1}, b_{2} being Real st ( for e being Real st 0 < e holds

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - b_{1}).| < e ) & ( for e being Real st 0 < e holds

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - b_{2}).| < e ) holds

b_{1} = b_{2}

end;
assume a2: lim_in_cod1 Rseq is convergent ;

func cod1_major_iterated_lim Rseq -> Real means :def34: :: DBLSEQ_1:def 7

for e being Real st 0 < e holds

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - it).| < e;

existence for e being Real st 0 < e holds

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - it).| < e;

ex b

for e being Real st 0 < e holds

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - b

uniqueness

for b

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - b

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - b

b

proof end;

:: deftheorem def34 defines cod1_major_iterated_lim DBLSEQ_1:def 7 :

for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod1 Rseq is convergent holds

for b_{2} being Real holds

( b_{2} = cod1_major_iterated_lim Rseq iff for e being Real st 0 < e holds

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - b_{2}).| < e );

for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod1 Rseq is convergent holds

for b

( b

ex M being Nat st

for m being Nat st m >= M holds

|.(((lim_in_cod1 Rseq) . m) - b

definition

let Rseq be Function of [:NAT,NAT:],REAL;

assume a2: lim_in_cod2 Rseq is convergent ;

ex b_{1} being Real st

for e being Real st 0 < e holds

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - b_{1}).| < e
by a2, SEQ_2:def 6;

uniqueness

for b_{1}, b_{2} being Real st ( for e being Real st 0 < e holds

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - b_{1}).| < e ) & ( for e being Real st 0 < e holds

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - b_{2}).| < e ) holds

b_{1} = b_{2}

end;
assume a2: lim_in_cod2 Rseq is convergent ;

func cod2_major_iterated_lim Rseq -> Real means :def35: :: DBLSEQ_1:def 8

for e being Real st 0 < e holds

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - it).| < e;

existence for e being Real st 0 < e holds

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - it).| < e;

ex b

for e being Real st 0 < e holds

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - b

uniqueness

for b

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - b

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - b

b

proof end;

:: deftheorem def35 defines cod2_major_iterated_lim DBLSEQ_1:def 8 :

for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod2 Rseq is convergent holds

for b_{2} being Real holds

( b_{2} = cod2_major_iterated_lim Rseq iff for e being Real st 0 < e holds

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - b_{2}).| < e );

for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod2 Rseq is convergent holds

for b

( b

ex N being Nat st

for n being Nat st n >= N holds

|.(((lim_in_cod2 Rseq) . n) - b

definition

let Rseq be Function of [:NAT,NAT:],REAL;

end;
attr Rseq is uniformly_convergent_in_cod1 means :: DBLSEQ_1:def 9

( Rseq is convergent_in_cod1 & ( for e being Real st e > 0 holds

ex M being Nat st

for m being Nat st m >= M holds

for n being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e ) );

( Rseq is convergent_in_cod1 & ( for e being Real st e > 0 holds

ex M being Nat st

for m being Nat st m >= M holds

for n being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e ) );

:: deftheorem defines uniformly_convergent_in_cod1 DBLSEQ_1:def 9 :

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is uniformly_convergent_in_cod1 iff ( Rseq is convergent_in_cod1 & ( for e being Real st e > 0 holds

ex M being Nat st

for m being Nat st m >= M holds

for n being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e ) ) );

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is uniformly_convergent_in_cod1 iff ( Rseq is convergent_in_cod1 & ( for e being Real st e > 0 holds

ex M being Nat st

for m being Nat st m >= M holds

for n being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e ) ) );

definition

let Rseq be Function of [:NAT,NAT:],REAL;

end;
attr Rseq is uniformly_convergent_in_cod2 means :: DBLSEQ_1:def 10

( Rseq is convergent_in_cod2 & ( for e being Real st e > 0 holds

ex N being Nat st

for n being Nat st n >= N holds

for m being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod2 Rseq) . m)).| < e ) );

( Rseq is convergent_in_cod2 & ( for e being Real st e > 0 holds

ex N being Nat st

for n being Nat st n >= N holds

for m being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod2 Rseq) . m)).| < e ) );

:: deftheorem defines uniformly_convergent_in_cod2 DBLSEQ_1:def 10 :

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is uniformly_convergent_in_cod2 iff ( Rseq is convergent_in_cod2 & ( for e being Real st e > 0 holds

ex N being Nat st

for n being Nat st n >= N holds

for m being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod2 Rseq) . m)).| < e ) ) );

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is uniformly_convergent_in_cod2 iff ( Rseq is convergent_in_cod2 & ( for e being Real st e > 0 holds

ex N being Nat st

for n being Nat st n >= N holds

for m being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod2 Rseq) . m)).| < e ) ) );

definition

let Rseq be Function of [:NAT,NAT:],REAL;

end;
attr Rseq is non-decreasing means :: DBLSEQ_1:def 11

for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds

Rseq . (n1,m1) >= Rseq . (n2,m2);

for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds

Rseq . (n1,m1) >= Rseq . (n2,m2);

attr Rseq is non-increasing means :: DBLSEQ_1:def 12

for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds

Rseq . (n1,m1) <= Rseq . (n2,m2);

for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds

Rseq . (n1,m1) <= Rseq . (n2,m2);

:: deftheorem defines non-decreasing DBLSEQ_1:def 11 :

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is non-decreasing iff for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds

Rseq . (n1,m1) >= Rseq . (n2,m2) );

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is non-decreasing iff for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds

Rseq . (n1,m1) >= Rseq . (n2,m2) );

:: deftheorem defines non-increasing DBLSEQ_1:def 12 :

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is non-increasing iff for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds

Rseq . (n1,m1) <= Rseq . (n2,m2) );

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is non-increasing iff for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds

Rseq . (n1,m1) <= Rseq . (n2,m2) );

registration

for b_{1} being Function of [:NAT,NAT:],REAL st b_{1} is non-decreasing & b_{1} is P-convergent holds

( b_{1} is bounded_below & b_{1} is bounded_above )
end;

cluster Function-like V32([:NAT,NAT:], REAL ) P-convergent non-decreasing -> bounded_above bounded_below for Element of bool [:[:NAT,NAT:],REAL:];

coherence for b

( b

proof end;

registration

for b_{1} being Function of [:NAT,NAT:],REAL st b_{1} is non-increasing & b_{1} is P-convergent holds

( b_{1} is bounded_below & b_{1} is bounded_above )
end;

cluster Function-like V32([:NAT,NAT:], REAL ) P-convergent non-increasing -> bounded_above bounded_below for Element of bool [:[:NAT,NAT:],REAL:];

coherence for b

( b

proof end;

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 )

proof end;

registration

let r be Element of REAL ;

for b_{1} being Function of [:NAT,NAT:],REAL st b_{1} = [:NAT,NAT:] --> r holds

( b_{1} is P-convergent & b_{1} is convergent_in_cod1 & b_{1} is convergent_in_cod2 )
by LM111;

end;
cluster [:NAT,NAT:] --> r -> P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [:NAT,NAT:],REAL;

coherence for b

( b

registration

ex b_{1} being Function of [:NAT,NAT:],REAL st

( b_{1} is P-convergent & b_{1} is convergent_in_cod1 & b_{1} is convergent_in_cod2 )
end;

cluster non empty Relation-like [:NAT,NAT:] -defined REAL -valued Function-like V28([:NAT,NAT:]) V32([:NAT,NAT:], REAL ) V109() V110() V111() P-convergent convergent_in_cod1 convergent_in_cod2 for Element of bool [:[:NAT,NAT:],REAL:];

existence ex b

( b

proof end;

registration

let Pseq2 be P-convergent convergent_in_cod2 Function of [:NAT,NAT:],REAL;

coherence

lim_in_cod2 Pseq2 is convergent

end;
coherence

lim_in_cod2 Pseq2 is convergent

proof end;

theorem :: DBLSEQ_1:3

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent & Rseq is convergent_in_cod2 holds

P-lim Rseq = cod2_major_iterated_lim Rseq

P-lim Rseq = cod2_major_iterated_lim Rseq

proof end;

registration

let Pseq1 be P-convergent convergent_in_cod1 Function of [:NAT,NAT:],REAL;

coherence

lim_in_cod1 Pseq1 is convergent

end;
coherence

lim_in_cod1 Pseq1 is convergent

proof end;

theorem :: DBLSEQ_1:4

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent & Rseq is convergent_in_cod1 holds

P-lim Rseq = cod1_major_iterated_lim Rseq

P-lim Rseq = cod1_major_iterated_lim Rseq

proof end;

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 )

proof end;

registration

for b_{1} being Function of [:NAT,NAT:],REAL st b_{1} is non-decreasing & b_{1} is bounded_above holds

( b_{1} is P-convergent & b_{1} is convergent_in_cod1 & b_{1} is convergent_in_cod2 )
by LM112;

end;

cluster Function-like V32([:NAT,NAT:], REAL ) bounded_above non-decreasing -> P-convergent convergent_in_cod1 convergent_in_cod2 for Element of bool [:[:NAT,NAT:],REAL:];

coherence for b

( b

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 )

proof end;

registration

for b_{1} being Function of [:NAT,NAT:],REAL st b_{1} is non-increasing & b_{1} is bounded_below holds

( b_{1} is P-convergent & b_{1} is convergent_in_cod1 & b_{1} is convergent_in_cod2 )
by LM113;

end;

cluster Function-like V32([:NAT,NAT:], REAL ) bounded_below non-increasing -> P-convergent convergent_in_cod1 convergent_in_cod2 for Element of bool [:[:NAT,NAT:],REAL:];

coherence for b

( b

theorem :: DBLSEQ_1:5

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is uniformly_convergent_in_cod1 & lim_in_cod1 Rseq is convergent holds

( Rseq is P-convergent & P-lim Rseq = cod1_major_iterated_lim Rseq )

( Rseq is P-convergent & P-lim Rseq = cod1_major_iterated_lim Rseq )

proof end;

theorem :: DBLSEQ_1:6

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is uniformly_convergent_in_cod2 & lim_in_cod2 Rseq is convergent holds

( Rseq is P-convergent & P-lim Rseq = cod2_major_iterated_lim Rseq )

( Rseq is P-convergent & P-lim Rseq = cod2_major_iterated_lim Rseq )

proof end;

:: deftheorem defines Cauchy DBLSEQ_1:def 13 :

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is Cauchy iff for e being Real st e > 0 holds

ex N being Nat st

for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds

|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e );

for Rseq being Function of [:NAT,NAT:],REAL holds

( Rseq is Cauchy iff for e being Real st e > 0 holds

ex N being Nat st

for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds

|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e );

theorem :: DBLSEQ_1:8

for Rseq being Function of [:NAT,NAT:],REAL st ( Rseq is non-decreasing or Rseq is non-increasing ) holds

( Rseq is P-convergent iff ( Rseq is bounded_below & Rseq is bounded_above ) ) ;

( Rseq is P-convergent iff ( Rseq is bounded_below & Rseq is bounded_above ) ) ;

definition

let X, Y be non empty set ;

let H be BinOp of Y;

let f, g be Function of X,Y;

:: original: *

redefine func H * (f,g) -> Function of [:X,X:],Y;

coherence

H * (f,g) is Function of [:X,X:],Y

end;
let H be BinOp of Y;

let f, g be Function of X,Y;

:: original: *

redefine func H * (f,g) -> Function of [:X,X:],Y;

coherence

H * (f,g) is Function of [:X,X:],Y

proof end;

theorem :: DBLSEQ_1:9

for rseq1, rseq2 being convergent Real_Sequence holds

( multreal * (rseq1,rseq2) is convergent_in_cod1 & multreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (multreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )

( multreal * (rseq1,rseq2) is convergent_in_cod1 & multreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (multreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & lim_in_cod2 (multreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) & multreal * (rseq1,rseq2) is P-convergent & P-lim (multreal * (rseq1,rseq2)) = (lim rseq1) * (lim rseq2) )

proof end;

theorem :: DBLSEQ_1:10

for rseq1, rseq2 being convergent Real_Sequence holds

( addreal * (rseq1,rseq2) is convergent_in_cod1 & addreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )

( addreal * (rseq1,rseq2) is convergent_in_cod1 & addreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )

proof end;

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

proof end;

theorem :: DBLSEQ_1:11

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent holds

( Rseq1 + Rseq2 is P-convergent & P-lim (Rseq1 + Rseq2) = (P-lim Rseq1) + (P-lim Rseq2) )

( Rseq1 + Rseq2 is P-convergent & P-lim (Rseq1 + Rseq2) = (P-lim Rseq1) + (P-lim Rseq2) )

proof end;

theorem th54b: :: DBLSEQ_1:12

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent holds

( Rseq1 - Rseq2 is P-convergent & P-lim (Rseq1 - Rseq2) = (P-lim Rseq1) - (P-lim Rseq2) )

( Rseq1 - Rseq2 is P-convergent & P-lim (Rseq1 - Rseq2) = (P-lim Rseq1) - (P-lim Rseq2) )

proof end;

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 )

proof end;

theorem :: DBLSEQ_1:13

for Rseq being Function of [:NAT,NAT:],REAL

for r being Real st Rseq is P-convergent holds

( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) )

for r being Real st Rseq is P-convergent holds

( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) )

proof end;

theorem th55b: :: DBLSEQ_1:14

for Rseq being Function of [:NAT,NAT:],REAL

for r being Real st Rseq is P-convergent & ( for n, m being Nat holds Rseq . (n,m) >= r ) holds

P-lim Rseq >= r

for r being Real st Rseq is P-convergent & ( for n, m being Nat holds Rseq . (n,m) >= r ) holds

P-lim Rseq >= r

proof end;

theorem :: DBLSEQ_1:15

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds

P-lim Rseq1 <= P-lim Rseq2

P-lim Rseq1 <= P-lim Rseq2

proof end;

theorem :: DBLSEQ_1:16

for Rseq, Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent & P-lim Rseq1 = P-lim Rseq2 & ( for n, m being Nat holds

( Rseq1 . (n,m) <= Rseq . (n,m) & Rseq . (n,m) <= Rseq2 . (n,m) ) ) holds

( Rseq is P-convergent & P-lim Rseq = P-lim Rseq1 )

( Rseq1 . (n,m) <= Rseq . (n,m) & Rseq . (n,m) <= Rseq2 . (n,m) ) ) holds

( Rseq is P-convergent & P-lim Rseq = P-lim Rseq1 )

proof end;

definition

let X be non empty set ;

let seq be Function of [:NAT,NAT:],X;

ex b_{1} being Function of [:NAT,NAT:],X ex N, M being V113() sequence of NAT st

for n, m being Nat holds b_{1} . (n,m) = seq . ((N . n),(M . m))

end;
let seq be Function of [:NAT,NAT:],X;

mode subsequence of seq -> Function of [:NAT,NAT:],X means :def9: :: DBLSEQ_1:def 14

ex N, M being V113() sequence of NAT st

for n, m being Nat holds it . (n,m) = seq . ((N . n),(M . m));

existence ex N, M being V113() sequence of NAT st

for n, m being Nat holds it . (n,m) = seq . ((N . n),(M . m));

ex b

for n, m being Nat holds b

proof end;

:: deftheorem def9 defines subsequence DBLSEQ_1:def 14 :

for X being non empty set

for seq, b_{3} being Function of [:NAT,NAT:],X holds

( b_{3} is subsequence of seq iff ex N, M being V113() sequence of NAT st

for n, m being Nat holds b_{3} . (n,m) = seq . ((N . n),(M . m)) );

for X being non empty set

for seq, b

( b

for n, m being Nat holds b

lem01: for seq being V113() sequence of NAT

for n being Nat holds n <= seq . n

proof end;

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 )

proof end;

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

proof end;

registration

let Pseq be P-convergent Function of [:NAT,NAT:],REAL;

coherence

for b_{1} being subsequence of Pseq holds b_{1} is P-convergent
by LM114;

end;
coherence

for b

theorem :: DBLSEQ_1:17

registration

let Rseq be convergent_in_cod1 Function of [:NAT,NAT:],REAL;

coherence

for b_{1} being subsequence of Rseq holds b_{1} is convergent_in_cod1
by th63d;

end;
coherence

for b

theorem :: DBLSEQ_1:18

for Rseq being Function of [:NAT,NAT:],REAL

for Rseq1 being subsequence of Rseq st Rseq is convergent_in_cod1 & lim_in_cod1 Rseq is convergent holds

( lim_in_cod1 Rseq1 is convergent & cod1_major_iterated_lim Rseq1 = cod1_major_iterated_lim Rseq )

for Rseq1 being subsequence of Rseq st Rseq is convergent_in_cod1 & lim_in_cod1 Rseq is convergent holds

( lim_in_cod1 Rseq1 is convergent & cod1_major_iterated_lim Rseq1 = cod1_major_iterated_lim Rseq )

proof end;

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

proof end;

registration

let Rseq be convergent_in_cod2 Function of [:NAT,NAT:],REAL;

coherence

for b_{1} being subsequence of Rseq holds b_{1} is convergent_in_cod2
by th63c;

end;
coherence

for b

theorem :: DBLSEQ_1:19

for Rseq being Function of [:NAT,NAT:],REAL

for Rseq1 being subsequence of Rseq st Rseq is convergent_in_cod2 & lim_in_cod2 Rseq is convergent holds

( lim_in_cod2 Rseq1 is convergent & cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq )

for Rseq1 being subsequence of Rseq st Rseq is convergent_in_cod2 & lim_in_cod2 Rseq is convergent holds

( lim_in_cod2 Rseq1 is convergent & cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq )

proof end;