:: deftheorem defines is_Lipschitzian_on NCFCONT1:def 18 :
for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS holds
( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st
( 0 < r & ( for x1, x2 being Point of CNS st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ) );