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 real positive number 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 real positive number 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 real positive number 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 #) ;
A3: m in NAT by ORDINAL1:def 13;
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 real positive number 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 real positive number st Ball (f . p),r c= f .: V ) implies f is open )

proof

assume A4: 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 real positive number 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 real positive number st Ball (f . p),r c= f .: V
let V be open Subset of T; :: thesis: ( p in V implies ex r being real positive number st Ball (f . p),r c= f .: V )
assume A5: p in V ; :: thesis: ex r being real positive number st Ball (f . p),r c= f .: V
reconsider fp = f . p as Point of (Euclid m) by EUCLID:71;
f1 is open by A4, A1, A2, Th1;
then consider r being real positive number such that
A6: Ball fp,r c= f1 .: V by A5, Th4;
Ball (f . p),r = Ball fp,r by A3, TOPREAL9:13;
hence ex r being real positive number st Ball (f . p),r c= f .: V by A6; :: thesis: verum

end;

assume A7: for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number 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 real positive number st Ball q,r c= f1 .: V

proof

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 real positive number 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 real positive number 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 real positive number st Ball q,r c= f1 .: V )
assume A8: q = f1 . p ; :: thesis: ( not p in V or ex r being real positive number st Ball q,r c= f1 .: V )
assume p in V ; :: thesis: ex r being real positive number st Ball q,r c= f1 .: V
then consider r being real positive number such that
A9: Ball (f . p),r c= f .: V by A7;
Ball (f . p),r = Ball q,r by A3, A8, TOPREAL9:13;
hence ex r being real positive number st Ball q,r c= f1 .: V by A9; :: thesis: verum

end;

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