let m be Nat; for f being Function of (TOP-REAL m),R^1 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= ].((f . p) - r),((f . p) + r).[ )
let f be Function of (TOP-REAL m),R^1; ( 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= ].((f . p) - r),((f . p) + r).[ )
A1:
TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m)
by EUCLID:def 8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),R^1 ;
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= ].((f . p) - r),((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= ].((f . p) - r),((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= ].((f . p) - r),((f . p) + r).[let r be
positive Real;
ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[reconsider p1 =
p as
Point of
(Euclid m) by EUCLID:67;
reconsider q1 =
f . p as
Point of
RealSpace ;
f1 is
continuous
by A1, A2, YELLOW12:36;
then consider s being
positive Real such that A3:
f .: (Ball (p1,s)) c= Ball (
q1,
r)
by A1, Th17;
take s =
s;
f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[
(
Ball (
p1,
s)
= Ball (
p,
s) &
Ball (
q1,
r)
= ].((f . p) - r),((f . p) + r).[ )
by FRECHET:7, TOPREAL9:13;
hence
f .: (Ball (p,s)) c= ].((f . p) - r),((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= ].((f . p) - r),((f . p) + r).[
; f is continuous
for p being Point of (Euclid m)
for q being Point of RealSpace
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 RealSpace
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
RealSpace;
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= ].((f . p) - r),((f . p) + r).[
by A4;
take
s
;
f1 .: (Ball (p,s)) c= Ball (q,r)
(
Ball (
p1,
s)
= Ball (
p,
s) &
].((f . p) - r),((f . p) + r).[ = Ball (
q,
r) )
by A5, FRECHET:7, 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