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 real-valued & g is real-valued & 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 real-valued & g is real-valued & 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 real-valued & g is real-valued & 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 real-valued & g is real-valued & f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A )
assume that
A1:
f is real-valued
and
A2:
g is real-valued
and
A3:
f is_measurable_on A
and
A4:
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 A5:
for
p being
Rational holds
F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
by A3, A4, Th6;
consider G being
Function of
NAT ,
S such that A6:
rng F = rng G
by Th5, MESFUNC1:5;
A /\ (less_dom (f + g),(R_EAL r)) = union (rng G)
by A1, A2, A5, A6, Th3;
hence
A /\ (less_dom (f + g),(R_EAL r)) in S
;
:: thesis: verum
end;
hence
f + g is_measurable_on A
by MESFUNC1:def 17; :: thesis: verum