let m be Nat; :: thesis: for T being non empty TopSpace

for f being Function of (TOP-REAL m),T holds

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

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

ex s being positive Real st f .: (Ball (p,s)) c= V )

let T be non empty TopSpace; :: thesis: for f being Function of (TOP-REAL m),T holds

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

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

ex s being positive Real st f .: (Ball (p,s)) c= V )

let f be Function of (TOP-REAL m),T; :: thesis: ( f is continuous iff for p being Point of (TOP-REAL m)

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

ex s being positive Real st f .: (Ball (p,s)) c= V )

A1: m in NAT by ORDINAL1:def 12;

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

ex s being positive Real st f .: (Ball (p,s)) c= V ; :: thesis: f is continuous

for p being Point of (TOP-REAL m)

for V being Subset of T st f . p in V & V is open holds

ex W being Subset of (TOP-REAL m) st

( p in W & W is open & f .: W c= V )

for f being Function of (TOP-REAL m),T holds

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

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

ex s being positive Real st f .: (Ball (p,s)) c= V )

let T be non empty TopSpace; :: thesis: for f being Function of (TOP-REAL m),T holds

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

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

ex s being positive Real st f .: (Ball (p,s)) c= V )

let f be Function of (TOP-REAL m),T; :: thesis: ( f is continuous iff for p being Point of (TOP-REAL m)

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

ex s being positive Real st f .: (Ball (p,s)) c= V )

A1: m in NAT by ORDINAL1:def 12;

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

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

ex s being positive Real st f .: (Ball (p,s)) c= V ) implies f is continuous )

assume A8:
for p being Point of (TOP-REAL m)for V being open Subset of T st f . p in V holds

ex s being positive Real st f .: (Ball (p,s)) c= V ) implies f is continuous )

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

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

ex s being positive Real st f .: (Ball (p,s)) c= V

let p be Point of (TOP-REAL m); :: thesis: for V being open Subset of T st f . p in V holds

ex s being positive Real st f .: (Ball (p,s)) c= V

let V be open Subset of T; :: thesis: ( f . p in V implies ex s being positive Real st f .: (Ball (p,s)) c= V )

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

then consider W being Subset of (TOP-REAL m) such that

A3: p in W and

A4: W is open and

A5: f .: W c= V by A2, JGRAPH_2:10;

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

Int W = W by A4, TOPS_1:23;

then consider s being Real such that

A6: s > 0 and

A7: Ball (u,s) c= W by A3, GOBOARD6:5;

reconsider s = s as positive Real by A6;

take s = s; :: thesis: f .: (Ball (p,s)) c= V

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

then f .: (Ball (p,s)) c= f .: W by A7, RELAT_1:123;

hence f .: (Ball (p,s)) c= V by A5; :: thesis: verum

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

ex s being positive Real st f .: (Ball (p,s)) c= V

let p be Point of (TOP-REAL m); :: thesis: for V being open Subset of T st f . p in V holds

ex s being positive Real st f .: (Ball (p,s)) c= V

let V be open Subset of T; :: thesis: ( f . p in V implies ex s being positive Real st f .: (Ball (p,s)) c= V )

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

then consider W being Subset of (TOP-REAL m) such that

A3: p in W and

A4: W is open and

A5: f .: W c= V by A2, JGRAPH_2:10;

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

Int W = W by A4, TOPS_1:23;

then consider s being Real such that

A6: s > 0 and

A7: Ball (u,s) c= W by A3, GOBOARD6:5;

reconsider s = s as positive Real by A6;

take s = s; :: thesis: f .: (Ball (p,s)) c= V

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

then f .: (Ball (p,s)) c= f .: W by A7, RELAT_1:123;

hence f .: (Ball (p,s)) c= V by A5; :: thesis: verum

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

ex s being positive Real st f .: (Ball (p,s)) c= V ; :: thesis: f is continuous

for p being Point of (TOP-REAL m)

for V being Subset of T st f . p in V & V is open holds

ex W being Subset of (TOP-REAL m) st

( p in W & W is open & f .: W c= V )

proof

hence
f is continuous
by JGRAPH_2:10; :: thesis: verum
let p be Point of (TOP-REAL m); :: thesis: for V being Subset of T st f . p in V & V is open holds

ex W being Subset of (TOP-REAL m) st

( p in W & W is open & f .: W c= V )

let V be Subset of T; :: thesis: ( f . p in V & V is open implies ex W being Subset of (TOP-REAL m) st

( p in W & W is open & f .: W c= V ) )

assume that

A9: f . p in V and

A10: V is open ; :: thesis: ex W being Subset of (TOP-REAL m) st

( p in W & W is open & f .: W c= V )

consider s being positive Real such that

A11: f .: (Ball (p,s)) c= V by A8, A9, A10;

take W = Ball (p,s); :: thesis: ( p in W & W is open & f .: W c= V )

thus p in W by A1, TOPGEN_5:13; :: thesis: ( W is open & f .: W c= V )

thus W is open ; :: thesis: f .: W c= V

thus f .: W c= V by A11; :: thesis: verum

end;ex W being Subset of (TOP-REAL m) st

( p in W & W is open & f .: W c= V )

let V be Subset of T; :: thesis: ( f . p in V & V is open implies ex W being Subset of (TOP-REAL m) st

( p in W & W is open & f .: W c= V ) )

assume that

A9: f . p in V and

A10: V is open ; :: thesis: ex W being Subset of (TOP-REAL m) st

( p in W & W is open & f .: W c= V )

consider s being positive Real such that

A11: f .: (Ball (p,s)) c= V by A8, A9, A10;

take W = Ball (p,s); :: thesis: ( p in W & W is open & f .: W c= V )

thus p in W by A1, TOPGEN_5:13; :: thesis: ( W is open & f .: W c= V )

thus W is open ; :: thesis: f .: W c= V

thus f .: W c= V by A11; :: thesis: verum