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