:: deftheorem Def8 defines Lipschitzian LOPBAN_9:def 3 :
for X, Y, Z being RealNormSpace
for IT being BilinearOperator of X,Y,Z holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K & ( for x being VECTOR of X
for y being VECTOR of Y holds ||.(IT . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) );