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).||
proof
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;
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
hence L is_uniformly_continuous_on the carrier of E by NFCONT_2:9; :: thesis: verum