let m be Nat; :: thesis: for f being Function of (TOP-REAL m),R^1 holds

( f is open iff for p being Point of (TOP-REAL m)

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

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

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

A1: m in NAT by ORDINAL1:def 12;

for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ; :: thesis: f is open

let A be Subset of (TOP-REAL m); :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or f .: A is open )

assume A7: A is open ; :: thesis: f .: A is open

for x being set holds

( x in f .: A iff ex Q being Subset of R^1 st

( Q is open & Q c= f .: A & x in Q ) )

( f is open iff for p being Point of (TOP-REAL m)

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

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

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

A1: m in NAT by ORDINAL1:def 12;

hereby :: thesis: ( ( for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ) implies f is open )

assume A6:
for p being Point of (TOP-REAL m)for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ) implies f is open )

assume A2:
f is open
; :: thesis: for p being Point of (TOP-REAL m)

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

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))

let r be positive Real; :: thesis: ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))

p in Ball (p,r) by A1, TOPGEN_5:13;

then A3: f . p in f .: (Ball (p,r)) by FUNCT_2:35;

f .: (Ball (p,r)) is open by A2;

then consider s being Real such that

A4: s > 0 and

A5: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A3, FRECHET:8;

reconsider s = s as positive Real by A4;

take s = s; :: thesis: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))

thus ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A5; :: thesis: verum

end;for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))

let r be positive Real; :: thesis: ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))

p in Ball (p,r) by A1, TOPGEN_5:13;

then A3: f . p in f .: (Ball (p,r)) by FUNCT_2:35;

f .: (Ball (p,r)) is open by A2;

then consider s being Real such that

A4: s > 0 and

A5: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A3, FRECHET:8;

reconsider s = s as positive Real by A4;

take s = s; :: thesis: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))

thus ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A5; :: thesis: verum

for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ; :: thesis: f is open

let A be Subset of (TOP-REAL m); :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or f .: A is open )

assume A7: A is open ; :: thesis: f .: A is open

for x being set holds

( x in f .: A iff ex Q being Subset of R^1 st

( Q is open & Q c= f .: A & x in Q ) )

proof

hence
f .: A is open
by TOPS_1:25; :: thesis: verum
let x be set ; :: thesis: ( x in f .: A iff ex Q being Subset of R^1 st

( Q is open & Q c= f .: A & x in Q ) )

( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; :: thesis: verum

end;( Q is open & Q c= f .: A & x in Q ) )

hereby :: thesis: ( ex Q being Subset of R^1 st

( Q is open & Q c= f .: A & x in Q ) implies x in f .: A )

thus
( ex Q being Subset of R^1 st ( Q is open & Q c= f .: A & x in Q ) implies x in f .: A )

assume
x in f .: A
; :: thesis: ex Q being Element of K16( the U1 of K409()) st

( Q is open & Q c= f .: A & x in Q )

then consider p being Point of (TOP-REAL m) such that

A8: p in A and

A9: x = f . p by FUNCT_2:65;

reconsider u = p as Point of (Euclid m) by EUCLID:67;

A = Int A by A7, TOPS_1:23;

then consider e being Real such that

A10: e > 0 and

A11: Ball (u,e) c= A by A8, GOBOARD6:5;

A12: Ball (u,e) = Ball (p,e) by TOPREAL9:13;

consider s being positive Real such that

A13: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,e)) by A6, A10;

take Q = R^1 ].((f . p) - s),((f . p) + s).[; :: thesis: ( Q is open & Q c= f .: A & x in Q )

thus Q is open ; :: thesis: ( Q c= f .: A & x in Q )

f .: (Ball (p,e)) c= f .: A by A11, A12, RELAT_1:123;

hence Q c= f .: A by A13; :: thesis: x in Q

thus x in Q by A9, TOPREAL6:15; :: thesis: verum

end;( Q is open & Q c= f .: A & x in Q )

then consider p being Point of (TOP-REAL m) such that

A8: p in A and

A9: x = f . p by FUNCT_2:65;

reconsider u = p as Point of (Euclid m) by EUCLID:67;

A = Int A by A7, TOPS_1:23;

then consider e being Real such that

A10: e > 0 and

A11: Ball (u,e) c= A by A8, GOBOARD6:5;

A12: Ball (u,e) = Ball (p,e) by TOPREAL9:13;

consider s being positive Real such that

A13: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,e)) by A6, A10;

take Q = R^1 ].((f . p) - s),((f . p) + s).[; :: thesis: ( Q is open & Q c= f .: A & x in Q )

thus Q is open ; :: thesis: ( Q c= f .: A & x in Q )

f .: (Ball (p,e)) c= f .: A by A11, A12, RELAT_1:123;

hence Q c= f .: A by A13; :: thesis: x in Q

thus x in Q by A9, TOPREAL6:15; :: thesis: verum

( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; :: thesis: verum