let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st f is A -measurable & A c= dom f holds
- f is A -measurable
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st f is A -measurable & A c= dom f holds
- f is A -measurable
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is A -measurable & A c= dom f holds
- f is A -measurable
let A be Element of S; :: thesis: ( f is A -measurable & A c= dom f implies - f is A -measurable )
assume that
A1: f is A -measurable and
A2: A c= dom f ; :: thesis: - f is A -measurable
- f = (- 1) (#) f by MESFUNC2:9;
hence - f is A -measurable by A1, A2, MESFUNC1:37; :: thesis: verum