let X be set ; for p being Real
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_Lipschitzian_on X holds
p (#) f is_Lipschitzian_on X
let p be Real; for S, T being RealNormSpace
for f being PartFunc of S,T st f is_Lipschitzian_on X holds
p (#) f is_Lipschitzian_on X
let S, T be RealNormSpace; for f being PartFunc of S,T st f is_Lipschitzian_on X holds
p (#) f is_Lipschitzian_on X
let f be PartFunc of S,T; ( f is_Lipschitzian_on X implies p (#) f is_Lipschitzian_on X )
assume A1:
f is_Lipschitzian_on X
; p (#) f is_Lipschitzian_on X
then consider s being Real such that
A2:
0 < s
and
A3:
for x1, x2 being Point of S st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).||
;
X c= dom f
by A1;
hence A4:
X c= dom (p (#) f)
by VFUNCT_1:def 4; NFCONT_1:def 9 ex r being Real st
( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= r * ||.(x1 - x2).|| ) )
per cases
( p = 0 or p <> 0 )
;
suppose A9:
p <> 0
;
ex r being Real st
( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= r * ||.(x1 - x2).|| ) )take g =
|.p.| * s;
( 0 < g & ( for x1, x2 being Point of S st x1 in X & x2 in X holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).|| ) )
0 < |.p.|
by A9, COMPLEX1:47;
then
0 * s < |.p.| * s
by A2, XREAL_1:68;
hence
0 < g
;
for x1, x2 being Point of S st x1 in X & x2 in X holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).||let x1,
x2 be
Point of
S;
( x1 in X & x2 in X implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).|| )assume that A10:
x1 in X
and A11:
x2 in X
;
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).||
0 <= |.p.|
by COMPLEX1:46;
then A12:
|.p.| * ||.((f /. x1) - (f /. x2)).|| <= |.p.| * (s * ||.(x1 - x2).||)
by A3, A10, A11, XREAL_1:64;
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| =
||.((p * (f /. x1)) - ((p (#) f) /. x2)).||
by A4, A10, VFUNCT_1:def 4
.=
||.((p * (f /. x1)) - (p * (f /. x2))).||
by A4, A11, VFUNCT_1:def 4
.=
||.(p * ((f /. x1) - (f /. x2))).||
by RLVECT_1:34
.=
|.p.| * ||.((f /. x1) - (f /. x2)).||
by NORMSP_1:def 1
;
hence
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).||
by A12;
verum end; end;