let X, Y be RealNormSpace; :: thesis: for f being Lipschitzian LinearOperator of X,Y holds
( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )
let f be Lipschitzian LinearOperator of X,Y; :: thesis: ( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )
consider K being Real such that
A1: 0 <= K and
A2: for x being VECTOR of X holds ||.(f . x).|| <= K * ||.x.|| by LOPBAN_1:def 8;
A3: 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).||
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 that
x in the carrier of X and
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 A2, A4, XREAL_1:38;
hence ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| ; :: thesis: verum
end;
dom f = the carrier of X by FUNCT_2:def 1;
hence f is_Lipschitzian_on the carrier of X by A1, A3, NFCONT_1:def 9; :: thesis: ( f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )
hence A5: f is_continuous_on the carrier of X by NFCONT_1:45; :: thesis: for x being Point of X holds f is_continuous_in x
hereby :: thesis: verum
let x be Point of X; :: thesis: f is_continuous_in x
f | the carrier of X = f by RELSET_1:19;
hence f is_continuous_in x by A5, NFCONT_1:def 7; :: thesis: verum
end;