let T be non empty TopSpace; 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; 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; ( 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 ) ) )
( ( 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
;
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;
( 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
;
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
;
( 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;
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;
( y in H implies |.((f . y) - (f . x)).| < e )
assume
y in H
;
|.((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;
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 ) )
; f is_continuous_at x
hence
f is_continuous_at x
by TMAP_1:43; verum