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