:: deftheorem Def5 defines P-lim DBLSEQ_3:def 18 :
for f being Function of [:NAT,NAT:],ExtREAL st f is P-convergent holds
for b₂ being ExtReal holds
( b₂ = P-lim f iff ( ex p being Real st
( b₂ = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b₂).| < e ) & f is P-convergent_to_finite_number ) or ( b₂ = +infty & f is P-convergent_to_+infty ) or ( b₂ = -infty & f is P-convergent_to_-infty ) ) );