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 A c= dom f holds
( f is A -measurable iff ( max+ f is A -measurable & max- 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 A c= dom f holds
( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st A c= dom f holds
( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )
let A be Element of S; :: thesis: ( A c= dom f implies ( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) ) )
assume A1: A c= dom f ; :: thesis: ( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )
hence ( f is A -measurable implies ( max+ f is A -measurable & max- f is A -measurable ) ) by MESFUNC2:25, MESFUNC2:26; :: thesis: ( max+ f is A -measurable & max- f is A -measurable implies f is A -measurable )
assume A2: ( max+ f is A -measurable & max- f is A -measurable ) ; :: thesis: f is A -measurable
A3: dom (max- f) = dom f by MESFUNC2:def 3;
now :: thesis: for r being Real holds A /\ (less_dom (f,r)) in S
let r be Real; :: thesis: A /\ (less_dom (f,b1)) in S
per cases ( r > 0 or r <= 0 ) ;
suppose r > 0 ; :: thesis: A /\ (less_dom (f,b1)) in S
then less_dom (f,r) = less_dom ((max+ f),r) by Lm1;
hence A /\ (less_dom (f,r)) in S by A2, MESFUNC1:def 16; :: thesis: verum
end;
suppose r <= 0 ; :: thesis: A /\ (less_dom (f,b1)) in S
then less_dom (f,r) = great_dom ((max- f),(- r)) by Lm1;
hence A /\ (less_dom (f,r)) in S by A1, A2, A3, MESFUNC1:29; :: thesis: verum
end;
end;
end;
hence f is A -measurable by MESFUNC1:def 16; :: thesis: verum