:: deftheorem defines a.e-eq-class_Lp LPSPACE2:def 6 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real holds a.e-eq-class_Lp (f,M,k) = { h where h is PartFunc of X,REAL : ( h in Lp_Functions (M,k) & f a.e.= h,M ) } ;