let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral (M,(f | E)) <= Integral (M,(g | E))
let S be SigmaField of X; for M being sigma_Measure of S
for E being Element of S
for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral (M,(f | E)) <= Integral (M,(g | E))
let M be sigma_Measure of S; for E being Element of S
for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral (M,(f | E)) <= Integral (M,(g | E))
let E be Element of S; for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral (M,(f | E)) <= Integral (M,(g | E))
let f, g be PartFunc of X,ExtREAL; ( E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) implies Integral (M,(f | E)) <= Integral (M,(g | E)) )
assume that
A1:
E c= dom f
and
A2:
E c= dom g
and
A3:
f is E -measurable
and
A4:
g is E -measurable
and
A5:
f is nonnegative
and
A6:
for x being Element of X st x in E holds
f . x <= g . x
; Integral (M,(f | E)) <= Integral (M,(g | E))
set F2 = g | E;
A7:
E = dom (f | E)
by A1, RELAT_1:62;
set F1 = f | E;
A8:
f | E is nonnegative
by A5, MESFUNC5:15;
A9:
E = dom (g | E)
by A2, RELAT_1:62;
A10:
for x being Element of X st x in dom (f | E) holds
(f | E) . x <= (g | E) . x
for x being object st x in dom (g | E) holds
0 <= (g | E) . x
then A14:
g | E is nonnegative
by SUPINF_2:52;
A15:
(dom g) /\ E = E
by A2, XBOOLE_1:28;
then A16:
g | E is E -measurable
by A4, MESFUNC5:42;
A17:
(dom f) /\ E = E
by A1, XBOOLE_1:28;
then
f | E is E -measurable
by A3, MESFUNC5:42;
then
integral+ (M,(f | E)) <= integral+ (M,(g | E))
by A8, A7, A9, A10, A14, A16, MESFUNC5:85;
then
Integral (M,(f | E)) <= integral+ (M,(g | E))
by A3, A8, A7, A17, MESFUNC5:42, MESFUNC5:88;
hence
Integral (M,(f | E)) <= Integral (M,(g | E))
by A4, A9, A14, A15, MESFUNC5:42, MESFUNC5:88; verum