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