let X be non empty set ; 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; 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; 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; ( f is A -measurable & A c= dom f implies |.f.| is A -measurable )
assume A1:
( f is A -measurable & A c= dom f )
; |.f.| is A -measurable
for r being Real holds A /\ (less_dom (|.f.|,r)) in S
proof
let r be
Real;
A /\ (less_dom (|.f.|,r)) in S
reconsider r =
r as
R_eal by XXREAL_0:def 1;
for
x being
object st
x in less_dom (
|.f.|,
r) holds
x in (less_dom (f,r)) /\ (great_dom (f,(- r)))
proof
let x be
object ;
( x in less_dom (|.f.|,r) implies x in (less_dom (f,r)) /\ (great_dom (f,(- r))) )
assume A2:
x in less_dom (
|.f.|,
r)
;
x in (less_dom (f,r)) /\ (great_dom (f,(- r)))
then A3:
x in dom |.f.|
by MESFUNC1:def 11;
A4:
|.f.| . x < r
by A2, MESFUNC1:def 11;
reconsider x =
x as
Element of
X by A2;
A5:
x in dom f
by A3, MESFUNC1:def 10;
A6:
|.(f . x).| < r
by A3, A4, MESFUNC1:def 10;
then A7:
- r < f . x
by EXTREAL1:21;
A8:
f . x < r
by A6, EXTREAL1:21;
A9:
x in less_dom (
f,
r)
by A5, A8, MESFUNC1:def 11;
x in great_dom (
f,
(- r))
by A5, A7, MESFUNC1:def 13;
hence
x in (less_dom (f,r)) /\ (great_dom (f,(- r)))
by A9, XBOOLE_0:def 4;
verum
end;
then A10:
less_dom (
|.f.|,
r)
c= (less_dom (f,r)) /\ (great_dom (f,(- r)))
;
for
x being
object st
x in (less_dom (f,r)) /\ (great_dom (f,(- r))) holds
x in less_dom (
|.f.|,
r)
proof
let x be
object ;
( x in (less_dom (f,r)) /\ (great_dom (f,(- r))) implies x in less_dom (|.f.|,r) )
assume A11:
x in (less_dom (f,r)) /\ (great_dom (f,(- r)))
;
x in less_dom (|.f.|,r)
then A12:
x in less_dom (
f,
r)
by XBOOLE_0:def 4;
A13:
x in great_dom (
f,
(- r))
by A11, XBOOLE_0:def 4;
A14:
x in dom f
by A12, MESFUNC1:def 11;
A15:
f . x < r
by A12, MESFUNC1:def 11;
A16:
- r < f . x
by A13, MESFUNC1:def 13;
reconsider x =
x as
Element of
X by A11;
A17:
x in dom |.f.|
by A14, MESFUNC1:def 10;
|.(f . x).| < r
by A15, A16, EXTREAL1:22;
then
|.f.| . x < r
by A17, MESFUNC1:def 10;
hence
x in less_dom (
|.f.|,
r)
by A17, MESFUNC1:def 11;
verum
end;
then
(less_dom (f,r)) /\ (great_dom (f,(- r))) c= less_dom (
|.f.|,
r)
;
then A18:
less_dom (
|.f.|,
r)
= (less_dom (f,r)) /\ (great_dom (f,(- r)))
by A10;
(A /\ (great_dom (f,(- r)))) /\ (less_dom (f,r)) in S
by A1, MESFUNC1:32;
hence
A /\ (less_dom (|.f.|,r)) in S
by A18, XBOOLE_1:16;
verum
end;
hence
|.f.| is A -measurable
; verum