let n, m be Nat; for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is continuous iff for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) )
let f be Function of (TOP-REAL m),(TOP-REAL n); ( f is continuous iff for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) )
A1:
( TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) & TopStruct(# the U1 of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) )
by EUCLID:def 8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),(TopSpaceMetr (Euclid n)) ;
hereby ( ( for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r) ) implies f is continuous )
assume A2:
f is
continuous
;
for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r)let p be
Point of
(TOP-REAL m);
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r)let r be
positive Real;
ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r)reconsider p1 =
p as
Point of
(Euclid m) by EUCLID:67;
reconsider q1 =
f . p as
Point of
(Euclid n) by EUCLID:67;
f1 is
continuous
by A1, A2, YELLOW12:36;
then consider s being
positive Real such that A3:
f1 .: (Ball (p1,s)) c= Ball (
q1,
r)
by Th17;
take s =
s;
f .: (Ball (p,s)) c= Ball ((f . p),r)
(
Ball (
p1,
s)
= Ball (
p,
s) &
Ball (
q1,
r)
= Ball (
(f . p),
r) )
by TOPREAL9:13;
hence
f .: (Ball (p,s)) c= Ball (
(f . p),
r)
by A3;
verum
end;
assume A4:
for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= Ball ((f . p),r)
; f is continuous
for p being Point of (Euclid m)
for q being Point of (Euclid n)
for r being positive Real st q = f1 . p holds
ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)
proof
let p be
Point of
(Euclid m);
for q being Point of (Euclid n)
for r being positive Real st q = f1 . p holds
ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)let q be
Point of
(Euclid n);
for r being positive Real st q = f1 . p holds
ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)let r be
positive Real;
( q = f1 . p implies ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r) )
assume A5:
q = f1 . p
;
ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)
reconsider p1 =
p as
Point of
(TOP-REAL m) by EUCLID:67;
consider s being
positive Real such that A6:
f .: (Ball (p1,s)) c= Ball (
(f . p1),
r)
by A4;
take
s
;
f1 .: (Ball (p,s)) c= Ball (q,r)
(
Ball (
p1,
s)
= Ball (
p,
s) &
Ball (
(f . p1),
r)
= Ball (
q,
r) )
by A5, TOPREAL9:13;
hence
f1 .: (Ball (p,s)) c= Ball (
q,
r)
by A6;
verum
end;
then
f1 is continuous
by Th17;
hence
f is continuous
by A1, YELLOW12:36; verum