let S be RealNormSpace; for Y being Subset of S
for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds
f is_continuous_on Y
let Y be Subset of S; for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds
f is_continuous_on Y
let f be PartFunc of S,S; ( Y c= dom f & f | Y = id Y implies f is_continuous_on Y )
assume that
A1:
Y c= dom f
and
A2:
f | Y = id Y
; f is_continuous_on Y
now for x1, x2 being Point of S st x1 in Y & x2 in Y holds
||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||let x1,
x2 be
Point of
S;
( x1 in Y & x2 in Y implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| )assume that A3:
x1 in Y
and A4:
x2 in Y
;
||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||
x1 in (dom f) /\ Y
by A1, A3, XBOOLE_0:def 4;
then A5:
x1 in dom (f | Y)
by RELAT_1:61;
(f | Y) . x1 = x1
by A2, A3, FUNCT_1:17;
then
f . x1 = x1
by A5, FUNCT_1:47;
then A6:
f /. x1 = x1
by A1, A3, PARTFUN1:def 6;
x2 in (dom f) /\ Y
by A1, A4, XBOOLE_0:def 4;
then A7:
x2 in dom (f | Y)
by RELAT_1:61;
(f | Y) . x2 = x2
by A2, A4, FUNCT_1:17;
then
f . x2 = x2
by A7, FUNCT_1:47;
hence
||.((f /. x1) - (f /. x2)).|| <= 1
* ||.(x1 - x2).||
by A1, A4, A6, PARTFUN1:def 6;
verum end;
then
f is_Lipschitzian_on Y
by A1;
hence
f is_continuous_on Y
by Th45; verum