let T be non empty TopSpace; :: thesis: for f being Function of T,R^1 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 ].((f . p) - r),((f . p) + r).[ c= f .: V )

let f be Function of T,R^1; :: 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 ].((f . p) - r),((f . p) + r).[ c= f .: V )

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 ].((f . p) - r),((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 ].((f . p) - r),((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 ].((f . p) - r),((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 RealSpace 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 T

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

ex r being positive Real st ].((f . p) - r),((f . p) + r).[ c= f .: V )

let f be Function of T,R^1; :: 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 ].((f . p) - r),((f . p) + r).[ c= f .: V )

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 ].((f . p) - r),((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 ].((f . p) - r),((f . p) + r).[ c= f .: V ) implies f is open )

proof

assume A4:
for p being Point of T
assume A1:
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 ].((f . p) - r),((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 ].((f . p) - r),((f . p) + r).[ c= f .: V

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

assume A2: p in V ; :: thesis: ex r being positive Real st ].((f . p) - r),((f . p) + r).[ c= f .: V

reconsider fp = f . p as Point of RealSpace ;

consider r being positive Real such that

A3: Ball (fp,r) c= f .: V by A1, A2, Th4;

].(fp - r),(fp + r).[ = Ball (fp,r) by FRECHET:7;

hence ex r being positive Real st ].((f . p) - r),((f . p) + r).[ c= f .: V by A3; :: thesis: verum

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

ex r being positive Real st ].((f . p) - r),((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 ].((f . p) - r),((f . p) + r).[ c= f .: V

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

assume A2: p in V ; :: thesis: ex r being positive Real st ].((f . p) - r),((f . p) + r).[ c= f .: V

reconsider fp = f . p as Point of RealSpace ;

consider r being positive Real such that

A3: Ball (fp,r) c= f .: V by A1, A2, Th4;

].(fp - r),(fp + r).[ = Ball (fp,r) by FRECHET:7;

hence ex r being positive Real st ].((f . p) - r),((f . p) + r).[ c= f .: V by A3; :: thesis: verum

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

ex r being positive Real st ].((f . p) - r),((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 RealSpace 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 T; :: thesis: for V being open Subset of T

for q being Point of RealSpace 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 T; :: thesis: for q being Point of RealSpace 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 RealSpace; :: 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 )

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

then consider r being positive Real such that

A6: ].((f . p) - r),((f . p) + r).[ c= f .: V by A4;

].(q - r),(q + r).[ = Ball (q,r) by FRECHET:7;

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

end;for q being Point of RealSpace 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 T; :: thesis: for q being Point of RealSpace 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 RealSpace; :: 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 )

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

then consider r being positive Real such that

A6: ].((f . p) - r),((f . p) + r).[ c= f .: V by A4;

].(q - r),(q + r).[ = Ball (q,r) by FRECHET:7;

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