let T be non empty TopSpace; 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; ( 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 )
( ( 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 A1:
f is
open
;
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;
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 .: Vlet V be
open Subset of
T;
( p in V implies ex r being positive Real st ].((f . p) - r),((f . p) + r).[ c= f .: V )
assume A2:
p in V
;
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;
verum
end;
assume A4:
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
; 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
let p be
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 .: Vlet V be
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 .: Vlet q be
Point of
RealSpace;
( q = f . p & p in V implies ex r being positive Real st Ball (q,r) c= f .: V )
assume A5:
q = f . p
;
( not p in V or ex r being positive Real st Ball (q,r) c= f .: V )
assume
p in V
;
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;
verum
end;
hence
f is open
by Th4; verum