let T be non empty TopSpace; :: thesis: for f being Function of T,R^1
for x being Point of T holds
( f is_continuous_at x iff for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) ) )
let f be Function of T,R^1; :: thesis: for x being Point of T holds
( f is_continuous_at x iff for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) ) )
let x be Point of T; :: thesis: ( f is_continuous_at x iff for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) ) )
thus ( f is_continuous_at x implies for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) ) ) :: thesis: ( ( for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) ) ) implies f is_continuous_at x )
proof
reconsider fx = f . x as Point of RealSpace by TOPMETR:12, TOPMETR:def 6;
assume A1: f is_continuous_at x ; :: thesis: for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) )
let e be Real; :: thesis: ( e > 0 implies ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) ) )
assume A2: e > 0 ; :: thesis: ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) )
reconsider G = Ball (fx,e) as Subset of R^1 by TOPMETR:12, TOPMETR:def 6;
( G is open & fx in G ) by A2, GOBOARD6:1, TOPMETR:14, TOPMETR:def 6;
then consider H being Subset of T such that
A3: ( H is open & x in H ) and
A4: f .: H c= G by A1, TMAP_1:43;
take H ; :: thesis: ( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) )
thus ( H is open & x in H ) by A3; :: thesis: for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e
A5: dom f = the carrier of T by FUNCT_2:def 1;
let y be Point of T; :: thesis: ( y in H implies |.((f . y) - (f . x)).| < e )
assume y in H ; :: thesis: |.((f . y) - (f . x)).| < e
then A6: f . y in f .: H by A5, FUNCT_1:def 6;
then f . y in G by A4;
then reconsider fy = f . y as Point of RealSpace ;
dist (fy,fx) < e by A4, A6, METRIC_1:11;
hence |.((f . y) - (f . x)).| < e by TOPMETR:11; :: thesis: verum
end;
assume A7: for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) ) ; :: thesis: f is_continuous_at x
now :: thesis: for G being Subset of R^1 st G is open & f . x in G holds
ex H being Subset of T st
( H is open & x in H & f .: H c= G )
reconsider fx = f . x as Point of RealSpace by TOPMETR:12, TOPMETR:def 6;
let G be Subset of R^1; :: thesis: ( G is open & f . x in G implies ex H being Subset of T st
( H is open & x in H & f .: H c= G ) )
assume ( G is open & f . x in G ) ; :: thesis: ex H being Subset of T st
( H is open & x in H & f .: H c= G )
then consider r being Real such that
A8: r > 0 and
A9: Ball (fx,r) c= G by TOPMETR:15, TOPMETR:def 6;
consider H being Subset of T such that
A10: ( H is open & x in H ) and
A11: for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < r by A7, A8;
take H = H; :: thesis: ( H is open & x in H & f .: H c= G )
thus ( H is open & x in H ) by A10; :: thesis: f .: H c= G
thus f .: H c= G :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f .: H or a in G )
assume a in f .: H ; :: thesis: a in G
then consider y being object such that
A12: y in dom f and
A13: y in H and
A14: a = f . y by FUNCT_1:def 6;
reconsider y = y as Point of T by A12;
reconsider fy = f . y as Point of RealSpace by TOPMETR:12, TOPMETR:def 6;
|.((f . y) - (f . x)).| < r by A11, A13;
then |.(- ((f . y) - (f . x))).| < r by COMPLEX1:52;
then |.((f . x) - (f . y)).| < r ;
then dist (fx,fy) < r by TOPMETR:11;
then fy in Ball (fx,r) by METRIC_1:11;
hence a in G by A9, A14; :: thesis: verum
end;
end;
hence f is_continuous_at x by TMAP_1:43; :: thesis: verum