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