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

( f is open 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 Ball (q,s) c= f .: (Ball (p,r)) )

let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); :: thesis: ( f is open 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 Ball (q,s) c= f .: (Ball (p,r)) )

thus ( f is open implies 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 Ball (q,s) c= f .: (Ball (p,r)) ) :: 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 Ball (q,s) c= f .: (Ball (p,r)) ) implies f is open )

for q being Point of M2

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

ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) ; :: thesis: f is open

for p being Point of (TopSpaceMetr M1)

for V being open Subset of (TopSpaceMetr M1)

for q being Point of M2 st q = f . p & p in V holds

ex r being positive Real st Ball (q,r) c= f .: V

( f is open 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 Ball (q,s) c= f .: (Ball (p,r)) )

let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); :: thesis: ( f is open 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 Ball (q,s) c= f .: (Ball (p,r)) )

thus ( f is open implies 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 Ball (q,s) c= f .: (Ball (p,r)) ) :: 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 Ball (q,s) c= f .: (Ball (p,r)) ) implies f is open )

proof

assume A4:
for p being Point of M1
assume A1:
f is open
; :: 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 Ball (q,s) c= f .: (Ball (p,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 Ball (q,s) c= f .: (Ball (p,r))

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

ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r))

let r be positive Real; :: thesis: ( q = f . p implies ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) )

assume A2: q = f . p ; :: thesis: ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r))

reconsider V = Ball (p,r) as Subset of (TopSpaceMetr M1) ;

A3: p in V by GOBOARD6:1;

V is open by TOPMETR:14;

hence ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) by A1, A2, A3, Th4; :: 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 Ball (q,s) c= f .: (Ball (p,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 Ball (q,s) c= f .: (Ball (p,r))

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

ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r))

let r be positive Real; :: thesis: ( q = f . p implies ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) )

assume A2: q = f . p ; :: thesis: ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r))

reconsider V = Ball (p,r) as Subset of (TopSpaceMetr M1) ;

A3: p in V by GOBOARD6:1;

V is open by TOPMETR:14;

hence ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) by A1, A2, A3, Th4; :: thesis: verum

for q being Point of M2

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

ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) ; :: thesis: f is open

for p being Point of (TopSpaceMetr M1)

for V being open Subset of (TopSpaceMetr M1)

for q being Point of M2 st q = f . p & p in V holds

ex r being positive Real st Ball (q,r) c= f .: V

proof

hence
f is open
by Th4; :: thesis: verum
let p be Point of (TopSpaceMetr M1); :: thesis: for V being open Subset of (TopSpaceMetr M1)

for q being Point of M2 st q = f . p & p in V holds

ex r being positive Real st Ball (q,r) c= f .: V

let V be open Subset of (TopSpaceMetr M1); :: thesis: for q being Point of M2 st q = f . p & p in V holds

ex r being positive Real st Ball (q,r) c= f .: V

let q be Point of M2; :: thesis: ( q = f . p & p in V implies ex r being positive Real st Ball (q,r) c= f .: V )

assume A5: q = f . p ; :: thesis: ( not p in V or ex r being positive Real st Ball (q,r) c= f .: V )

reconsider p1 = p as Point of M1 ;

assume p in V ; :: thesis: ex r being positive Real st Ball (q,r) c= f .: V

then consider r being Real such that

A6: r > 0 and

A7: Ball (p1,r) c= V by TOPMETR:15;

A8: f .: (Ball (p1,r)) c= f .: V by A7, RELAT_1:123;

ex s being positive Real st Ball (q,s) c= f .: (Ball (p1,r)) by A4, A5, A6;

hence ex r being positive Real st Ball (q,r) c= f .: V by A8, XBOOLE_1:1; :: thesis: verum

end;for q being Point of M2 st q = f . p & p in V holds

ex r being positive Real st Ball (q,r) c= f .: V

let V be open Subset of (TopSpaceMetr M1); :: thesis: for q being Point of M2 st q = f . p & p in V holds

ex r being positive Real st Ball (q,r) c= f .: V

let q be Point of M2; :: thesis: ( q = f . p & p in V implies ex r being positive Real st Ball (q,r) c= f .: V )

assume A5: q = f . p ; :: thesis: ( not p in V or ex r being positive Real st Ball (q,r) c= f .: V )

reconsider p1 = p as Point of M1 ;

assume p in V ; :: thesis: ex r being positive Real st Ball (q,r) c= f .: V

then consider r being Real such that

A6: r > 0 and

A7: Ball (p1,r) c= V by TOPMETR:15;

A8: f .: (Ball (p1,r)) c= f .: V by A7, RELAT_1:123;

ex s being positive Real st Ball (q,s) c= f .: (Ball (p1,r)) by A4, A5, A6;

hence ex r being positive Real st Ball (q,r) c= f .: V by A8, XBOOLE_1:1; :: thesis: verum