environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, SEQ_1, XXREAL_0, SEQ_2, ORDINAL2, CARD_1, ARYTM_3, COMPLEX1, ARYTM_1, SETFAM_1, FINSUB_1, ZFMISC_1, TARSKI, RELAT_1, CARD_3, EQREL_1, FUNCT_7, FUNCOP_1, NAT_1, RPR_1, REAL_1, VALUED_0, XXREAL_1, PROB_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSUB_1, RELAT_1, FUNCT_1, XCMPLX_0, REAL_1, FUNCT_2, FUNCOP_1, FUNCT_7, ORDINAL1, CARD_3, NUMBERS, VALUED_0, XREAL_0, COMPLEX1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, SETFAM_1, XXREAL_0, XXREAL_1;
definitions FINSUB_1, TARSKI, MEMBERED, FUNCT_2, VALUED_0;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, ABSVALUE, SEQ_2, SETFAM_1, SUBSET_1, RELAT_1, RELSET_1, FINSUB_1, FUNCOP_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, XXREAL_1, FUNCT_7, NAT_1, ORDINAL1, XREAL_0;
schemes FUNCT_2, PARTFUN1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, XXREAL_1, RELAT_1, VALUED_0, RELSET_1;
constructors HIDDEN, SETFAM_1, FINSUB_1, XXREAL_1, COMPLEX1, REAL_1, SEQ_2, CARD_3, MEMBERED, FUNCT_7, RELSET_1, COMSEQ_2, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUBSET_1, CARD_3;
expansions TARSKI, FUNCT_2;
Lm1:
for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)
theorem Th27:
for
Omega,
p being
set for
Sigma being
SigmaField of
Omega ex
f being
Function st
(
dom f = Sigma & ( for
D being
Subset of
Omega st
D in Sigma holds
( (
p in D implies
f . D = 1 ) & ( not
p in D implies
f . D = 0 ) ) ) )
theorem Th28:
for
Omega,
p being
set for
Sigma being
SigmaField of
Omega ex
P being
Function of
Sigma,
REAL st
for
D being
Subset of
Omega st
D in Sigma holds
( (
p in D implies
P . D = 1 ) & ( not
p in D implies
P . D = 0 ) )
:: a field of subsets of given nonempty set Omega. ::