let M1, M2 be non empty MetrSpace; for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is continuous iff for p being Point of M1
for q being Point of M2
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) )
let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); ( f is continuous iff for p being Point of M1
for q being Point of M2
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) )
hereby ( ( for p being Point of M1
for q being Point of M2
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) ) implies f is continuous )
assume A1:
f is
continuous
;
for p being Point of M1
for q being Point of M2
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)let p be
Point of
M1;
for q being Point of M2
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)let q be
Point of
M2;
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)let r be
positive Real;
( q = f . p implies ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) )assume A2:
q = f . p
;
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)consider s being
Real such that A3:
s > 0
and A4:
for
w being
Element of
M1 for
w1 being
Element of
M2 st
w1 = f . w &
dist (
p,
w)
< s holds
dist (
q,
w1)
< r
by A1, A2, UNIFORM1:4;
reconsider s =
s as
positive Real by A3;
take s =
s;
f .: (Ball (p,s)) c= Ball (q,r)thus
f .: (Ball (p,s)) c= Ball (
q,
r)
verumproof
let y be
object ;
TARSKI:def 3 ( not y in f .: (Ball (p,s)) or y in Ball (q,r) )
assume
y in f .: (Ball (p,s))
;
y in Ball (q,r)
then consider x being
Point of
(TopSpaceMetr M1) such that A5:
x in Ball (
p,
s)
and A6:
f . x = y
by FUNCT_2:65;
reconsider x1 =
x as
Point of
M1 ;
reconsider y1 =
y as
Point of
M2 by A6;
dist (
p,
x1)
< s
by A5, METRIC_1:11;
then
dist (
q,
y1)
< r
by A6, A4;
hence
y in Ball (
q,
r)
by METRIC_1:11;
verum
end;
end;
assume A7:
for p being Point of M1
for q being Point of M2
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)
; f is continuous
for r being Real
for u being Element of M1
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
proof
let r be
Real;
for u being Element of M1
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let u be
Element of
M1;
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let u1 be
Element of
M2;
( r > 0 & u1 = f . u implies ex s being Real st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
assume
(
r > 0 &
u1 = f . u )
;
ex s being Real st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
then consider s being
positive Real such that A8:
f .: (Ball (u,s)) c= Ball (
u1,
r)
by A7;
take
s
;
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
thus
s > 0
;
for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r
let w be
Element of
M1;
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < rlet w1 be
Element of
M2;
( w1 = f . w & dist (u,w) < s implies dist (u1,w1) < r )
assume A9:
w1 = f . w
;
( not dist (u,w) < s or dist (u1,w1) < r )
assume
dist (
u,
w)
< s
;
dist (u1,w1) < r
then
w in Ball (
u,
s)
by METRIC_1:11;
then
f . w in f .: (Ball (u,s))
by FUNCT_2:35;
hence
dist (
u1,
w1)
< r
by A8, A9, METRIC_1:11;
verum
end;
hence
f is continuous
by UNIFORM1:3; verum