:: deftheorem defines Lipschitzian BHSP_6:def 4 :

for X being RealUnitarySpace

for L being linear-Functional of X holds

( L is Lipschitzian iff ex K being Real st

( K > 0 & ( for x being Point of X holds |.(L . x).| <= K * ||.x.|| ) ) );

for X being RealUnitarySpace

for L being linear-Functional of X holds

( L is Lipschitzian iff ex K being Real st

( K > 0 & ( for x being Point of X holds |.(L . x).| <= K * ||.x.|| ) ) );