let X, Y be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y)
for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S & f is continuous holds
T is convergent
let f be Function of (TopSpaceMetr X),(TopSpaceMetr Y); :: thesis: for S being sequence of X
for T being sequence of Y st S is convergent & T = f * S & f is continuous holds
T is convergent
let S be sequence of X; :: thesis: for T being sequence of Y st S is convergent & T = f * S & f is continuous holds
T is convergent
let T be sequence of Y; :: thesis: ( S is convergent & T = f * S & f is continuous implies T is convergent )
assume that
A1: S is convergent and
A2: T = f * S and
A3: f is continuous ; :: thesis: T is convergent
set z0 = lim S;
reconsider p = lim S as Point of (TopSpaceMetr X) by TOPMETR:12;
A4: dom f = the carrier of (TopSpaceMetr X) by FUNCT_2:def 1
.= the carrier of X by TOPMETR:12 ;
then f . (lim S) in rng f by FUNCT_1:def 3;
then reconsider x0 = f . (lim S) as Element of Y by TOPMETR:12;
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((T . m),x0) < r
proof
let r be Real; :: thesis: ( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
dist ((T . m),x0) < r )
reconsider V = Ball (x0,r) as Subset of (TopSpaceMetr Y) by TOPMETR:12;
assume r > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist ((T . m),x0) < r
then ( V is open & x0 in V ) by GOBOARD6:1, TOPMETR:14;
then consider W being Subset of (TopSpaceMetr X) such that
A5: ( p in W & W is open ) and
A6: f .: W c= V by A3, JGRAPH_2:10;
consider r0 being Real such that
A7: r0 > 0 and
A8: Ball ((lim S),r0) c= W by A5, TOPMETR:15;
reconsider r00 = r0 as Real ;
consider n0 being Nat such that
A9: for m being Nat st n0 <= m holds
dist ((S . m),(lim S)) < r00 by A1, A7, TBSP_1:def 3;
for m being Nat st n0 <= m holds
dist ((T . m),x0) < r
proof
let m be Nat; :: thesis: ( n0 <= m implies dist ((T . m),x0) < r )
assume n0 <= m ; :: thesis: dist ((T . m),x0) < r
then dist ((S . m),(lim S)) < r0 by A9;
then S . m in Ball ((lim S),r0) by METRIC_1:11;
then A10: f . (S . m) in f .: W by A4, A8, FUNCT_1:def 6;
A11: m in NAT by ORDINAL1:def 12;
dom T = NAT by FUNCT_2:def 1;
then T . m in f .: W by A2, A10, FUNCT_1:12, A11;
hence dist ((T . m),x0) < r by A6, METRIC_1:11; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
dist ((T . m),x0) < r ; :: thesis: verum
end;
hence T is convergent by TBSP_1:def 2; :: thesis: verum