environ
vocabularies HIDDEN, DIST_2, DIST_1, FINSEQ_1, RELAT_1, FINSEQ_4, NAT_1, XXREAL_0, FUNCT_7, FUNCT_1, RPR_1, CARD_1, XBOOLE_0, CQC_SIM1, ARYTM_3, TARSKI, ZFMISC_1, SUBSET_1, NUMBERS, PROB_2, FINSET_1, UPROOTS, MATRPROB, MARGREL1, CARD_3, XBOOLEAN, VALUED_1, EQREL_1, PROB_1, SETFAM_1, FUNCT_2, ORDINAL2, ARYTM_1, FUNCT_3, RANDOM_1, SEQ_2, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, FUNCT_2, DOMAIN_1, FUNCT_3, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, CARD_3, KURATO_0, FRECHET, COMSEQ_2, XXREAL_0, XREAL_0, REAL_1, NAT_1, FINSEQ_1, VALUED_1, FINSEQ_2, XBOOLEAN, SEQ_2, MARGREL1, FINSEQ_4, RVSUM_1, RPR_1, PROB_1, PROB_2, BVFUNC_1, UPROOTS, MATRPROB, RANDOM_1, DIST_1;
definitions ;
theorems TARSKI, FINSEQ_2, CARD_1, FINSEQ_4, FUNCT_1, FINSEQ_1, XBOOLE_0, XBOOLE_1, PROB_2, RELAT_1, ZFMISC_1, FUNCT_2, XCMPLX_1, VALUED_1, FINSEQ_5, RVSUM_1, DIST_1, ORDINAL1, INTEGRA1, BVFUNC_1, MARGREL1, XBOOLEAN, PROB_1, CARD_2, FUNCT_3, RANDOM_1, XREAL_0, SETFAM_1;
schemes FUNCT_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, VALUED_0, FINSEQ_1, DIST_1, VALUED_1, MARGREL1, MATRPROB, XBOOLEAN, XCMPLX_0, ORDINAL1;
constructors HIDDEN, KURATO_0, FRECHET, COMSEQ_2, CARD_3, RELSET_1, DOMAIN_1, REAL_1, BINOP_2, FINSEQ_4, RVSUM_1, RPR_1, PROB_4, BVFUNC_1, UPROOTS, PROB_3, DIST_1, RANDOM_1, SEQ_2, MESFUNC5, SEQ_4, WELLORD2, NUMBERS;
requirements HIDDEN, REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
equalities SUBSET_1, RELAT_1, FINSEQ_1, RPR_1, DIST_1, XBOOLEAN, CARD_3;
expansions DIST_1;
Lm1:
for S being non empty finite set
for A being Element of distribution_family S holds not A is empty
Lm2:
for p, q being boolean-valued Function
for x being set st x in (dom p) /\ (dom q) holds
( (p 'or' q) . x = TRUE iff ( p . x = TRUE or q . x = TRUE ) )
Lm3:
for p, q being boolean-valued Function
for x being set st x in (dom p) /\ (dom q) holds
( (p '&' q) . x = TRUE iff ( p . x = TRUE & q . x = TRUE ) )
Lm4:
for p being boolean-valued Function
for x being set st x in dom p holds
( ('not' p) . x = TRUE iff p . x = FALSE )
Lm5:
for S being non empty finite set
for D being EqSampleSpaces of S ex EP being Probability of Trivial-SigmaField S st
for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
definition
let S be non
empty finite set ;
let D be
EqSampleSpaces of
S;
existence
ex b1 being Probability of Trivial-SigmaField S st
for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & b1 . x = Prob (ch,D) )
by Lm5;
uniqueness
for b1, b2 being Probability of Trivial-SigmaField S st ( for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & b1 . x = Prob (ch,D) ) ) & ( for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & b2 . x = Prob (ch,D) ) ) holds
b1 = b2
end;