let X, Y be ComplexNormSpace; :: thesis: for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds

f is Lipschitzian

let f be LinearOperator of X,Y; :: thesis: ( ( for x being VECTOR of X holds f . x = 0. Y ) implies f is Lipschitzian )

assume A1: for x being VECTOR of X holds f . x = 0. Y ; :: thesis: f is Lipschitzian

thus ( 0 <= 0 & ( for x being VECTOR of X holds ||.(f . x).|| <= 0 * ||.x.|| ) ) by A2; :: thesis: verum

f is Lipschitzian

let f be LinearOperator of X,Y; :: thesis: ( ( for x being VECTOR of X holds f . x = 0. Y ) implies f is Lipschitzian )

assume A1: for x being VECTOR of X holds f . x = 0. Y ; :: thesis: f is Lipschitzian

A2: now :: thesis: for x being VECTOR of X holds ||.(f . x).|| = 0 * ||.x.||

take
0
; :: according to CLOPBAN1:def 6 :: thesis: ( 0 <= 0 & ( for x being VECTOR of X holds ||.(f . x).|| <= 0 * ||.x.|| ) )let x be VECTOR of X; :: thesis: ||.(f . x).|| = 0 * ||.x.||

thus ||.(f . x).|| = ||.(0. Y).|| by A1

.= 0 * ||.x.|| by CLVECT_1:102 ; :: thesis: verum

end;thus ||.(f . x).|| = ||.(0. Y).|| by A1

.= 0 * ||.x.|| by CLVECT_1:102 ; :: thesis: verum

thus ( 0 <= 0 & ( for x being VECTOR of X holds ||.(f . x).|| <= 0 * ||.x.|| ) ) by A2; :: thesis: verum