environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, INTEGRA1, XBOOLE_0, MEASURE7, CARD_1, FINSEQ_1, RELAT_1, XXREAL_0, FUNCT_1, SEQ_4, ARYTM_3, ARYTM_1, FUNCT_3, TARSKI, PARTFUN1, CARD_3, VALUED_1, XXREAL_2, XXREAL_1, INTEGRA2, SEQ_2, ORDINAL2, FINSET_1, NAT_1, FINSEQ_2, VALUED_0, FDIFF_1, COMPLEX1, INT_1, ZFMISC_1, RFUNCT_3, SEQ_1, ORDINAL4, SQUARE_1, INTEGRA4, MEASURE5, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, INT_1, XXREAL_2, VALUED_0, ZFMISC_1, FUNCT_1, RELSET_1, FINSET_1, FUNCT_2, FINSEQ_1, VALUED_1, SEQ_1, RFUNCT_1, FINSEQ_2, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, FDIFF_1, SQUARE_1, RVSUM_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, RFUNCT_3, PARTFUN1, XXREAL_0;
definitions XXREAL_2;
theorems SEQ_4, SUBSET_1, PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1, RVSUM_1, SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, NAT_1, TARSKI, FINSEQ_3, INTEGRA2, INTEGRA3, SEQM_3, PARTFUN2, NAT_2, INT_1, FINSEQ_2, RFUNCT_3, RELAT_1, XREAL_0, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, FINSOP_1, FUNCOP_1, VALUED_1, XXREAL_2, VALUED_0, ORDINAL1, RELSET_1, CARD_1;
schemes FINSEQ_2, FUNCT_2;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, INTEGRA1, VALUED_0, VALUED_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, SEQM_3, MEASURE5, SQUARE_1;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, FINSOP_1, PARTFUN2, FDIFF_1, ZFMISC_1, RFUNCT_3, INTEGRA2, XXREAL_2, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, INTEGRA3, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SQUARE_1, RVSUM_1, FINSEQ_2, VALUED_1;
expansions XXREAL_2;
Lm1:
0 in REAL
by XREAL_0:def 1;
Lm2:
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )
Lm3:
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is lower_integrable & lower_integral f = 0 )
Lm4:
for A being non empty closed_interval Subset of REAL
for n being Nat st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Nat st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
Lm5:
for A being non empty closed_interval Subset of REAL st vol A > 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
Lm6:
for A being non empty closed_interval Subset of REAL st vol A = 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )