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
A2: now :: thesis: 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;
take 0 ; :: according to CLOPBAN1:def 6 :: thesis: ( 0 <= 0 & ( for x being VECTOR of X holds ||.(f . x).|| <= 0 * ||.x.|| ) )
thus ( 0 <= 0 & ( for x being VECTOR of X holds ||.(f . x).|| <= 0 * ||.x.|| ) ) by A2; :: thesis: verum