let f be Function of R^1,R^1; ( f is continuous iff for p being Point of R^1
for r being positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ )
hereby ( ( for p being Point of R^1
for r being positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ) implies f is continuous )
assume A1:
f is
continuous
;
for p being Point of R^1
for r being positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[let p be
Point of
R^1;
for r being positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[let r be
positive Real;
ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[reconsider p1 =
p,
q1 =
f . p as
Point of
RealSpace ;
consider s being
positive Real such that A2:
f .: (Ball (p1,s)) c= Ball (
q1,
r)
by A1, Th17;
take s =
s;
f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
(
Ball (
p1,
s)
= ].(p1 - s),(p1 + s).[ &
Ball (
q1,
r)
= ].(q1 - r),(q1 + r).[ )
by FRECHET:7;
hence
f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
by A2;
verum
end;
assume A3:
for p being Point of R^1
for r being positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
; f is continuous
for p, q being Point of RealSpace
for r being positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)
proof
let p,
q be
Point of
RealSpace;
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 A4:
q = f . p
;
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)
consider s being
positive Real such that A5:
f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
by A3;
take
s
;
f .: (Ball (p,s)) c= Ball (q,r)
(
Ball (
p,
s)
= ].(p - s),(p + s).[ &
Ball (
q,
r)
= ].(q - r),(q + r).[ )
by FRECHET:7;
hence
f .: (Ball (p,s)) c= Ball (
q,
r)
by A5, A4;
verum
end;
hence
f is continuous
by Th17; verum