:: deftheorem defines Lp-Space LPSPACE2:def 13 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds Lp-Space (M,k) = NORMSTR(# the carrier of (Pre-Lp-Space (M,k)), the ZeroF of (Pre-Lp-Space (M,k)), the addF of (Pre-Lp-Space (M,k)), the Mult of (Pre-Lp-Space (M,k)),(Lp-Norm (M,k)) #);