let T be non empty TopSpace; :: thesis: for M being non empty MetrSpace

for f being Function of T,(TopSpaceMetr M) holds

( f is continuous iff for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) )

let M be non empty MetrSpace; :: thesis: for f being Function of T,(TopSpaceMetr M) holds

( f is continuous iff for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) )

let f be Function of T,(TopSpaceMetr M); :: thesis: ( f is continuous iff for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) )

thus ( f is continuous implies for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) ) :: thesis: ( ( for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) ) implies f is continuous )

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) ; :: thesis: f is continuous

for p being Point of T

for V being Subset of (TopSpaceMetr M) st f . p in V & V is open holds

ex W being Subset of T st

( p in W & W is open & f .: W c= V )

for f being Function of T,(TopSpaceMetr M) holds

( f is continuous iff for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) )

let M be non empty MetrSpace; :: thesis: for f being Function of T,(TopSpaceMetr M) holds

( f is continuous iff for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) )

let f be Function of T,(TopSpaceMetr M); :: thesis: ( f is continuous iff for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) )

thus ( f is continuous implies for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) ) :: thesis: ( ( for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) ) implies f is continuous )

proof

assume A4:
for p being Point of T
assume A1:
f is continuous
; :: thesis: for p being Point of T

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) )

let p be Point of T; :: thesis: for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) )

let q be Point of M; :: thesis: for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) )

let r be positive Real; :: thesis: ( q = f . p implies ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) )

assume A2: f . p = q ; :: thesis: ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) )

reconsider V = Ball (q,r) as Subset of (TopSpaceMetr M) ;

A3: q in Ball (q,r) by GOBOARD6:1;

V is open by TOPMETR:14;

then ex W being Subset of T st

( p in W & W is open & f .: W c= V ) by A1, A2, A3, JGRAPH_2:10;

hence ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) ; :: thesis: verum

end;for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) )

let p be Point of T; :: thesis: for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) )

let q be Point of M; :: thesis: for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) )

let r be positive Real; :: thesis: ( q = f . p implies ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) )

assume A2: f . p = q ; :: thesis: ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) )

reconsider V = Ball (q,r) as Subset of (TopSpaceMetr M) ;

A3: q in Ball (q,r) by GOBOARD6:1;

V is open by TOPMETR:14;

then ex W being Subset of T st

( p in W & W is open & f .: W c= V ) by A1, A2, A3, JGRAPH_2:10;

hence ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) ; :: thesis: verum

for q being Point of M

for r being positive Real st q = f . p holds

ex W being open Subset of T st

( p in W & f .: W c= Ball (q,r) ) ; :: thesis: f is continuous

for p being Point of T

for V being Subset of (TopSpaceMetr M) st f . p in V & V is open holds

ex W being Subset of T st

( p in W & W is open & f .: W c= V )

proof

hence
f is continuous
by JGRAPH_2:10; :: thesis: verum
let p be Point of T; :: thesis: for V being Subset of (TopSpaceMetr M) st f . p in V & V is open holds

ex W being Subset of T st

( p in W & W is open & f .: W c= V )

let V be Subset of (TopSpaceMetr M); :: thesis: ( f . p in V & V is open implies ex W being Subset of T st

( p in W & W is open & f .: W c= V ) )

assume A5: f . p in V ; :: thesis: ( not V is open or ex W being Subset of T st

( p in W & W is open & f .: W c= V ) )

reconsider u = f . p as Point of M ;

assume V is open ; :: thesis: ex W being Subset of T st

( p in W & W is open & f .: W c= V )

then Int V = V by TOPS_1:23;

then consider e being Real such that

A6: ( e > 0 & Ball (u,e) c= V ) by A5, GOBOARD6:4;

ex W being open Subset of T st

( p in W & f .: W c= Ball (u,e) ) by A4, A6;

hence ex W being Subset of T st

( p in W & W is open & f .: W c= V ) by A6, XBOOLE_1:1; :: thesis: verum

end;ex W being Subset of T st

( p in W & W is open & f .: W c= V )

let V be Subset of (TopSpaceMetr M); :: thesis: ( f . p in V & V is open implies ex W being Subset of T st

( p in W & W is open & f .: W c= V ) )

assume A5: f . p in V ; :: thesis: ( not V is open or ex W being Subset of T st

( p in W & W is open & f .: W c= V ) )

reconsider u = f . p as Point of M ;

assume V is open ; :: thesis: ex W being Subset of T st

( p in W & W is open & f .: W c= V )

then Int V = V by TOPS_1:23;

then consider e being Real such that

A6: ( e > 0 & Ball (u,e) c= V ) by A5, GOBOARD6:4;

ex W being open Subset of T st

( p in W & f .: W c= Ball (u,e) ) by A4, A6;

hence ex W being Subset of T st

( p in W & W is open & f .: W c= V ) by A6, XBOOLE_1:1; :: thesis: verum