let X, Y be RealNormSpace; for f being LinearOperator of X,Y holds
( f is Lipschitzian iff f is_continuous_on the carrier of X )
let f be LinearOperator of X,Y; ( f is Lipschitzian iff f is_continuous_on the carrier of X )
assume A5:
f is_continuous_on the carrier of X
; f is Lipschitzian
A6:
dom f = the carrier of X
by FUNCT_2:def 1;
f | the carrier of X = f
;
then
f is_continuous_in 0. X
by A5, NFCONT_1:def 7;
then consider s being Real such that
A7:
( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - (0. X)).|| < s holds
||.((f /. x1) - (f /. (0. X))).|| < 1 ) )
by NFCONT_1:7;
set r1 = 2 / s;
now for x1 being VECTOR of X holds ||.(f . x1).|| <= (2 / s) * ||.x1.||let x1 be
VECTOR of
X;
||.(f . b1).|| <= (2 / s) * ||.b1.||A8:
0. Y = f /. (0. X)
by Th3;
per cases
( x1 = 0. X or x1 <> 0. X )
;
suppose A9:
x1 <> 0. X
;
||.(f . b1).|| <= (2 / s) * ||.b1.||then A10:
||.x1.|| <> 0
by NORMSP_0:def 5;
set r3 =
(s / 2) / ||.x1.||;
0 < s / 2
by A7, XREAL_1:215;
then A11:
0 < (s / 2) / ||.x1.||
by A10, XREAL_1:139;
set x2 =
((s / 2) / ||.x1.||) * x1;
A12: 1
/ ((s / 2) / ||.x1.||) =
||.x1.|| / (s / 2)
by XCMPLX_1:57
.=
||.x1.|| * (2 / s)
by XCMPLX_1:79
;
||.(((s / 2) / ||.x1.||) * x1).|| =
|.((s / 2) / ||.x1.||).| * ||.x1.||
by NORMSP_1:def 1
.=
((s / 2) / ||.x1.||) * ||.x1.||
by A7, ABSVALUE:def 1
.=
s / 2
by A9, NORMSP_0:def 5, XCMPLX_1:87
;
then
||.(((s / 2) / ||.x1.||) * x1).|| < s
by A7, XREAL_1:216;
then
||.((((s / 2) / ||.x1.||) * x1) - (0. X)).|| < s
by RLVECT_1:13;
then A13:
||.((f /. (((s / 2) / ||.x1.||) * x1)) - (f /. (0. X))).|| < 1
by A6, A7;
||.(f /. (((s / 2) / ||.x1.||) * x1)).|| =
||.(((s / 2) / ||.x1.||) * (f . x1)).||
by LOPBAN_1:def 5
.=
|.((s / 2) / ||.x1.||).| * ||.(f . x1).||
by NORMSP_1:def 1
.=
((s / 2) / ||.x1.||) * ||.(f . x1).||
by A7, ABSVALUE:def 1
;
then
((s / 2) / ||.x1.||) * ||.(f . x1).|| < 1
by A13, A8, RLVECT_1:13;
hence
||.(f . x1).|| <= (2 / s) * ||.x1.||
by A12, A11, XREAL_1:81;
verum end; end; end;
hence
f is Lipschitzian
by A7; verum