:: deftheorem Def12 defines Lp-Norm LPSPACE2:def 12 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real
for b₅ being Function of the carrier of (Pre-Lp-Space (M,k)),REAL holds
( b₅ = Lp-Norm (M,k) iff for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st
( f in x & ex r being Real st
( r = Integral (M,((abs f) to_power k)) & b₅ . x = r to_power (1 / k) ) ) );