let m be Nat; :: thesis: for T being non empty TopSpace

for f being Function of T,(TOP-REAL m) holds

( f is open iff for p being Point of T

for V being open Subset of T st p in V holds

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

let T be non empty TopSpace; :: thesis: for f being Function of T,(TOP-REAL m) holds

( f is open iff for p being Point of T

for V being open Subset of T st p in V holds

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

let f be Function of T,(TOP-REAL m); :: thesis: ( f is open iff for p being Point of T

for V being open Subset of T st p in V holds

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

A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def 8;

then reconsider f1 = f as Function of T,(TopSpaceMetr (Euclid m)) ;

A2: TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #) ;

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

for V being open Subset of T st p in V holds

ex r being positive Real st Ball ((f . p),r) c= f .: V ) :: thesis: ( ( for p being Point of T

for V being open Subset of T st p in V holds

ex r being positive Real st Ball ((f . p),r) c= f .: V ) implies f is open )

for V being open Subset of T st p in V holds

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

for p being Point of T

for V being open Subset of T

for q being Point of (Euclid m) st q = f1 . p & p in V holds

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

hence f is open by A1, A2, Th1; :: thesis: verum

for f being Function of T,(TOP-REAL m) holds

( f is open iff for p being Point of T

for V being open Subset of T st p in V holds

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

let T be non empty TopSpace; :: thesis: for f being Function of T,(TOP-REAL m) holds

( f is open iff for p being Point of T

for V being open Subset of T st p in V holds

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

let f be Function of T,(TOP-REAL m); :: thesis: ( f is open iff for p being Point of T

for V being open Subset of T st p in V holds

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

A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def 8;

then reconsider f1 = f as Function of T,(TopSpaceMetr (Euclid m)) ;

A2: TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #) ;

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

for V being open Subset of T st p in V holds

ex r being positive Real st Ball ((f . p),r) c= f .: V ) :: thesis: ( ( for p being Point of T

for V being open Subset of T st p in V holds

ex r being positive Real st Ball ((f . p),r) c= f .: V ) implies f is open )

proof

assume A6:
for p being Point of T
assume A3:
f is open
; :: thesis: for p being Point of T

for V being open Subset of T st p in V holds

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

let p be Point of T; :: thesis: for V being open Subset of T st p in V holds

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

let V be open Subset of T; :: thesis: ( p in V implies ex r being positive Real st Ball ((f . p),r) c= f .: V )

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

reconsider fp = f . p as Point of (Euclid m) by EUCLID:67;

f1 is open by A3, A1, A2, Th1;

then consider r being positive Real such that

A5: Ball (fp,r) c= f1 .: V by A4, Th4;

Ball ((f . p),r) = Ball (fp,r) by TOPREAL9:13;

hence ex r being positive Real st Ball ((f . p),r) c= f .: V by A5; :: thesis: verum

end;for V being open Subset of T st p in V holds

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

let p be Point of T; :: thesis: for V being open Subset of T st p in V holds

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

let V be open Subset of T; :: thesis: ( p in V implies ex r being positive Real st Ball ((f . p),r) c= f .: V )

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

reconsider fp = f . p as Point of (Euclid m) by EUCLID:67;

f1 is open by A3, A1, A2, Th1;

then consider r being positive Real such that

A5: Ball (fp,r) c= f1 .: V by A4, Th4;

Ball ((f . p),r) = Ball (fp,r) by TOPREAL9:13;

hence ex r being positive Real st Ball ((f . p),r) c= f .: V by A5; :: thesis: verum

for V being open Subset of T st p in V holds

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

for p being Point of T

for V being open Subset of T

for q being Point of (Euclid m) st q = f1 . p & p in V holds

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

proof

then
f1 is open
by Th4;
let p be Point of T; :: thesis: for V being open Subset of T

for q being Point of (Euclid m) st q = f1 . p & p in V holds

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

let V be open Subset of T; :: thesis: for q being Point of (Euclid m) st q = f1 . p & p in V holds

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

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

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

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

then consider r being positive Real such that

A8: Ball ((f . p),r) c= f .: V by A6;

Ball ((f . p),r) = Ball (q,r) by A7, TOPREAL9:13;

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

end;for q being Point of (Euclid m) st q = f1 . p & p in V holds

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

let V be open Subset of T; :: thesis: for q being Point of (Euclid m) st q = f1 . p & p in V holds

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

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

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

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

then consider r being positive Real such that

A8: Ball ((f . p),r) c= f .: V by A6;

Ball ((f . p),r) = Ball (q,r) by A7, TOPREAL9:13;

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

hence f is open by A1, A2, Th1; :: thesis: verum