environ
vocabularies HIDDEN, NUMBERS, INTEGRA1, SUBSET_1, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1, MEASURE7, XBOOLE_0, XXREAL_2, XXREAL_0, SEQ_4, CARD_1, REAL_1, ARYTM_3, ARYTM_1, CARD_3, FINSEQ_2, INTEGRA2, SEQ_1, SEQ_2, ORDINAL2, COMPLEX1, XXREAL_1, FUNCT_3, REAL_NS1, STRUCT_0, PARTFUN1, VALUED_1, TARSKI, PRE_TOPC, INTEGRA5, REALSET1, INTEGR15, VALUED_2, MEASURE5, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0, COMPLEX1, XXREAL_2, NAT_1, FUNCT_1, FUNCT_2, STRUCT_0, REAL_1, RCOMP_1, VALUED_1, RELSET_1, PARTFUN1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, FINSEQ_1, FINSEQ_2, FINSEQOP, VALUED_2, RVSUM_1, PRE_TOPC, XXREAL_0, EUCLID, PDIFF_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA5, NORMSP_0, NORMSP_1, REAL_NS1;
definitions TARSKI;
theorems XBOOLE_0, XBOOLE_1, XREAL_0, INTEGRA1, INTEGRA2, INTEGRA4, XXREAL_2, XXREAL_0, RELAT_1, XCMPLX_1, PREPOWER, ORDINAL1, XREAL_1, RCOMP_1, SEQ_4, SEQ_2, FINSEQ_1, FINSEQ_2, RVSUM_1, FUNCT_1, FUNCT_2, PARTFUN1, REAL_NS1, INTEGRA5, PDIFF_1, INTEGRA6, VALUED_1, VALUED_2, RELSET_1, CARD_1, TARSKI;
schemes SEQ_1, FUNCT_2, FINSEQ_1;
registrations NUMBERS, XREAL_0, SEQ_2, INTEGRA1, FUNCT_2, NAT_1, MEMBERED, XXREAL_0, ORDINAL1, VALUED_0, VALUED_1, REAL_NS1, RELSET_1, EUCLID, VALUED_2, CARD_1, MEASURE5, FINSEQ_1;
constructors HIDDEN, REAL_1, FINSEQOP, MONOID_0, SEQ_4, PSCOMP_1, NAT_D, VFUNCT_1, PDIFF_1, BINOP_2, INTEGRA2, INTEGRA5, RELSET_1, SEQ_2, INTEGRA3, VALUED_2, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, EUCLID, INTEGRA1, INTEGRA5;
expansions XBOOLE_0, INTEGRA5;
Lm1:
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume (f,D)) . i <= F . i
Lm2:
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
Lm3:
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i )
Lm4:
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i
Lm5:
for p, q, r being Real_Sequence st p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) holds
( q is convergent & lim p = lim q & lim r = lim q )
Lm6:
for n, i being Element of NAT
for f being PartFunc of REAL,(REAL n)
for i being Element of NAT
for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
definition
let a,
b be
Real;
let n be
Element of
NAT ;
let f be
PartFunc of
REAL,
(REAL n);
existence
ex b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),a,b) ) )
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),a,b) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral (((proj (i,n)) * f),a,b) ) holds
b1 = b2
end;