let Rseq be Function of [:NAT,NAT:],REAL; ( ( for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ) iff Rseq is convergent_in_cod1 )
hereby ( Rseq is convergent_in_cod1 implies for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} )
assume A1:
for
x being
Element of
NAT holds
lim_filter (
(ProjMap2 ((# Rseq),x)),
(Frechet_Filter NAT))
<> {}
;
Rseq is convergent_in_cod1 now for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent let m be
Element of
NAT ;
ProjMap2 (Rseq,m) is convergent
not
lim_filter (
(ProjMap2 ((# Rseq),m)),
(Frechet_Filter NAT)) is
empty
by A1;
then consider r being
Element of
(TopSpaceMetr RealSpace) such that A2:
r in lim_filter (
(ProjMap2 ((# Rseq),m)),
(Frechet_Filter NAT))
;
A3:
r in lim_f (ProjMap2 ((# Rseq),m))
by A2;
A4:
Balls r is
basis of
(BOOL2F (NeighborhoodSystem r))
by CARDFIL3:6;
reconsider r1 =
r as
Real ;
now for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < elet e be
Real;
( 0 < e implies ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e )assume
0 < e
;
ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < ethen consider m1 being
Nat such that A5:
not
m1 is
zero
and A6:
1
/ m1 < e
by Th5;
consider y being
Point of
RealSpace such that A7:
y = r
and A8:
Balls r = { (Ball (y,(1 / n))) where n is Nat : n <> 0 }
by FRECHET:def 1;
A9:
Ball (
y,
(1 / m1))
c= Ball (
y,
e)
by A6, PCOMPS_1:1;
Ball (
y,
(1 / m1))
in Balls r
by A8, A5;
then consider i being
Nat such that A10:
for
j being
Nat st
i <= j holds
(ProjMap2 ((# Rseq),m)) . j in Ball (
y,
(1 / m1))
by A4, A3, CARDFIL2:97;
thus
ex
N being
Nat st
for
n being
Nat st
N <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e
verumproof
take
i
;
for n being Nat st i <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e
let j be
Nat;
( i <= j implies |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e )
assume
i <= j
;
|.(((ProjMap2 (Rseq,m)) . j) - r1).| < e
then
(ProjMap2 ((# Rseq),m)) . j in Ball (
y,
e)
by A9, A10;
then
(ProjMap2 ((# Rseq),m)) . j in ].(y - e),(y + e).[
by FRECHET:7;
hence
|.(((ProjMap2 (Rseq,m)) . j) - r1).| < e
by A7, FCONT_3:1;
verum
end; end; hence
ProjMap2 (
Rseq,
m) is
convergent
by SEQ_2:def 6;
verum end; hence
Rseq is
convergent_in_cod1
;
verum
end;
assume A13:
Rseq is convergent_in_cod1
; for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}
now for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} let x be
Element of
NAT ;
lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} consider r being
Real such that A14:
for
p being
Real st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.(((ProjMap2 (Rseq,x)) . m) - r).| < p
by A13, SEQ_2:def 6;
reconsider r1 =
r as
Point of
(TopSpaceMetr RealSpace) by XREAL_0:def 1;
A15:
Balls r1 is
basis of
(BOOL2F (NeighborhoodSystem r1))
by CARDFIL3:6;
for
b being
Element of
Balls r1 ex
i being
Nat st
for
j being
Nat st
i <= j holds
(ProjMap2 ((# Rseq),x)) . j in b
proof
let b be
Element of
Balls r1;
ex i being Nat st
for j being Nat st i <= j holds
(ProjMap2 ((# Rseq),x)) . j in b
consider y being
Point of
RealSpace such that A16:
y = r1
and A17:
Balls r1 = { (Ball (y,(1 / n))) where n is Nat : n <> 0 }
by FRECHET:def 1;
b in { (Ball (y,(1 / n))) where n is Nat : n <> 0 }
by A17;
then consider n0 being
Nat such that A18:
b = Ball (
y,
(1 / n0))
and A19:
n0 <> 0
;
(
0 < n0 &
0 * n0 < 1 )
by A19;
then consider n1 being
Nat such that A20:
for
m being
Nat st
n1 <= m holds
|.(((ProjMap2 (Rseq,x)) . m) - r).| < 1
/ n0
by A14, XREAL_1:81;
now ex n1 being Nat st
for j being Nat st n1 <= j holds
(ProjMap2 ((# Rseq),x)) . j in btake n1 =
n1;
for j being Nat st n1 <= j holds
(ProjMap2 ((# Rseq),x)) . j in bhereby verum
let j be
Nat;
( n1 <= j implies (ProjMap2 ((# Rseq),x)) . j in b )assume
n1 <= j
;
(ProjMap2 ((# Rseq),x)) . j in bthen A21:
|.(((ProjMap2 (Rseq,x)) . j) - r).| < 1
/ n0
by A20;
(ProjMap2 (Rseq,x)) . j = r + (((ProjMap2 (Rseq,x)) . j) - r)
;
then
(ProjMap2 (Rseq,x)) . j in ].(r - (1 / n0)),(r + (1 / n0)).[
by A21, FCONT_3:3;
hence
(ProjMap2 ((# Rseq),x)) . j in b
by A16, A18, FRECHET:7;
verum
end; end;
hence
ex
i being
Nat st
for
j being
Nat st
i <= j holds
(ProjMap2 ((# Rseq),x)) . j in b
;
verum
end; then
lim_f (ProjMap2 ((# Rseq),x)) <> {}
by A15, CARDFIL2:97;
hence
lim_filter (
(ProjMap2 ((# Rseq),x)),
(Frechet_Filter NAT))
<> {}
;
verum end;
hence
for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}
; verum