:: deftheorem defines is_LayerFunc NEURONS1:def 5 :
for X, Y being RealNormSpace
for F being Function of X,Y
for D, K being Real holds
( F is_LayerFunc D,K iff ( ( for x, y being Point of X holds ||.((F . x) - (F . y)).|| <= D * ||.(x - y).|| ) & ( for x being Point of X holds ||.(F . x).|| <= K ) ) );