:: Linearity of {L}ebesgue Integral of Simple Valued Function
:: by Noboru Endou and Yasunari Shidama
::
:: Received September 14, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: MESFUNC4:1
theorem Th2: :: MESFUNC4:2
theorem Th3: :: MESFUNC4:3
theorem Th4: :: MESFUNC4:4
theorem :: MESFUNC4:5
for
X being non
empty set for
S being
SigmaField of
X for
M being
sigma_Measure of
S for
f,
g being
PartFunc of
X,
ExtREAL st
f is_simple_func_in S &
dom f <> {} & ( for
x being
set st
x in dom f holds
0. <= f . x ) &
g is_simple_func_in S &
dom g = dom f & ( for
x being
set st
x in dom g holds
0. <= g . x ) holds
(
f + g is_simple_func_in S &
dom (f + g) <> {} & ( for
x being
set st
x in dom (f + g) holds
0. <= (f + g) . x ) &
integral X,
S,
M,
(f + g) = (integral X,S,M,f) + (integral X,S,M,g) )
theorem :: MESFUNC4:6