begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
canceled;
theorem Th6:
theorem Th7:
:: deftheorem Def1 defines On MEASURE7:def 1 :
for S being non empty set
for H being Function of S,ExtREAL
for b3 being Function of NAT,ExtREAL holds
( b3 = On H iff for n being Element of NAT holds
( ( n in S implies b3 . n = H . n ) & ( not n in S implies b3 . n = 0. ) ) );
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
REAL in bool REAL
by ZFMISC_1:def 1;
then reconsider G0 = NAT --> REAL as Function of NAT,(bool REAL) by FUNCOP_1:57;
Lm1:
rng G0 = {REAL}
by FUNCOP_1:14;
then Lm2:
REAL c= union (rng G0)
by ZFMISC_1:31;
Lm3:
for n being Element of NAT holds G0 . n is Interval
:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :
for A being Subset of REAL
for b2 being Function of NAT,(bool REAL) holds
( b2 is Interval_Covering of A iff ( A c= union (rng b2) & ( for n being Element of NAT holds b2 . n is Interval ) ) );
:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :
for F being Function of NAT,(bool REAL)
for b2 being Function of NAT,(Funcs (NAT,(bool REAL))) holds
( b2 is Interval_Covering of F iff for n being Element of NAT holds b2 . n is Interval_Covering of F . n );
:: deftheorem Def4 defines vol MEASURE7:def 4 :
for A being Subset of REAL
for F being Interval_Covering of A
for b3 being Function of NAT,ExtREAL holds
( b3 = F vol iff for n being Element of NAT holds b3 . n = diameter (F . n) );
theorem Th13:
:: deftheorem defines vol MEASURE7:def 5 :
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for b3 being Function of NAT,(Funcs (NAT,ExtREAL)) holds
( b3 = G vol iff for n being Element of NAT holds b3 . n = (G . n) vol );
:: deftheorem defines vol MEASURE7:def 6 :
for A being Subset of REAL
for F being Interval_Covering of A holds vol F = SUM (F vol);
:: deftheorem Def7 defines vol MEASURE7:def 7 :
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for b3 being Function of NAT,ExtREAL holds
( b3 = vol G iff for n being Element of NAT holds b3 . n = vol (G . n) );
theorem Th14:
:: deftheorem Def8 defines Svc MEASURE7:def 8 :
for A being Subset of REAL
for b2 being Subset of ExtREAL holds
( b2 = Svc A iff for x being R_eal holds
( x in b2 iff ex F being Interval_Covering of A st x = vol F ) );
:: deftheorem defines COMPLEX MEASURE7:def 9 :
for A being Subset of REAL holds COMPLEX A = inf (Svc A);
:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :
for b1 being Function of (bool REAL),ExtREAL holds
( b1 = OS_Meas iff for A being Subset of REAL holds b1 . A = inf (Svc A) );
:: deftheorem MEASURE7:def 11 :
canceled;
:: deftheorem MEASURE7:def 12 :
canceled;
:: deftheorem Def13 defines On MEASURE7:def 13 :
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for H being Function of NAT,[:NAT,NAT:] st rng H = [:NAT,NAT:] holds
for b4 being Interval_Covering of union (rng F) holds
( b4 = On (G,H) iff for n being Element of NAT holds b4 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) );
reconsider D = NAT --> ({} REAL) as Function of NAT,(bool REAL) ;
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem defines Lmi_sigmaFIELD MEASURE7:def 14 :
Lmi_sigmaFIELD = sigma_Field OS_Meas;
:: deftheorem defines L_mi MEASURE7:def 15 :
L_mi = sigma_Meas OS_Meas;