:: deftheorem defines PreNorms CLOPBAN1:def 10 :
for X, Y being ComplexNormSpace
for u being LinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;