:: deftheorem Def8 defines Lipschitzian DUALSP01:def 9 :
for X being RealNormSpace
for IT being Functional of X holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds |.(IT . x).| <= K * ||.x.|| ) ) );