let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is without-infty & g is without-infty & f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is without-infty & g is without-infty & f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let f, g be PartFunc of X,ExtREAL ; :: thesis: for A being Element of S st f is without-infty & g is without-infty & f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let A be Element of S; :: thesis: ( f is without-infty & g is without-infty & f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A )
assume that
A1:
( f is without-infty & g is without-infty )
and
A2:
( f is_measurable_on A & g is_measurable_on A )
; :: thesis: f + g is_measurable_on A
for r being real number holds A /\ (less_dom (f + g),(R_EAL r)) in S
proof
let r be
real number ;
:: thesis: A /\ (less_dom (f + g),(R_EAL r)) in S
reconsider r =
r as
Real by XREAL_0:def 1;
consider F being
Function of
RAT ,
S such that A3:
for
p being
Rational holds
F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
by A2, MESFUNC2:6;
A4:
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
by A1, A3, Th24;
ex
G being
Function of
NAT ,
S st
rng F = rng G
by MESFUNC1:5, MESFUNC2:5;
then
rng F is
N_Sub_set_fam of
X
by MEASURE1:52;
hence
A /\ (less_dom (f + g),(R_EAL r)) in S
by A4, MEASURE1:def 9;
:: thesis: verum
end;
hence
f + g is_measurable_on A
by MESFUNC1:def 17; :: thesis: verum