let X be non empty set ; 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; 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; 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; ( 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
; f | B is A -measurable
A3:
R_EAL f is B -measurable
by A1;
now for r being Real holds A /\ (less_dom ((f | B),r)) in Slet r be
Real;
A /\ (less_dom ((f | B),r)) in Snow 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 ;
( 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;
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
;
verum end;
hence
f | B is A -measurable
by Th12; verum