:: deftheorem defines CosetSet LPSPACE2:def 7 :
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 CosetSet (M,k) = { (a.e-eq-class_Lp (f,M,k)) where f is PartFunc of X,REAL : f in Lp_Functions (M,k) } ;