:: deftheorem Def11 defines BoundedLinearOperatorsNorm CLOPBAN1:def 11 :
for X, Y being ComplexNormSpace
for b₃ being Function of (BoundedLinearOperators (X,Y)),REAL holds
( b₃ = BoundedLinearOperatorsNorm (X,Y) iff for x being object st x in BoundedLinearOperators (X,Y) holds
b₃ . x = upper_bound (PreNorms (modetrans (x,X,Y))) );