let m be Nat; for f being Function of R^1,(TOP-REAL m) holds
( f is open iff for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )
let f be Function of R^1,(TOP-REAL m); ( f is open iff for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )
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 R^1,(TopSpaceMetr (Euclid m)) ;
thus
( f is open implies for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )
( ( for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) implies f is open )proof
assume A2:
f is
open
;
for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[
let p be
Point of
R^1;
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[let r be
positive Real;
ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[
reconsider p1 =
p as
Point of
RealSpace ;
reconsider q1 =
f . p as
Point of
(Euclid m) by EUCLID:67;
f1 is
open
by A1, A2, Th1;
then consider s being
positive Real such that A3:
Ball (
q1,
s)
c= f1 .: (Ball (p1,r))
by Th6;
(
].(p - r),(p + r).[ = Ball (
p1,
r) &
Ball (
(f . p),
s)
= Ball (
q1,
s) )
by FRECHET:7, TOPREAL9:13;
hence
ex
s being
positive Real st
Ball (
(f . p),
s)
c= f .: ].(p - r),(p + r).[
by A3;
verum
end;
assume A4:
for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[
; f is open
for p being Point of RealSpace
for q being Point of (Euclid m)
for r being positive Real st q = f1 . p holds
ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))
proof
let p be
Point of
RealSpace;
for q being Point of (Euclid m)
for r being positive Real st q = f1 . p holds
ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))let q be
Point of
(Euclid m);
for r being positive Real st q = f1 . p holds
ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))let r be
positive Real;
( q = f1 . p implies ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r)) )
assume A5:
q = f1 . p
;
ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))
reconsider p1 =
p as
Point of
R^1 ;
consider s being
positive Real such that A6:
Ball (
(f . p1),
s)
c= f .: ].(p1 - r),(p1 + r).[
by A4;
(
].(p1 - r),(p1 + r).[ = Ball (
p,
r) &
Ball (
(f . p1),
s)
= Ball (
q,
s) )
by A5, FRECHET:7, TOPREAL9:13;
hence
ex
s being
positive Real st
Ball (
q,
s)
c= f1 .: (Ball (p,r))
by A6;
verum
end;
then
f1 is open
by Th6;
hence
f is open
by A1, Th1; verum