let X, Y, Z be RealNormSpace; :: thesis: for f being BilinearOperator of X,Y,Z st ( for x being VECTOR of X
for y being VECTOR of Y holds f . (x,y) = 0. Z ) holds
f is Lipschitzian
let f be BilinearOperator of X,Y,Z; :: thesis: ( ( for x being VECTOR of X
for y being VECTOR of Y holds f . (x,y) = 0. Z ) implies f is Lipschitzian )
assume A1: for x being VECTOR of X
for y being VECTOR of Y holds f . (x,y) = 0. Z ; :: thesis: f is Lipschitzian
A2: now :: thesis: for x being VECTOR of X
for y being VECTOR of Y holds ||.(f . (x,y)).|| = (0 * ||.x.||) * ||.y.||
let x be VECTOR of X; :: thesis: for y being VECTOR of Y holds ||.(f . (x,y)).|| = (0 * ||.x.||) * ||.y.||
let y be VECTOR of Y; :: thesis: ||.(f . (x,y)).|| = (0 * ||.x.||) * ||.y.||
thus ||.(f . (x,y)).|| = ||.(0. Z).|| by A1
.= (0 * ||.x.||) * ||.y.|| ; :: thesis: verum
end;
take 0 ; :: according to LOPBAN_9:def 3 :: thesis: ( 0 <= 0 & ( for x being VECTOR of X
for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (0 * ||.x.||) * ||.y.|| ) )
thus ( 0 <= 0 & ( for x being VECTOR of X
for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (0 * ||.x.||) * ||.y.|| ) ) by A2; :: thesis: verum