begin
theorem Th1:
theorem Th2:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem MESFUNC6:def 1 :
canceled;
:: deftheorem MESFUNC6:def 2 :
canceled;
:: deftheorem MESFUNC6:def 3 :
canceled;
:: deftheorem MESFUNC6:def 4 :
canceled;
:: deftheorem MESFUNC6:def 5 :
canceled;
:: deftheorem Def6 defines is_measurable_on MESFUNC6:def 6 :
theorem Th12:
theorem Th13:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th20:
theorem Th21:
begin
theorem
theorem Th23:
theorem
theorem
theorem Th26:
theorem
theorem Th28:
theorem
begin
theorem Th30:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th43:
theorem Th44:
theorem
begin
theorem Th46:
theorem Th47:
theorem
begin
:: deftheorem Def7 defines is_simple_func_in MESFUNC6:def 7 :
theorem Th49:
theorem
theorem Th51:
theorem Th52:
theorem
theorem Th54:
theorem
theorem Th56:
theorem
theorem Th58:
theorem
theorem Th60:
theorem
theorem Th62:
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem Th70:
theorem Th71:
Lm1:
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 , st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th80:
theorem
begin
:: deftheorem defines Integral MESFUNC6:def 8 :
theorem Th82:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def9 defines is_integrable_on MESFUNC6:def 9 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Integral_on MESFUNC6:def 10 :
theorem
theorem