let RNS be RealNormSpace; for X being set
for f being PartFunc of the carrier of RNS,COMPLEX st f is_Lipschitzian_on X holds
f is_continuous_on X
let X be set ; for f being PartFunc of the carrier of RNS,COMPLEX st f is_Lipschitzian_on X holds
f is_continuous_on X
let f be PartFunc of the carrier of RNS,COMPLEX; ( f is_Lipschitzian_on X implies f is_continuous_on X )
assume A1:
f is_Lipschitzian_on X
; f is_continuous_on X
then consider r being Real such that
A2:
0 < r
and
A3:
for x1, x2 being Point of RNS st x1 in X & x2 in X holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).||
;
A4:
X c= dom f
by A1;
then A5:
dom (f | X) = X
by RELAT_1:62;
now for x0 being Point of RNS st x0 in X holds
f | X is_continuous_in x0let x0 be
Point of
RNS;
( x0 in X implies f | X is_continuous_in x0 )assume A6:
x0 in X
;
f | X is_continuous_in x0now for g being Real st 0 < g holds
ex s9 being Real st
( 0 < s9 & ( for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) )let g be
Real;
( 0 < g implies ex s9 being Real st
( 0 < s9 & ( for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) ) )assume A7:
0 < g
;
ex s9 being Real st
( 0 < s9 & ( for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) )reconsider s =
g / r as
Real ;
take s9 =
s;
( 0 < s9 & ( for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) )A8:
now for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < glet x1 be
Point of
RNS;
( x1 in dom (f | X) & ||.(x1 - x0).|| < s implies |.(((f | X) /. x1) - ((f | X) /. x0)).| < g )assume that A9:
x1 in dom (f | X)
and A10:
||.(x1 - x0).|| < s
;
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g
r * ||.(x1 - x0).|| < (g / r) * r
by A2, A10, XREAL_1:68;
then A11:
r * ||.(x1 - x0).|| < g
by A2, XCMPLX_1:87;
|.((f /. x1) - (f /. x0)).| <= r * ||.(x1 - x0).||
by A3, A5, A6, A9;
then
|.((f /. x1) - (f /. x0)).| < g
by A11, XXREAL_0:2;
then
|.(((f | X) /. x1) - (f /. x0)).| < g
by A9, PARTFUN2:15;
hence
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g
by A5, A6, PARTFUN2:15;
verum end;
(
0 < r " &
s9 = g * (r ") )
by A2, XCMPLX_0:def 9;
hence
(
0 < s9 & ( for
x1 being
Point of
RNS st
x1 in dom (f | X) &
||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) )
by A7, A8, XREAL_1:129;
verum end; hence
f | X is_continuous_in x0
by A5, A6, Th13;
verum end;
hence
f is_continuous_on X
by A4; verum