let M1, M2 be non empty MetrSpace; :: thesis: 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); :: thesis: ( 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) )

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) ; :: thesis: 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 ) )

( 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); :: thesis: ( 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 :: thesis: ( ( 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 A7:
for p being Point of M1for 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
; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( q = f . p implies ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) )

assume A2: q = f . p ; :: thesis: 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; :: thesis: f .: (Ball (p,s)) c= Ball (q,r)

thus f .: (Ball (p,s)) c= Ball (q,r) :: thesis: verum

end;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; :: thesis: 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; :: thesis: 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; :: thesis: ( q = f . p implies ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) )

assume A2: q = f . p ; :: thesis: 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; :: thesis: f .: (Ball (p,s)) c= Ball (q,r)

thus f .: (Ball (p,s)) c= Ball (q,r) :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Ball (p,s)) or y in Ball (q,r) )

assume y in f .: (Ball (p,s)) ; :: thesis: 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; :: thesis: verum

end;assume y in f .: (Ball (p,s)) ; :: thesis: 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; :: thesis: verum

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) ; :: thesis: 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

hence
f is continuous
by UNIFORM1:3; :: thesis: verum
let r be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r

let w1 be Element of M2; :: thesis: ( w1 = f . w & dist (u,w) < s implies dist (u1,w1) < r )

assume A9: w1 = f . w ; :: thesis: ( not dist (u,w) < s or dist (u1,w1) < r )

assume dist (u,w) < s ; :: thesis: 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; :: thesis: verum

end;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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds

dist (u1,w1) < r

let w1 be Element of M2; :: thesis: ( w1 = f . w & dist (u,w) < s implies dist (u1,w1) < r )

assume A9: w1 = f . w ; :: thesis: ( not dist (u,w) < s or dist (u1,w1) < r )

assume dist (u,w) < s ; :: thesis: 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; :: thesis: verum