let X be set ; for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds
f | X is continuous
let f be PartFunc of REAL,REAL; ( X c= dom f & f | X is uniformly_continuous implies f | X is continuous )
assume A1:
X c= dom f
; ( not f | X is uniformly_continuous or f | X is continuous )
assume A2:
f | X is uniformly_continuous
; f | X is continuous
now for x0, r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) )let x0,
r be
Real;
( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) ) )assume that A3:
x0 in X
and A4:
0 < r
;
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) )A5:
x0 in dom (f | X)
by A1, A3, RELAT_1:62;
consider s being
Real such that A6:
0 < s
and A7:
for
x1,
x2 being
Real st
x1 in dom (f | X) &
x2 in dom (f | X) &
|.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r
by A2, A4, Th1;
reconsider s =
s as
Real ;
take s =
s;
( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) )thus
0 < s
by A6;
for x1 being Real st x1 in X & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < rlet x1 be
Real;
( x1 in X & |.(x1 - x0).| < s implies |.((f . x1) - (f . x0)).| < r )assume that A8:
x1 in X
and A9:
|.(x1 - x0).| < s
;
|.((f . x1) - (f . x0)).| < r
x1 in dom (f | X)
by A1, A8, RELAT_1:62;
hence
|.((f . x1) - (f . x0)).| < r
by A7, A9, A5;
verum end;
hence
f | X is continuous
by A1, FCONT_1:14; verum