let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
let f be PartFunc of X,ExtREAL; :: thesis: for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
let A, B, E be Element of S; :: thesis: ( E = dom f & f is E -measurable & f is nonpositive & A c= B implies Integral (M,(f | A)) >= Integral (M,(f | B)) )
assume that
A1: E = dom f and
A2: f is E -measurable and
A3: f is nonpositive and
A4: A c= B ; :: thesis: Integral (M,(f | A)) >= Integral (M,(f | B))
set g = - f;
E = dom (- f) by A1, MESFUNC1:def 7;
then A5: Integral (M,((- f) | A)) <= Integral (M,((- f) | B)) by A1, A2, A3, A4, MESFUNC5:93, MEASUR11:63;
reconsider E1 = E /\ A as Element of S ;
A6: dom (f | A) = E1 by A1, RELAT_1:61;
A7: E1 = (dom f) /\ E1 by A1, XBOOLE_1:17, XBOOLE_1:28;
A8: f is E1 -measurable by A2, XBOOLE_1:17, MESFUNC1:30;
A9: f | E1 = (f | E) | A by RELAT_1:71;
(- f) | A = - (f | A) by Th3;
then A10: Integral (M,((- f) | A)) = - (Integral (M,(f | A))) by A1, A6, A7, A8, A9, Th52, MESFUNC5:42;
reconsider E2 = E /\ B as Element of S ;
A11: dom (f | B) = E2 by A1, RELAT_1:61;
A12: E2 = (dom f) /\ E2 by A1, XBOOLE_1:17, XBOOLE_1:28;
A13: f is E2 -measurable by A2, XBOOLE_1:17, MESFUNC1:30;
A14: f | E2 = (f | E) | B by RELAT_1:71;
(- f) | B = - (f | B) by Th3;
then Integral (M,((- f) | B)) = - (Integral (M,(f | B))) by A1, A11, A12, A13, A14, Th52, MESFUNC5:42;
hence Integral (M,(f | A)) >= Integral (M,(f | B)) by A5, A10, XXREAL_3:38; :: thesis: verum