let X be non empty set ; for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is () & g is () & f is A -measurable & g is A -measurable holds
f + g is A -measurable
let S be SigmaField of X; for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is () & g is () & f is A -measurable & g is A -measurable holds
f + g is A -measurable
let f, g be PartFunc of X,ExtREAL; for A being Element of S st f is () & g is () & f is A -measurable & g is A -measurable holds
f + g is A -measurable
let A be Element of S; ( f is () & g is () & f is A -measurable & g is A -measurable implies f + g is A -measurable )
assume that
A1:
f is ()
and
A2:
g is ()
and
A3:
f is A -measurable
and
A4:
g is A -measurable
; f + g is A -measurable
for r being Real holds A /\ (less_dom ((f + g),r)) in S
proof
let r be
Real;
A /\ (less_dom ((f + g),r)) in S
consider F being
Function of
RAT,
S such that A5:
for
p being
Rational holds
F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
by A3, A4, MESFUNC2:6;
ex
G being
sequence of
S st
rng F = rng G
by MESFUNC1:5, MESFUNC2:5;
then A6:
rng F is
N_Sub_set_fam of
X
by MEASURE1:23;
A /\ (less_dom ((f + g),r)) = union (rng F)
by A1, A2, A5, Th18;
hence
A /\ (less_dom ((f + g),r)) in S
by A6, MEASURE1:def 5;
verum
end;
hence
f + g is A -measurable
by MESFUNC1:def 16; verum