:: deftheorem defines is_measurable_on MESFUNC1:def 15 :
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S holds
( f is_measurable_on A iff for r being Real holds A /\ (less_dom (f,r)) in S );