:: deftheorem defines is_Lipschitzian_on DUALSP04:def 7 :
for X being RealUnitarySpace
for Y being set
for f being PartFunc of the carrier of X,REAL holds
( f is_Lipschitzian_on Y iff ( Y c= dom f & ex r being Real st
( 0 < r & ( for x1, x2 being Point of X st x1 in Y & x2 in Y holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) ) );