:: deftheorem Def11 defines Pre-Lp-Space LPSPACE2:def 11 :
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 strict RLSStruct holds
( b₅ = Pre-Lp-Space (M,k) iff ( the carrier of b₅ = CosetSet (M,k) & the addF of b₅ = addCoset (M,k) & 0. b₅ = zeroCoset (M,k) & the Mult of b₅ = lmultCoset (M,k) ) );