let CNS be ComplexNormSpace; for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds
f1 - f2 is_Lipschitzian_on X /\ X1
let RNS be RealNormSpace; for X, X1 being set
for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds
f1 - f2 is_Lipschitzian_on X /\ X1
let X, X1 be set ; for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds
f1 - f2 is_Lipschitzian_on X /\ X1
let f1, f2 be PartFunc of CNS,RNS; ( f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 implies f1 - f2 is_Lipschitzian_on X /\ X1 )
assume that
A1:
f1 is_Lipschitzian_on X
and
A2:
f2 is_Lipschitzian_on X1
; f1 - f2 is_Lipschitzian_on X /\ X1
A3:
f1 is_Lipschitzian_on X /\ X1
by A1, Th98, XBOOLE_1:17;
then consider s being Real such that
A4:
0 < s
and
A5:
for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||.((f1 /. x1) - (f1 /. x2)).|| <= s * ||.(x1 - x2).||
;
A6:
f2 is_Lipschitzian_on X /\ X1
by A2, Th98, XBOOLE_1:17;
then A7:
X /\ X1 c= dom f2
;
X /\ X1 c= dom f1
by A3;
then
X /\ X1 c= (dom f1) /\ (dom f2)
by A7, XBOOLE_1:19;
hence A8:
X /\ X1 c= dom (f1 - f2)
by VFUNCT_1:def 2; NCFCONT1:def 18 ex r being Real st
( 0 < r & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= r * ||.(x1 - x2).|| ) )
consider g being Real such that
A9:
0 < g
and
A10:
for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||.((f2 /. x1) - (f2 /. x2)).|| <= g * ||.(x1 - x2).||
by A6;
take p = s + g; ( 0 < p & ( for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).|| ) )
0 + 0 < s + g
by A4, A9;
hence
0 < p
; for x1, x2 being Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).||
let x1, x2 be Point of CNS; ( x1 in X /\ X1 & x2 in X /\ X1 implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).|| )
assume that
A11:
x1 in X /\ X1
and
A12:
x2 in X /\ X1
; ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).||
A13:
||.((f2 /. x1) - (f2 /. x2)).|| <= g * ||.(x1 - x2).||
by A10, A11, A12;
||.((f1 /. x1) - (f1 /. x2)).|| <= s * ||.(x1 - x2).||
by A5, A11, A12;
then A14:
||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| <= (s * ||.(x1 - x2).||) + (g * ||.(x1 - x2).||)
by A13, XREAL_1:7;
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| =
||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).||
by A8, A11, VFUNCT_1:def 2
.=
||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).||
by A8, A12, VFUNCT_1:def 2
.=
||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).||
by RLVECT_1:27
.=
||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).||
by RLVECT_1:28
.=
||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).||
by RLVECT_1:28
.=
||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).||
by RLVECT_1:27
;
then
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||
by NORMSP_1:3;
hence
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).||
by A14, XXREAL_0:2; verum