let f be Function of [:NAT,NAT:],ExtREAL; for c being ExtReal st ( for n, m being Nat holds f . (n,m) = c ) holds
( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )
let c be ExtReal; ( ( for n, m being Nat holds f . (n,m) = c ) implies ( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) ) )
reconsider cc = c as R_eal by XXREAL_0:def 1;
A1:
dom f = [:NAT,NAT:]
by FUNCT_2:def 1;
c in ExtREAL
by XXREAL_0:def 1;
then A2:
( c in REAL or c in {-infty,+infty} )
by XBOOLE_0:def 3, XXREAL_0:def 4;
assume A3:
for n, m being Nat holds f . (n,m) = c
; ( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )
then A4:
f . (1,1) = c
;
then A5:
c is UpperBound of rng f
by XXREAL_2:def 1;
per cases
( c in REAL or c = -infty or c = +infty )
by A2, TARSKI:def 2;
suppose
c in REAL
;
( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )then reconsider rc =
c as
Real ;
A6:
now for p being Real st 0 < p holds
ex N being Nat st
for n1, m1 being Nat st N <= n1 & N <= m1 holds
|.((f . (n1,m1)) - rc).| < preconsider N =
0 as
Nat ;
let p be
Real;
( 0 < p implies ex N being Nat st
for n1, m1 being Nat st N <= n1 & N <= m1 holds
|.((f . (n1,m1)) - rc).| < p )assume A7:
0 < p
;
ex N being Nat st
for n1, m1 being Nat st N <= n1 & N <= m1 holds
|.((f . (n1,m1)) - rc).| < ptake N =
N;
for n1, m1 being Nat st N <= n1 & N <= m1 holds
|.((f . (n1,m1)) - rc).| < plet n1,
m1 be
Nat;
( N <= n1 & N <= m1 implies |.((f . (n1,m1)) - rc).| < p )assume
(
N <= n1 &
N <= m1 )
;
|.((f . (n1,m1)) - rc).| < p
(f . (n1,m1)) - rc = (f . (n1,m1)) - (f . (n1,m1))
by A3;
hence
|.((f . (n1,m1)) - rc).| < p
by A7, EXTREAL1:16, XXREAL_3:7;
verum end; then A8:
f is
P-convergent_to_finite_number
;
hence
f is
P-convergent
;
( P-lim f = c & P-lim f = sup (rng f) )hence A9:
P-lim f = c
by A6, A8, Def5;
P-lim f = sup (rng f)
[1,1] in dom f
by A1, ZFMISC_1:87;
hence
P-lim f = sup (rng f)
by A9, A5, A4, FUNCT_1:3, XXREAL_2:55;
verum end; suppose A10:
c = -infty
;
( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )
for
p being
Real st
p < 0 holds
ex
N being
Nat st
for
n,
m being
Nat st
n >= N &
m >= N holds
f . (
n,
m)
<= p
proof
let p be
Real;
( p < 0 implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
f . (n,m) <= p )
assume
p < 0
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
f . (n,m) <= p
take
0
;
for n, m being Nat st n >= 0 & m >= 0 holds
f . (n,m) <= p
hence
for
n,
m being
Nat st
n >= 0 &
m >= 0 holds
f . (
n,
m)
<= p
;
verum
end; then A12:
f is
P-convergent_to_-infty
;
hence
f is
P-convergent
;
( P-lim f = c & P-lim f = sup (rng f) )hence A13:
P-lim f = c
by A10, A12, Def5;
P-lim f = sup (rng f)
[1,1] in dom f
by A1, ZFMISC_1:87;
hence
P-lim f = sup (rng f)
by A5, A4, A13, FUNCT_1:3, XXREAL_2:55;
verum end; suppose A14:
c = +infty
;
( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )
for
p being
Real st
0 < p holds
ex
N being
Nat st
for
n,
m being
Nat st
n >= N &
m >= N holds
p <= f . (
n,
m)
proof
let p be
Real;
( 0 < p implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m) )
assume
0 < p
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m)
take
0
;
for n, m being Nat st n >= 0 & m >= 0 holds
p <= f . (n,m)
hence
for
n,
m being
Nat st
n >= 0 &
m >= 0 holds
p <= f . (
n,
m)
;
verum
end; then A16:
f is
P-convergent_to_+infty
;
hence
f is
P-convergent
;
( P-lim f = c & P-lim f = sup (rng f) )hence A17:
P-lim f = c
by A14, A16, Def5;
P-lim f = sup (rng f)
[1,1] in dom f
by A1, ZFMISC_1:87;
hence
P-lim f = sup (rng f)
by A5, A4, A17, FUNCT_1:3, XXREAL_2:55;
verum end; end;