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

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

( f is open iff for p being Point of M

for r being positive Real ex W being open Subset of T st

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

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

( f is open iff for p being Point of M

for r being positive Real ex W being open Subset of T st

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

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

for r being positive Real ex W being open Subset of T st

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

for r being positive Real ex W being open Subset of T st

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

for p being Point of (TopSpaceMetr M)

for V being open Subset of (TopSpaceMetr M) st p in V holds

ex W being open Subset of T st

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

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

( f is open iff for p being Point of M

for r being positive Real ex W being open Subset of T st

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

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

( f is open iff for p being Point of M

for r being positive Real ex W being open Subset of T st

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

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

for r being positive Real ex W being open Subset of T st

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

hereby :: thesis: ( ( for p being Point of M

for r being positive Real ex W being open Subset of T st

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

assume A4:
for p being Point of Mfor r being positive Real ex W being open Subset of T st

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

assume A1:
f is open
; :: thesis: for p being Point of M

for r being positive Real ex W being open Subset of T st

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

let p be Point of M; :: thesis: for r being positive Real ex W being open Subset of T st

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

let r be positive Real; :: thesis: ex W being open Subset of T st

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

A2: p in Ball (p,r) by GOBOARD6:1;

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

V is open by TOPMETR:14;

then consider W being open Subset of T such that

A3: ( f . p in W & W c= f .: V ) by A1, A2, Th3;

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

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

end;for r being positive Real ex W being open Subset of T st

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

let p be Point of M; :: thesis: for r being positive Real ex W being open Subset of T st

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

let r be positive Real; :: thesis: ex W being open Subset of T st

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

A2: p in Ball (p,r) by GOBOARD6:1;

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

V is open by TOPMETR:14;

then consider W being open Subset of T such that

A3: ( f . p in W & W c= f .: V ) by A1, A2, Th3;

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

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

for r being positive Real ex W being open Subset of T st

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

for p being Point of (TopSpaceMetr M)

for V being open Subset of (TopSpaceMetr M) st p in V holds

ex W being open Subset of T st

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

proof

hence
f is open
by Th3; :: thesis: verum
let p be Point of (TopSpaceMetr M); :: thesis: for V being open Subset of (TopSpaceMetr M) st p in V holds

ex W being open Subset of T st

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

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

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

reconsider q = p as Point of M ;

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

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

then consider r being Real such that

A5: r > 0 and

A6: Ball (q,r) c= V by TOPMETR:15;

consider W being open Subset of T such that

A7: f . p in W and

A8: W c= f .: (Ball (q,r)) by A4, A5;

take W ; :: thesis: ( f . p in W & W c= f .: V )

thus f . p in W by A7; :: thesis: W c= f .: V

f .: (Ball (q,r)) c= f .: V by A6, RELAT_1:123;

hence W c= f .: V by A8; :: thesis: verum

end;ex W being open Subset of T st

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

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

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

reconsider q = p as Point of M ;

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

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

then consider r being Real such that

A5: r > 0 and

A6: Ball (q,r) c= V by TOPMETR:15;

consider W being open Subset of T such that

A7: f . p in W and

A8: W c= f .: (Ball (q,r)) by A4, A5;

take W ; :: thesis: ( f . p in W & W c= f .: V )

thus f . p in W by A7; :: thesis: W c= f .: V

f .: (Ball (q,r)) c= f .: V by A6, RELAT_1:123;

hence W c= f .: V by A8; :: thesis: verum