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 f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let f be PartFunc of X,ExtREAL ; :: thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let A be Element of S; :: thesis: ( f is_measurable_on A & A c= dom f implies |.f.| is_measurable_on A )
assume that
A1:
f is_measurable_on A
and
A2:
A c= dom f
; :: thesis: |.f.| is_measurable_on A
for r being real number holds A /\ (less_dom |.f.|,(R_EAL r)) in S
proof
let r be
real number ;
:: thesis: A /\ (less_dom |.f.|,(R_EAL r)) in S
reconsider r =
r as
Real by XREAL_0:def 1;
now A3:
less_dom |.f.|,
(R_EAL r) = (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r)))
proof
for
x being
set st
x in less_dom |.f.|,
(R_EAL r) holds
x in (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r)))
proof
let x be
set ;
:: thesis: ( x in less_dom |.f.|,(R_EAL r) implies x in (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r))) )
assume A4:
x in less_dom |.f.|,
(R_EAL r)
;
:: thesis: x in (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r)))
then A5:
(
x in dom |.f.| &
|.f.| . x < R_EAL r )
by MESFUNC1:def 12;
reconsider x =
x as
Element of
X by A4;
A6:
x in dom f
by A5, MESFUNC1:def 10;
|.(f . x).| < R_EAL r
by A5, MESFUNC1:def 10;
then A7:
(
- (R_EAL r) < f . x &
f . x < R_EAL r )
by EXTREAL2:58;
- (R_EAL r) = - r
by SUPINF_2:3;
then
(
x in less_dom f,
(R_EAL r) &
x in great_dom f,
(R_EAL (- r)) )
by A6, A7, MESFUNC1:def 12, MESFUNC1:def 14;
hence
x in (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r)))
by XBOOLE_0:def 4;
:: thesis: verum
end;
then A8:
less_dom |.f.|,
(R_EAL r) c= (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r)))
by TARSKI:def 3;
for
x being
set st
x in (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r))) holds
x in less_dom |.f.|,
(R_EAL r)
proof
let x be
set ;
:: thesis: ( x in (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r))) implies x in less_dom |.f.|,(R_EAL r) )
assume A9:
x in (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r)))
;
:: thesis: x in less_dom |.f.|,(R_EAL r)
then A10:
(
x in less_dom f,
(R_EAL r) &
x in great_dom f,
(R_EAL (- r)) )
by XBOOLE_0:def 4;
then A11:
(
x in dom f &
f . x < R_EAL r )
by MESFUNC1:def 12;
A12:
f . x < R_EAL r
by A10, MESFUNC1:def 12;
A13:
R_EAL (- r) < f . x
by A10, MESFUNC1:def 14;
reconsider x =
x as
Element of
X by A9;
A14:
x in dom |.f.|
by A11, MESFUNC1:def 10;
- (R_EAL r) = - r
by SUPINF_2:3;
then
|.(f . x).| < R_EAL r
by A12, A13, EXTREAL2:59;
then
|.f.| . x < R_EAL r
by A14, MESFUNC1:def 10;
hence
x in less_dom |.f.|,
(R_EAL r)
by A14, MESFUNC1:def 12;
:: thesis: verum
end;
then
(less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r))) c= less_dom |.f.|,
(R_EAL r)
by TARSKI:def 3;
hence
less_dom |.f.|,
(R_EAL r) = (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r)))
by A8, XBOOLE_0:def 10;
:: thesis: verum
end;
(A /\ (great_dom f,(R_EAL (- r)))) /\ (less_dom f,(R_EAL r)) in S
by A1, A2, MESFUNC1:36;
hence
A /\ (less_dom |.f.|,(R_EAL r)) in S
by A3, XBOOLE_1:16;
:: thesis: verum end;
hence
A /\ (less_dom |.f.|,(R_EAL r)) in S
;
:: thesis: verum
end;
hence
|.f.| is_measurable_on A
by MESFUNC1:def 17; :: thesis: verum