let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A, B being Element of S st f is B -measurable & A = (dom f) /\ B holds
f | B is A -measurable
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL
for A, B being Element of S st f is B -measurable & A = (dom f) /\ B holds
f | B is A -measurable
let f be PartFunc of X,REAL; :: thesis: for A, B being Element of S st f is B -measurable & A = (dom f) /\ B holds
f | B is A -measurable
let A, B be Element of S; :: thesis: ( f is B -measurable & A = (dom f) /\ B implies f | B is A -measurable )
assume that
A1: f is B -measurable and
A2: A = (dom f) /\ B ; :: thesis: f | B is A -measurable
A3: R_EAL f is B -measurable by A1;
now :: thesis: for r being Real holds A /\ (less_dom ((f | B),r)) in S
let r be Real; :: thesis: A /\ (less_dom ((f | B),r)) in S
now :: thesis: for x being object holds
( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) )
let x be object ; :: thesis: ( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) )
( x in dom (f | B) & (f | B) . x < r iff ( x in (dom f) /\ B & (f | B) . x < r ) ) by RELAT_1:61;
then A4: ( x in A & x in less_dom ((f | B),r) iff ( x in B & x in dom f & (f | B) . x < r ) ) by A2, MESFUNC1:def 11, XBOOLE_0:def 4;
( x in B & x in dom f implies ( f . x < r iff (f | B) . x < r ) ) by FUNCT_1:49;
then ( x in A /\ (less_dom ((f | B),r)) iff ( x in B & x in less_dom (f,r) ) ) by A4, MESFUNC1:def 11, XBOOLE_0:def 4;
hence ( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) ) by XBOOLE_0:def 4; :: thesis: verum
end;
then ( A /\ (less_dom ((f | B),r)) c= B /\ (less_dom (f,r)) & B /\ (less_dom (f,r)) c= A /\ (less_dom ((f | B),r)) ) ;
then A /\ (less_dom ((f | B),r)) = B /\ (less_dom (f,r)) ;
then A /\ (less_dom ((f | B),r)) in S by A3, MESFUNC1:def 16;
hence A /\ (less_dom ((f | B),r)) in S ; :: thesis: verum
end;
hence f | B is A -measurable by Th12; :: thesis: verum