environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, REAL_1, SEQ_1, PROB_1, RPR_1, CARD_1, ARYTM_3, RELAT_1, SEQ_2, FUNCT_1, ARYTM_1, ORDINAL2, XXREAL_0, COMPLEX1, EQREL_1, TARSKI, ZFMISC_1, NAT_1, CARD_3, VALUED_1, PROB_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, RELAT_1, REAL_1, FUNCT_1, FUNCT_2, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, PROB_1, NAT_1, XXREAL_0;
definitions PROB_1;
theorems FUNCT_1, FUNCT_2, SEQ_2, SUBSET_1, PROB_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, COMPLEX1, XREAL_1, ORDINAL1, VALUED_1, VALUED_0, RELAT_1;
schemes FUNCT_1, FUNCT_2, NAT_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, VALUED_0, PROB_1, NAT_1;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, PROB_1, XXREAL_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities PROB_1, SUBSET_1;
expansions PROB_1;
theorem Th1:
for
r,
r1,
r2,
r3 being
Real st
r <> 0 &
r1 <> 0 holds
(
r3 / r1 = r2 / r iff
r3 * r = r2 * r1 )
Lm1:
for Omega being set
for ASeq being SetSequence of Omega holds
( ASeq is non-descending iff Complement ASeq is non-ascending )
Lm2:
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )