:: deftheorem Def19 defines L-1-Norm LPSPACE1:def 19 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Function of the carrier of (Pre-L-Space M),REAL holds
( b₄ = L-1-Norm M iff for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b₄ . x = Integral (M,(abs f)) ) );