environ
vocabularies HIDDEN, INTEGRA1, INTEGRA2, FINSEQ_1, NORMSP_1, SEQ_2, TARSKI, STRUCT_0, ORDINAL2, INTEGRA5, XBOOLE_0, SUBSET_1, NUMBERS, ARYTM_1, NAT_1, MEASURE7, CARD_3, RELAT_1, FUNCT_1, REAL_1, XXREAL_0, XXREAL_1, VALUED_1, PARTFUN1, RLVECT_1, FUNCT_3, INTEGR15, PRE_TOPC, ARYTM_3, CARD_1, SUPINF_2, SEQ_4, MEASURE5;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, FINSEQ_1, FINSEQ_2, SEQ_2, SEQ_4, RCOMP_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA5, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, BINOM;
definitions ;
theorems XBOOLE_1, INTEGRA1, INTEGRA2, INTEGRA4, RELSET_1, BINOM, XXREAL_0, RELAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, PARTFUN1, INTEGRA5, NORMSP_1, VFUNCT_1, RLVECT_1, RLVECT_2, FINSEQ_3, MEASURE5, ORDINAL1;
schemes FUNCT_2, FINSEQ_1;
registrations NUMBERS, XREAL_0, STRUCT_0, RELSET_1, INTEGRA1, FUNCT_2, XXREAL_0, ORDINAL1, FUNCT_1, MEASURE5, FINSEQ_1, MEMBERED;
constructors HIDDEN, REAL_1, SEQ_4, VFUNCT_1, RELSET_1, INTEGRA2, INTEGRA5, INTEGRA3, SEQ_2, BINOM, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, INTEGRA1;
expansions XBOOLE_0;
definition
let X be
RealNormSpace;
let A be non
empty closed_interval Subset of
REAL;
let f be
Function of
A, the
carrier of
X;
assume A1:
f is
integrable
;
existence
ex b1 being Point of X st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = b1 )
by A1;
uniqueness
for b1, b2 being Point of X st ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = b1 ) ) & ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = b2 ) ) holds
b1 = b2
end;
reconsider jj = 1 as Real ;
::
deftheorem Def9 defines
integral INTEGR18:def 9 :
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for a, b being Real holds
( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) & ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) );