let T be non empty TopSpace; :: thesis: for f being Function of T,R^1 holds

( f is continuous iff for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )

let f be Function of T,R^1; :: thesis: ( f is continuous iff for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )

thus ( f is continuous implies for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) :: thesis: ( ( for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) implies f is continuous )

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ; :: thesis: f is continuous

for p being Point of T

for V being Subset of R^1 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 )

( f is continuous iff for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )

let f be Function of T,R^1; :: thesis: ( f is continuous iff for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )

thus ( f is continuous implies for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) :: thesis: ( ( for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) implies f is continuous )

proof

assume A3:
for p being Point of T
assume A1:
f is continuous
; :: thesis: for p being Point of T

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )

let p be Point of T; :: thesis: for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )

let r be positive Real; :: thesis: ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )

A2: f . p in ].((f . p) - r),((f . p) + r).[ by TOPREAL6:15;

R^1 ].((f . p) - r),((f . p) + r).[ is open ;

then ex W being Subset of T st

( p in W & W is open & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A1, A2, JGRAPH_2:10;

hence ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ; :: thesis: verum

end;for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )

let p be Point of T; :: thesis: for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )

let r be positive Real; :: thesis: ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )

A2: f . p in ].((f . p) - r),((f . p) + r).[ by TOPREAL6:15;

R^1 ].((f . p) - r),((f . p) + r).[ is open ;

then ex W being Subset of T st

( p in W & W is open & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A1, A2, JGRAPH_2:10;

hence ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ; :: thesis: verum

for r being positive Real ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ; :: thesis: f is continuous

for p being Point of T

for V being Subset of R^1 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

hence
f is continuous
by JGRAPH_2:10; :: thesis: verum
let p be Point of T; :: thesis: for V being Subset of R^1 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 R^1; :: 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 ) )

assume V is open ; :: thesis: ex W being Subset of T st

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

then consider r being Real such that

A5: r > 0 and

A6: ].((f . p) - r),((f . p) + r).[ c= V by A4, FRECHET:8;

ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A3, A5;

hence ex W being Subset of T st

( p in W & W is open & f .: W c= V ) by A6, XBOOLE_1:1; :: thesis: verum

end;ex W being Subset of T st

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

let V be Subset of R^1; :: 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 ) )

assume V is open ; :: thesis: ex W being Subset of T st

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

then consider r being Real such that

A5: r > 0 and

A6: ].((f . p) - r),((f . p) + r).[ c= V by A4, FRECHET:8;

ex W being open Subset of T st

( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A3, A5;

hence ex W being Subset of T st

( p in W & W is open & f .: W c= V ) by A6, XBOOLE_1:1; :: thesis: verum