environ
vocabularies HIDDEN, FINSEQ_1, ARYTM_1, INTEGRA1, RELAT_1, ORDINAL2, FUNCT_1, CARD_1, FUNCT_3, SEQ_2, JORDAN3, RFINSEQ, INTEGRA2, FDIFF_1, ARYTM_3, SEQ_4, CLASSES1, VALUED_0, XBOOLE_0, NUMBERS, MEASURE7, REAL_1, SUBSET_1, XXREAL_2, XXREAL_0, NAT_1, TARSKI, ORDINAL4, COMPLEX1, CARD_3, XXREAL_1, PARTFUN1, SEQ_1, MEASURE5, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, FUNCT_2, XXREAL_2, SEQ_4, VALUED_0, PARTFUN1, MEASURE6, FINSEQ_1, RFUNCT_1, RVSUM_1, INTEGRA1, SEQ_1, COMSEQ_2, SEQ_2, FINSEQ_6, RCOMP_1, FDIFF_1, CLASSES1, RFINSEQ, MEASURE5, INTEGRA2;
definitions TARSKI;
theorems SEQ_4, SUBSET_1, PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1, RVSUM_1, SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, NAT_1, RFINSEQ, TARSKI, FINSEQ_5, FINSEQ_3, FINSEQ_4, FINSEQ_6, INTEGRA2, RELAT_1, XREAL_0, FUNCT_2, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, FINSOP_1, ORDINAL1, XXREAL_2, SEQM_3, CLASSES1, MEASURE5;
schemes FINSEQ_2, NAT_1, SEQ_1;
registrations XBOOLE_0, RELAT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, SEQM_3, INTEGRA1, INTEGRA2, VALUED_0, FUNCT_2, FINSET_1, XXREAL_2, CARD_1, SEQ_2, MEASURE5;
constructors HIDDEN, PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, FINSOP_1, RFUNCT_1, FDIFF_1, RFINSEQ, BINARITH, MEASURE6, FINSEQ_6, INTEGRA2, BINOP_2, XXREAL_2, NAT_D, RVSUM_1, CLASSES1, SEQ_4, RELSET_1, SEQ_2, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RVSUM_1;
expansions TARSKI;
Lm1:
for j being Element of NAT holds (j -' j) + 1 = 1
Lm2:
for n being Element of NAT st 1 <= n & n <= 2 & not n = 1 holds
n = 2
Lm3:
for A being non empty closed_interval Subset of REAL
for g being Function of A,REAL st g | A is bounded holds
upper_bound (rng g) >= lower_bound (rng g)
Lm4:
for A, B being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & B c= A holds
( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )
Lm5:
for j being Element of NAT
for A being non empty closed_interval Subset of REAL
for D1 being Division of A st j in dom D1 holds
vol (divset (D1,j)) <= delta D1
Lm6:
for x being Real
for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A
for j1 being Element of NAT st j1 = (len D1) - 1 & x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} holds
rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1)
Lm7:
for y being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds
ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
Lm8:
for A being non empty closed_interval Subset of REAL
for D1 being Division of A st vol A <> 0 & len D1 = 1 holds
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
Lm9:
for A being non empty closed_interval Subset of REAL
for D2 being Division of A st lower_bound A < D2 . 1 holds
<*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL
Lm10:
for A being non empty closed_interval Subset of REAL
for D1 being Division of A
for f being Function of A,REAL
for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
( ( for i being Element of NAT st i in Seg (len D1) holds
divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )
Lm11:
for A being non empty closed_interval Subset of REAL
for D2, MD2 being Division of A st MD2 = <*(lower_bound A)*> ^ D2 holds
vol (divset (MD2,1)) = 0
Lm12:
for A being non empty closed_interval Subset of REAL
for D1, MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
delta MD1 = delta D1
theorem Th15:
for
r being
Real for
i,
j being
Element of
NAT for
A being non
empty closed_interval Subset of
REAL for
D1,
D2 being
Division of
A st
i in dom D1 &
j in dom D1 &
i <= j &
D1 <= D2 &
r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds
ex
B being non
empty closed_interval Subset of
REAL ex
MD1,
MD2 being
Division of
B st
(
r = lower_bound B &
upper_bound B = MD2 . (len MD2) &
upper_bound B = MD1 . (len MD1) &
MD1 <= MD2 &
MD1 = mid (
D1,
i,
j) &
MD2 = mid (
D2,
(indx (D2,D1,i)),
(indx (D2,D1,j))) )