let E, F be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of E,F holds

( L is_Lipschitzian_on the carrier of E & L is_uniformly_continuous_on the carrier of E )

let L be Lipschitzian LinearOperator of E,F; :: thesis: ( L is_Lipschitzian_on the carrier of E & L is_uniformly_continuous_on the carrier of E )

consider K being Real such that

A2: ( 0 <= K & ( for x being VECTOR of E holds ||.(L . x).|| <= K * ||.x.|| ) ) by LOPBAN_1:def 8;

set r = K + 1;

A3: K + 0 < K + 1 by XREAL_1:8;

set E0 = the carrier of E;

for x1, x2 being Point of E st x1 in the carrier of E & x2 in the carrier of E holds

||.((L /. x1) - (L /. x2)).|| <= (K + 1) * ||.(x1 - x2).||

hence L is_uniformly_continuous_on the carrier of E by NFCONT_2:9; :: thesis: verum

( L is_Lipschitzian_on the carrier of E & L is_uniformly_continuous_on the carrier of E )

let L be Lipschitzian LinearOperator of E,F; :: thesis: ( L is_Lipschitzian_on the carrier of E & L is_uniformly_continuous_on the carrier of E )

consider K being Real such that

A2: ( 0 <= K & ( for x being VECTOR of E holds ||.(L . x).|| <= K * ||.x.|| ) ) by LOPBAN_1:def 8;

set r = K + 1;

A3: K + 0 < K + 1 by XREAL_1:8;

set E0 = the carrier of E;

for x1, x2 being Point of E st x1 in the carrier of E & x2 in the carrier of E holds

||.((L /. x1) - (L /. x2)).|| <= (K + 1) * ||.(x1 - x2).||

proof

hence
L is_Lipschitzian_on the carrier of E
by A2, FUNCT_2:def 1; :: thesis: L is_uniformly_continuous_on the carrier of E
let x1, x2 be Point of E; :: thesis: ( x1 in the carrier of E & x2 in the carrier of E implies ||.((L /. x1) - (L /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| )

(L /. x1) - (L /. x2) = (L . x1) + ((- 1) * (L . x2)) by RLVECT_1:16

.= (L . x1) + (L . ((- 1) * x2)) by LOPBAN_1:def 5

.= L . (x1 + ((- 1) * x2)) by VECTSP_1:def 20

.= L . (x1 - x2) by RLVECT_1:16 ;

then A8: ||.((L /. x1) - (L /. x2)).|| <= K * ||.(x1 - x2).|| by A2;

K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by A3, XREAL_1:64;

hence ( x1 in the carrier of E & x2 in the carrier of E implies ||.((L /. x1) - (L /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| ) by A8, XXREAL_0:2; :: thesis: verum

end;(L /. x1) - (L /. x2) = (L . x1) + ((- 1) * (L . x2)) by RLVECT_1:16

.= (L . x1) + (L . ((- 1) * x2)) by LOPBAN_1:def 5

.= L . (x1 + ((- 1) * x2)) by VECTSP_1:def 20

.= L . (x1 - x2) by RLVECT_1:16 ;

then A8: ||.((L /. x1) - (L /. x2)).|| <= K * ||.(x1 - x2).|| by A2;

K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by A3, XREAL_1:64;

hence ( x1 in the carrier of E & x2 in the carrier of E implies ||.((L /. x1) - (L /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| ) by A8, XXREAL_0:2; :: thesis: verum

hence L is_uniformly_continuous_on the carrier of E by NFCONT_2:9; :: thesis: verum