let X, Y be RealNormSpace; :: thesis: 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; :: thesis: ( f is Lipschitzian iff f is_continuous_on the carrier of X )

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;

( f is Lipschitzian iff f is_continuous_on the carrier of X )

let f be LinearOperator of X,Y; :: thesis: ( f is Lipschitzian iff f is_continuous_on the carrier of X )

hereby :: thesis: ( f is_continuous_on the carrier of X implies f is Lipschitzian )

assume A5:
f is_continuous_on the carrier of X
; :: thesis: f is Lipschitzian assume A1:
f is Lipschitzian
; :: thesis: f is_continuous_on the carrier of X

A2: dom f = the carrier of X by FUNCT_2:def 1;

consider K being Real such that

A3: ( 0 <= K & ( for x being VECTOR of X holds ||.(f . x).|| <= K * ||.x.|| ) ) by A1;

end;A2: dom f = the carrier of X by FUNCT_2:def 1;

consider K being Real such that

A3: ( 0 <= K & ( for x being VECTOR of X holds ||.(f . x).|| <= K * ||.x.|| ) ) by A1;

now :: thesis: for x, y being Point of X st x in the carrier of X & y in the carrier of X holds

||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).||

hence
f is_continuous_on the carrier of X
by NFCONT_1:45, A2, A3, NFCONT_1:def 9; :: thesis: verum||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).||

let x, y be Point of X; :: thesis: ( x in the carrier of X & y in the carrier of X implies ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| )

assume ( x in the carrier of X & y in the carrier of X ) ; :: thesis: ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).||

(f /. x) - (f /. y) = (f . x) + ((- 1) * (f . y)) by RLVECT_1:16;

then (f /. x) - (f /. y) = (f . x) + (f . ((- 1) * y)) by LOPBAN_1:def 5;

then (f /. x) - (f /. y) = f . (x + ((- 1) * y)) by VECTSP_1:def 20;

then A4: (f /. x) - (f /. y) = f . (x + (- y)) by RLVECT_1:16;

||.((f /. x) - (f /. y)).|| <= (K * ||.(x - y).||) + ||.(x - y).|| by A3, A4, XREAL_1:38;

hence ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| ; :: thesis: verum

end;assume ( x in the carrier of X & y in the carrier of X ) ; :: thesis: ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).||

(f /. x) - (f /. y) = (f . x) + ((- 1) * (f . y)) by RLVECT_1:16;

then (f /. x) - (f /. y) = (f . x) + (f . ((- 1) * y)) by LOPBAN_1:def 5;

then (f /. x) - (f /. y) = f . (x + ((- 1) * y)) by VECTSP_1:def 20;

then A4: (f /. x) - (f /. y) = f . (x + (- y)) by RLVECT_1:16;

||.((f /. x) - (f /. y)).|| <= (K * ||.(x - y).||) + ||.(x - y).|| by A3, A4, XREAL_1:38;

hence ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| ; :: thesis: verum

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 :: thesis: for x1 being VECTOR of X holds ||.(f . x1).|| <= (2 / s) * ||.x1.||

hence
f is Lipschitzian
by A7; :: thesis: verumlet x1 be VECTOR of X; :: thesis: ||.(f . b_{1}).|| <= (2 / s) * ||.b_{1}.||

A8: 0. Y = f /. (0. X) by Th3;

end;A8: 0. Y = f /. (0. X) by Th3;

per cases
( x1 = 0. X or x1 <> 0. X )
;

end;

suppose A9:
x1 <> 0. X
; :: thesis: ||.(f . b_{1}).|| <= (2 / s) * ||.b_{1}.||

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; :: thesis: verum

end;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; :: thesis: verum