let m be Nat; :: thesis: for T being non empty TopSpace
for f being Function of T,(TOP-REAL m) holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )
let T be non empty TopSpace; :: thesis: for f being Function of T,(TOP-REAL m) holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )
let f be Function of T,(TOP-REAL m); :: thesis: ( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )
A1: m in NAT by ORDINAL1:def 12;
thus ( f is continuous implies for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) ) :: thesis: ( ( for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) ) implies f is continuous )

proof

assume A2: f is continuous ; :: thesis: for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) )
let p be Point of T; :: thesis: for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) )
let r be real positive number ; :: thesis: ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) )
f . p in Ball ((f . p),r) by A1, TOPGEN_5:13;
then ex W being Subset of T st
( p in W & W is open & f .: W c= Ball ((f . p),r) ) by A2, JGRAPH_2:10;
hence ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) ; :: thesis: verum

end;

assume A3: for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) ; :: thesis: f is continuous
for p being Point of T
for V being Subset of (TOP-REAL m) st f . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & f .: W c= V )

proof

let p be Point of T; :: thesis: for V being Subset of (TOP-REAL m) st f . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & f .: W c= V )
let V be Subset of (TOP-REAL m); :: thesis: ( f . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & f .: W c= V ) )
assume A4: f . p in V ; :: thesis: ( not V is open or ex W being Subset of T st
( p in W & W is open & f .: W c= V ) )
reconsider u = f . p as Point of (Euclid m) by EUCLID:67;
assume V is open ; :: thesis: ex W being Subset of T st
( p in W & W is open & f .: W c= V )
then Int V = V by TOPS_1:23;
then consider e being real number such that
A5: e > 0 and
A6: Ball (u,e) c= V by A1, A4, GOBOARD6:5;
A7: Ball (u,e) = Ball ((f . p),e) by A1, TOPREAL9:13;
ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),e) ) by A3, A5;
hence ex W being Subset of T st
( p in W & W is open & f .: W c= V ) by A6, A7, XBOOLE_1:1; :: thesis: verum

end;

hence f is continuous by JGRAPH_2:10; :: thesis: verum