### The Mizar article:

### Introduction to Probability

**by****Jan Popiolek**

- Received June 13, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: RPR_1
- [ MML identifier index ]

environ vocabulary FINSEQ_1, FINSET_1, BOOLE, RELAT_1, PROB_1, SUBSET_1, CARD_1, ARYTM_3, ARYTM_1, RPR_1, REALSET1; notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, FUNCT_1, DOMAIN_1, REAL_1, FINSEQ_1, FINSET_1, CARD_1, REALSET1; constructors DOMAIN_1, REAL_1, NAT_1, REALSET1, XREAL_0, MEMBERED, XBOOLE_0; clusters FINSET_1, RELSET_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions XBOOLE_0; theorems AXIOMS, TARSKI, SUBSET_1, ZFMISC_1, FINSEQ_1, REAL_1, CARD_1, CARD_2, SQUARE_1, PROB_1, REALSET1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; begin reserve E for non empty set; reserve a for Element of E; reserve A, B for Subset of E; reserve Y for set; reserve p for FinSequence; definition let E be non empty set; cluster non empty trivial Subset of E; existence proof consider x being set such that A1: x in E by XBOOLE_0:def 1; take {x}; thus thesis by A1,REALSET1:def 12,ZFMISC_1:37; end; end; definition let E; mode El_ev of E is non empty trivial Subset of E; end; theorem Th1: for e being non empty Subset of E holds e is El_ev of E iff for Y holds (Y c= e iff Y = {} or Y = e) proof let e be non empty Subset of E; thus e is El_ev of E implies for Y holds (Y c= e iff Y = {} or Y = e) proof assume e is El_ev of E; then consider x being set such that A1: e = {x} by REALSET1:def 12; let Y; thus Y c= e iff Y = {} or Y = e by A1,ZFMISC_1:39; end; assume A2: for Y holds Y c= e iff Y = {} or Y = e; consider x being set such that A3:x in e by XBOOLE_0:def 1; e is trivial proof {x} c= e by A3,ZFMISC_1:37; then {x} = e by A2; hence thesis by REALSET1:def 12; end; hence e is El_ev of E; end; definition let E; cluster -> finite El_ev of E; coherence proof let e be El_ev of E; per cases by REALSET1:def 12; suppose e is empty; then reconsider T = e as empty set; T is finite; hence thesis; suppose ex x being set st e = {x}; hence thesis; end; end; reserve e, e1, e2 for El_ev of E; canceled 3; theorem e = A \/ B & A <> B implies A = {} & B = e or A = e & B = {} proof assume that A1: e = A \/ B and A2: A <> B; A c= e & B c= e by A1,XBOOLE_1:7; then ( A = {} or A = e ) & ( B = {} or B = e ) by Th1; hence thesis by A2; end; theorem e = A \/ B implies A = e & B = e or A = e & B = {} or A = {} & B = e proof assume A1: e = A \/ B; then A c= e & B c= e by XBOOLE_1:7; then A = {} & B = e or A = e & B = {} or A = e & B = e or A = {} & B = {} by Th1; hence thesis by A1; end; theorem Th7: {a} is El_ev of E proof set e = {a}; e c= E & e <> {} & ( Y c= e iff Y = {} or Y = e ) by ZFMISC_1:39; hence thesis by Th1; end; canceled 2; theorem e1 c= e2 implies e1 = e2 by Th1; theorem Th11: ex a st a in E & e = {a} proof consider x being Element of e; A1:{x} c= e; reconsider x as Element of E; x in E & {x} = e by A1,Th1; hence thesis; end; theorem ex e st e is El_ev of E proof consider a being Element of E; {a} is El_ev of E by Th7; hence thesis; end; canceled; theorem ex p st p is FinSequence of E & rng p = e & len p = 1 proof consider a such that A1: a in E & e = {a} by Th11; reconsider p = <*a*> as FinSequence; A2: rng p = {a} by FINSEQ_1:56; len p = 1 by FINSEQ_1:56; hence thesis by A1,A2; end; definition let E be set; mode Event of E is Subset of E; end; canceled 7; theorem for E being non empty set, e being El_ev of E, A being Event of E holds e misses A or e /\ A = e proof let E be non empty set, e be El_ev of E, A be Event of E; A1: e /\ E = e by XBOOLE_1:28; A \/ A` = [#] E by SUBSET_1:25; then A \/ A` = E by SUBSET_1:def 4; then e = e /\ A \/ e /\ A` by A1,XBOOLE_1:23; then e /\ A c= e by XBOOLE_1:7; then e /\ A = {} or e /\ A = e by Th1; hence thesis by XBOOLE_0:def 7; end; canceled 2; theorem for E being non empty set, A being Event of E st A <> {} ex e being El_ev of E st e c= A proof let E be non empty set, A be Event of E; assume A1: A <> {}; consider x being Element of A; reconsider x as Element of E by A1,TARSKI:def 3; A2: {x} is El_ev of E by Th7; {x} c= A by A1,ZFMISC_1:37; hence thesis by A2; end; theorem for E being non empty set, e being El_ev of E, A being Event of E st e c= A \/ A` holds e c= A or e c= A` proof let E be non empty set, e be El_ev of E, A be Event of E; assume A1: e c= A \/ A`; ex a being Element of E st a in E & e = {a} by Th11; then consider a being Element of E such that A2: e = {a}; a in A \/ A` by A1,A2,ZFMISC_1:37; then a in A or a in A` by XBOOLE_0:def 2; hence thesis by A2,ZFMISC_1:37; end; theorem e1 = e2 or e1 misses e2 proof e1 /\ e2 c= e1 by XBOOLE_1:17; then e1 /\ e2 = {} or e1 /\ e2 = e1 by Th1; then e1 c= e2 or e1 /\ e2 = {} by XBOOLE_1:17; hence thesis by Th1,XBOOLE_0:def 7; end; canceled 6; theorem Th34: A /\ B misses A /\ B` proof A /\ B misses A \ B by XBOOLE_1:89; hence thesis by SUBSET_1:32; end; Lm1: for E being finite non empty set holds 0 < card E proof let E be finite non empty set; consider x being Element of E; card {x} <= card E by CARD_1:80; then 1 <= card E by CARD_1:79; hence thesis by AXIOMS:22; end; Lm2: card e = 1 proof ex a st a in E & {a} = e by Th11; hence thesis by CARD_1:79; end; definition let E be finite non empty set; let A be Event of E; canceled 3; func prob(A) -> Real equals :Def4: card A / card E; coherence; end; canceled 3; theorem for E being finite non empty set, e being El_ev of E holds prob(e) = 1 / card E proof let E be finite non empty set, e be El_ev of E; prob(e) = card e / card E by Def4; hence thesis by Lm2; end; theorem Th39: for E being finite non empty set holds prob([#] E) = 1 proof let E be finite non empty set; reconsider EE = [#] E as Subset of E; prob([#] E) = card EE / card E by Def4; then A1: prob([#] E) = card E / card E by SUBSET_1:def 4; card E <> 0 by Lm1; hence thesis by A1,XCMPLX_1:60; end; theorem Th40: for E being finite non empty set holds prob({} E) = 0 proof let E be finite non empty set; card {} / card E = 0 by CARD_1:78; hence thesis by Def4; end; theorem Th41: for E being finite non empty set, A,B being Event of E st A misses B holds prob(A /\ B) = 0 proof let E be finite non empty set, A,B be Event of E; assume A misses B; then A /\ B = {} E by XBOOLE_0:def 7; hence thesis by Th40; end; theorem for E being finite non empty set, A being Event of E holds prob(A) <= 1 proof let E be finite non empty set, A be Event of E; A1: prob(A) = card A / card E by Def4; reconsider EE = [#] E as Subset of E; prob [#] E = card EE / card E by Def4; then A2: prob([#] E) = card E / card E by SUBSET_1:def 4; A3: card A <= card E by CARD_1:80; 0 < card E by Lm1; then 0 <= (card E)" by REAL_1:72; then card A * (card E)" <= card E * (card E)" by A3,AXIOMS:25; then card A / card E <= card E * (card E)" by XCMPLX_0:def 9; then prob(A) <= card E / card E by A1,XCMPLX_0:def 9; hence thesis by A2,Th39; end; theorem Th43: for E being finite non empty set, A being Event of E holds 0 <= prob(A) proof let E be finite non empty set, A be Event of E; A1: prob(A) = card A / card E by Def4; 0 < card E by Lm1; then A2: 0 <= (card E)" by REAL_1:72; {} c= A by XBOOLE_1:2; then 0 <= card A by CARD_1:78,80; then 0 * (card E)" <= card A * (card E)" by A2,AXIOMS:25; hence thesis by A1,XCMPLX_0:def 9; end; theorem Th44: for E being finite non empty set, A,B being Event of E st A c= B holds prob(A) <= prob(B) proof let E be finite non empty set, A,B be Event of E; assume A c= B; then A1: card A <= card B by CARD_1:80; 0 < card E by Lm1; then 0 <= (card E)" by REAL_1:72; then card A * (card E)" <= card B * (card E)" by A1,AXIOMS:25; then card A / card E <= card B * (card E)" by XCMPLX_0:def 9; then card A / card E <= card B / card E by XCMPLX_0:def 9; then prob(A) <= card B / card E by Def4; hence thesis by Def4; end; canceled; theorem Th46: for E being finite non empty set, A,B being Event of E holds prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B) proof let E be finite non empty set, A,B be Event of E; card (( A \/ B ) qua Event of E) = card A + card B - card ( A /\ B ) by CARD_2:64; then A1: card ( A \/ B ) = card A + ( card B - card ( A /\ B )) by XCMPLX_1:29; set q = ( card E )"; set p = card E; card ( A \/ B ) * q = card A * q + ( card B - card ( A /\ B )) * q by A1,XCMPLX_1:8; then card ( A \/ B ) * q = card A * q + ( card B * q - card ( A /\ B ) * q ) by XCMPLX_1:40; then card ( A \/ B ) * q = card A * q + card B * q - card ( A /\ B ) * q by XCMPLX_1:29; then card ( A \/ B ) / p = card A * q + card B * q - card ( A /\ B ) * q by XCMPLX_0:def 9; then card ( A \/ B ) / p = card A / p + card B * q - card ( A /\ B ) * q by XCMPLX_0:def 9; then card ( A \/ B ) / p = card A / p + card B / p - card ( A /\ B ) * q by XCMPLX_0:def 9; then card ( A \/ B ) / p = card A / p + card B / p - card ( A /\ B ) / p by XCMPLX_0:def 9; then prob(A \/ B) = card A / p + card B / p - card ( A /\ B ) / p by Def4; then prob(A \/ B) = prob(A) + card B / p - card ( A /\ B ) / p by Def4; then prob(A \/ B) = prob(A) + prob(B) - card ( A /\ B ) / p by Def4; hence thesis by Def4; end; theorem Th47: for E being finite non empty set, A,B being Event of E st A misses B holds prob(A \/ B) = prob(A) + prob(B) proof let E be finite non empty set, A,B be Event of E; assume A misses B; then prob(A /\ B) = 0 by Th41; then prob(A \/ B) = prob(A) + prob(B) - 0 by Th46; hence thesis; end; theorem Th48: for E being finite non empty set, A being Event of E holds prob(A) = 1 - prob(A`) & prob(A`) = 1 - prob(A) proof let E be finite non empty set, A be Event of E; A misses A` by SUBSET_1:44; then prob(A \/ A`) = prob(A) + prob(A`) by Th47; then prob( [#] E ) = prob(A) + prob(A`) by SUBSET_1:25; then 1 = prob(A) + prob(A`) by Th39; hence thesis by XCMPLX_1:26; end; theorem Th49: for E being finite non empty set, A,B being Event of E holds prob(A \ B) = prob(A) - prob(A /\ B) proof let E be finite non empty set, A,B be Event of E; A1: prob(A) = prob((A \ B) \/ (A /\ B)) by XBOOLE_1:51; A \ B misses A /\ B by XBOOLE_1:89; then prob(A) = prob(A \ B) + prob(A /\ B) by A1,Th47; hence thesis by XCMPLX_1:26; end; theorem Th50: for E being finite non empty set, A,B being Event of E st B c= A holds prob(A \ B) = prob(A) - prob(B) proof let E be finite non empty set, A,B be Event of E; assume B c= A; then prob(A /\ B) = prob(B) by XBOOLE_1:28; hence thesis by Th49; end; theorem for E being finite non empty set, A,B being Event of E holds prob(A \/ B) <= prob(A) + prob(B) proof let E be finite non empty set, A,B be Event of E; A1: prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B) by Th46; 0 <= prob(A /\ B) by Th43; hence thesis by A1,PROB_1:2; end; canceled; theorem Th53: for E being finite non empty set, A,B being Event of E holds prob(A) = prob(A /\ B) + prob(A /\ B`) proof let E be finite non empty set, A,B be Event of E; A /\ B misses A /\ B` by Th34; then A1: prob((A /\ B) \/ (A /\ B`)) = prob(A /\ B) + prob(A /\ B`) by Th47; A = A /\ ( A \/ [#] E ) by XBOOLE_1:21; then A = A /\ [#] E by SUBSET_1:28; then A = A /\ ( B \/ B`) by SUBSET_1:25; hence thesis by A1,XBOOLE_1:23; end; theorem for E being finite non empty set, A,B being Event of E holds prob(A) = prob(A \/ B) - prob(B \ A) proof let E be finite non empty set, A,B be Event of E; A1: A misses ( B \ A ) by XBOOLE_1:79; prob(A \/ (B \ A)) = prob(A \/ B) by XBOOLE_1:39; then prob(A \/ B) = prob(A) + prob(B \ A) by A1,Th47; hence thesis by XCMPLX_1:26; end; theorem for E being finite non empty set, A,B being Event of E holds prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) proof let E be finite non empty set, A,B be Event of E; prob(A) = prob(A /\ B) + prob(A /\ B`) by Th53; then A1: prob(A /\ B) = prob(A) - prob(B` /\ A) by XCMPLX_1:26; prob(B) = prob(A /\ B) + prob(B /\ A`) by Th53; then prob(A) - prob(B` /\ A) = prob(B) - prob(A` /\ B) by A1,XCMPLX_1:26; then prob(A) - ( prob(B` /\ A) - prob(B` /\ A) ) = prob(B) - prob(A` /\ B) + prob(B` /\ A) by XCMPLX_1:37; then prob(A) - 0 = prob(B) - prob(A` /\ B) + prob(B` /\ A) by XCMPLX_1:14; then prob(A) = prob(B) + -prob(A` /\ B) + prob(B` /\ A) by XCMPLX_0:def 8; then prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) + -prob(A` /\ B) + prob(A` /\ B) by XCMPLX_1:1; then prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) - prob(A` /\ B) + prob(A` /\ B) by XCMPLX_0:def 8; then prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) - ( prob(A` /\ B) - prob(A` /\ B) ) by XCMPLX_1:37; then prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) - 0 by XCMPLX_1:14; hence thesis; end; theorem Th56: for E being finite non empty set, A,B,C being Event of E holds prob(A \/ B \/ C) = ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) proof let E be finite non empty set, A,B,C be Event of E; prob(A \/ B \/ C) = prob(A \/ B) + prob(C) - prob((A \/ B) /\ C) by Th46 .= ( ( prob(A) + prob(B) ) - prob(A /\ B) ) + prob(C) - prob((A \/ B) /\ C) by Th46 .= ( ( prob(A) + prob(B) ) + -prob(A /\ B) ) + prob(C) - prob((A \/ B) /\ C) by XCMPLX_0:def 8 .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - prob((A \/ B) /\ C) by XCMPLX_1:1 .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - prob((A /\ C) \/ (B /\ C)) by XBOOLE_1:23 .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - ( prob(A /\ C) + prob(B /\ C) - prob((A /\ C) /\ (B /\ C)) ) by Th46 .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - ( prob(A /\ C) + prob(B /\ C) - prob(A /\ ( C /\ (C /\ B)) )) by XBOOLE_1:16 .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - ( prob(A /\ C) + prob(B /\ C) - prob(A /\ (( C /\ C ) /\ B) )) by XBOOLE_1: 16 .= (( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B)) - ( prob(A /\ C) + prob(B /\ C) - prob(A /\ B /\ C) ) by XBOOLE_1:16 .= (( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B)) - ( prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) by XCMPLX_1:37 .= ( prob(A) + prob(B) + prob(C) ) + ( -(1 * prob(A /\ B)) - ( prob(A /\ C) + prob(B /\ C) )) + prob(A /\ B /\ C) by XCMPLX_1:29 .= ( prob(A) + prob(B) + prob(C) ) + ( (-1) * prob(A /\ B) - ( 1 * ( prob(A /\ C) + prob(B /\ C) ))) + prob(A /\ B /\ C) by XCMPLX_1:175 .= ( prob(A) + prob(B) + prob(C) ) + ( (-1) * prob(A /\ B) + -(1*( prob(A /\ C) + prob(B /\ C) ))) + prob(A /\ B /\ C) by XCMPLX_0:def 8 .= ( prob(A) + prob(B) + prob(C) ) + ( (-1) * prob(A /\ B) + (-1) * ( prob(A /\ C) + prob(B /\ C) )) + prob(A /\ B /\ C) by XCMPLX_1:175 .= ( prob(A) + prob(B) + prob(C) ) + (-1) * ( prob(A /\ B) + ( prob(A /\ C) + prob(B /\ C) )) + prob(A /\ B /\ C) by XCMPLX_1:8 .= ( prob(A) + prob(B) + prob(C) ) + -( 1 * ( prob(A /\ B) + ( prob(A /\ C) + prob(B /\ C) ))) + prob(A /\ B /\ C) by XCMPLX_1:175 .= ( prob(A) + prob(B) + prob(C) ) + -( prob(A /\ B) + prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) by XCMPLX_1:1; hence thesis by XCMPLX_0:def 8; end; theorem for E being finite non empty set, A,B,C being Event of E st A misses B & A misses C & B misses C holds prob(A \/ B \/ C) = prob(A) + prob(B) + prob(C) proof let E be finite non empty set, A,B,C be Event of E; assume that A1: A misses B and A2: A misses C and A3: B misses C; A misses (B /\ C) by A1,XBOOLE_1:74; then A4: prob(A /\ (B /\ C)) = 0 by Th41; prob(A \/ B \/ C) = ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) by Th56 .= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) + prob(B /\ C) ) + 0 by A4,XBOOLE_1:16 .= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) + 0 ) by A3,Th41 .= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + 0 ) by A2,Th41 .= ( prob(A) + prob(B) + prob(C) ) - 0 by A1,Th41; hence thesis; end; theorem for E being finite non empty set, A,B being Event of E holds prob(A) - prob(B) <= prob(A \ B) proof let E be finite non empty set, A,B be Event of E; A /\ B c= B by XBOOLE_1:17; then prob(A /\ B) <= prob(B) by Th44; then prob(A) - prob(B) <= prob(A) - prob(A /\ B) by REAL_1:92; hence thesis by Th49; end; definition let E be finite non empty set; let B,A be Event of E; func prob(A , B) -> Real equals :Def5: prob(A /\ B) / prob(B); coherence; end; canceled; theorem Th60: for E being finite non empty set, A,B being Event of E st 0 < prob(B) holds prob(A /\ B) = prob(A , B) * prob(B) proof let E be finite non empty set, A,B be Event of E; assume A1: 0 < prob(B); prob(A , B) * prob(B) = prob(A /\ B) / prob(B) * prob(B) by Def5; hence thesis by A1,XCMPLX_1:88; end; theorem Th61: for E being finite non empty set, A being Event of E holds prob(A , [#] E ) = prob(A) proof let E be finite non empty set, A be Event of E; prob([#] E) = 1 by Th39; then A1:prob(A , [#] E) = prob(A /\ [#] E) / 1 by Def5; A c= E; then A c= [#] E by SUBSET_1:def 4; hence thesis by A1,XBOOLE_1:28; end; theorem for E being finite non empty set holds prob([#] E , [#] E) = 1 proof let E be finite non empty set; prob([#] E) = 1 by Th39; hence thesis by Th61; end; theorem for E being finite non empty set holds prob({} E , [#] E) = 0 proof let E be finite non empty set; prob({} E , [#] E) = prob({} E) by Th61; hence thesis by Th40; end; theorem for E being finite non empty set, A,B being Event of E st 0 < prob(B) holds prob(A , B) <= 1 proof let E be finite non empty set, A,B be Event of E; assume A1: 0 < prob(B); then A2: 0 <= (prob(B))" by REAL_1:72; A3: prob(A , B) = prob(A /\ B) / prob(B) by Def5; A /\ B c= B by XBOOLE_1:17; then prob(A /\ B) <= prob(B) by Th44; then prob(A /\ B) * (prob(B))" <= prob(B) * (prob(B))" by A2,AXIOMS:25; then prob(A /\ B) * (prob(B))" <= 1 by A1,XCMPLX_0:def 7; hence thesis by A3,XCMPLX_0:def 9; end; theorem for E being finite non empty set, A,B being Event of E st 0 < prob(B) holds 0 <= prob(A , B) proof let E be finite non empty set, A,B be Event of E; assume A1: 0 < prob(B); 0 <= prob(A /\ B) by Th43; then 0 <= prob(A /\ B) / prob(B) by A1,SQUARE_1:27; hence thesis by Def5; end; theorem Th66: for E being finite non empty set, A,B being Event of E st 0 < prob(B) holds prob(A , B) = 1 - prob(B \ A) / prob(B) proof let E be finite non empty set, A,B be Event of E; assume A1: 0 < prob(B); A2: prob(A , B) = prob(A /\ B) / prob(B) by Def5; prob(B \ A) + prob(A /\ B) = ( prob(B) - prob(A /\ B) ) + prob(A /\ B) by Th49; then ( prob(A /\ B) + prob(B \ A) ) - prob(B \ A) = prob(B) - prob(B \ A) by XCMPLX_1:27; then prob(A , B) = ( prob(B) - prob(B \ A) ) / prob(B) by A2,XCMPLX_1:26; then prob(A , B) = prob(B) / prob(B) - prob(B \ A) / prob(B) by XCMPLX_1:121; hence thesis by A1,XCMPLX_1:60; end; theorem for E being finite non empty set, A,B being Event of E st 0 < prob(B) & A c= B holds prob(A , B) = prob(A) / prob(B) proof let E be finite non empty set, A,B be Event of E; assume that A1: 0 < prob(B) and A2: A c= B; prob(A , B) = 1 - prob(B \ A) / prob(B) by A1,Th66; then prob(A , B) = 1 - ( prob(B) - prob(A) ) / prob(B) by A2,Th50; then prob(A , B) = 1 - ( prob(B) / prob(B) - prob(A) / prob(B) ) by XCMPLX_1:121; then prob(A , B) = 1 - ( 1 - prob(A) / prob(B) ) by A1,XCMPLX_1:60; then prob(A , B) = 1 - 1 + prob(A) / prob(B) by XCMPLX_1:37; hence thesis; end; theorem Th68: for E being finite non empty set, A,B being Event of E st A misses B holds prob(A , B) = 0 proof let E be finite non empty set, A,B be Event of E; assume A misses B; then prob(A /\ B) = 0 by Th41; then prob(A , B) = 0 / prob(B) by Def5 .= 0 * (prob(B))"; hence thesis; end; theorem Th69: for E being finite non empty set, A,B being Event of E st 0 < prob(A) & 0 < prob(B) holds prob(A) * prob(B , A) = prob(B) * prob(A , B) proof let E be finite non empty set, A,B be Event of E; assume that A1: 0 < prob(A) and A2: 0 < prob(B); prob(A) * prob(B , A) = prob(A /\ B) by A1,Th60; hence thesis by A2,Th60; end; theorem Th70: for E being finite non empty set, A,B being Event of E st 0 < prob B holds prob(A , B) = 1 - prob(A` , B) & prob(A` , B) = 1 - prob(A , B) proof let E be finite non empty set, A,B be Event of E; assume A1: 0 < prob(B); A2: (A \/ A`) /\ B = [#] E /\ B by SUBSET_1:25; [#] E /\ B = B proof [#] E /\ B = E /\ B by SUBSET_1:def 4; hence thesis by XBOOLE_1:28; end; then A3: (A /\ B) \/ (A` /\ B) = B by A2,XBOOLE_1:23; A /\ B misses B /\ A` by Th34; then prob(A /\ B) + prob(A` /\ B) = prob(B) by A3,Th47; then prob(A , B) * prob(B) + prob(A` /\ B) = prob(B) by A1,Th60; then prob(A , B) * prob(B) + prob(A` , B) * prob(B) = prob(B) by A1,Th60; then ( prob(A , B) + prob(A` , B) ) * prob(B) = prob(B) by XCMPLX_1:8; then ( prob(A , B) + prob(A` , B) ) * prob(B) * (prob(B))" = 1 by A1,XCMPLX_0:def 7; then ( prob(A , B) + prob(A` , B) ) * ( prob(B) * (prob(B))" ) = 1 by XCMPLX_1:4; then ( prob(A , B) + prob(A` , B) ) * 1 = 1 by A1,XCMPLX_0:def 7; hence thesis by XCMPLX_1:26; end; theorem Th71: for E being finite non empty set, A,B being Event of E st 0 < prob(B) & B c= A holds prob(A , B) = 1 proof let E be finite non empty set, A,B be Event of E; assume that A1: 0 < prob(B) and A2: B c= A; prob(A /\ B) = prob(B) by A2,XBOOLE_1:28; then prob(A , B) = prob(B) / prob(B) by Def5; hence thesis by A1,XCMPLX_1:60; end; theorem for E being finite non empty set, B being Event of E st 0 < prob(B) holds prob([#] E , B) = 1 proof let E be finite non empty set, B be Event of E; assume A1: 0 < prob(B); B c= E; then B c= [#] E by SUBSET_1:def 4; hence thesis by A1,Th71; end; theorem for E being finite non empty set, A being Event of E st 0 < prob(A) holds prob(A` , A) = 0 proof let E be finite non empty set, A be Event of E; assume A1: 0 < prob(A); A` misses A by SUBSET_1:44; then prob(A` /\ A) = 0 by Th41; then prob(A` , A) * prob(A) = 0 by A1,Th60; hence thesis by A1,XCMPLX_1:6; end; theorem for E being finite non empty set, A being Event of E st prob(A) < 1 holds prob(A , A`) = 0 proof let E be finite non empty set, A be Event of E; assume prob(A) < 1; then prob(A) -1 < 1 - 1 by REAL_1:54; then - ( 1 - prob(A) ) < 0 by XCMPLX_1:143; then 0 < - ( - ( 1 - prob(A) ) ) by REAL_1:66; then A1: 0 < prob(A`) by Th48; A misses A` by SUBSET_1:44; then prob(A /\ A`) = 0 by Th41; then prob(A , A`) * prob(A`) = 0 by A1,Th60; hence thesis by A1,XCMPLX_1:6; end; theorem Th75: for E being finite non empty set, A,B being Event of E st 0 < prob(B) & A misses B holds prob(A` , B) = 1 proof let E be finite non empty set, A,B be Event of E; assume that A1: 0 < prob(B) and A2: A misses B; prob(A , B) = 0 by A2,Th68; then 1 - prob(A` , B) = 0 by A1,Th70; hence thesis by XCMPLX_1:15; end; theorem Th76: for E being finite non empty set, A,B being Event of E st 0 < prob(A) & prob(B) < 1 & A misses B holds prob(A , B`) = prob(A) / (1 - prob(B)) proof let E be finite non empty set, A,B be Event of E; assume that A1: 0 < prob(A) and A2: prob(B) < 1 and A3: A misses B; A4: prob(B`) = 1 - prob(B) by Th48; prob(B) - 1 < 1 - 1 by A2,REAL_1:54; then - ( 1 - prob(B) ) < 0 by XCMPLX_1:143; then 0 < - ( - ( 1 - prob(B) ) ) by REAL_1:66; then A5: 0 < prob(B`) by Th48; then prob(A) * prob(B` , A) = prob(B`) * prob(A , B`) by A1,Th69; then prob(A) * 1 = prob(B`) * prob(A , B`) by A1,A3,Th75; then prob(A) * (prob(B`))" = prob(A , B`) * ( prob(B`) * (prob(B`))" ) by XCMPLX_1:4; then prob(A) * (prob(B`))" = prob(A , B`) * 1 by A5,XCMPLX_0:def 7; hence thesis by A4,XCMPLX_0:def 9; end; theorem for E being finite non empty set, A,B being Event of E st 0 < prob(A) & prob(B) < 1 & A misses B holds prob(A` , B`) = 1 - prob(A) / (1 - prob(B)) proof let E be finite non empty set, A,B be Event of E; assume that A1: 0 < prob(A) and A2: prob(B) < 1 and A3: A misses B; A4: prob(B`) = 1 - prob(B) by Th48; prob(B) -1 < 1 - 1 by A2,REAL_1:54; then - ( 1 - prob(B) ) < 0 by XCMPLX_1:143; then 0 < - ( - ( 1 - prob(B) ) ) by REAL_1:66; then prob(A` , B`) = 1 - prob(A , B`) by A4,Th70; hence thesis by A1,A2,A3,Th76; end; theorem for E being finite non empty set, A,B,C being Event of E st 0 < prob(B /\ C) & 0 < prob(C) holds prob(A /\ B /\ C) = prob(A , B /\ C) * prob(B , C) * prob(C) proof let E be finite non empty set, A,B,C be Event of E; assume that A1: 0 < prob(B /\ C) and A2: 0 < prob(C); prob(A /\ B /\ C) = prob(A /\ (B /\ C)) by XBOOLE_1:16; then A3: prob(A /\ B /\ C) = prob(A , B /\ C) * prob(B /\ C) by A1,Th60; prob(B /\ C) = prob(B , C) * prob(C) by A2,Th60; hence thesis by A3,XCMPLX_1:4; end; theorem Th79: for E being finite non empty set, A,B being Event of E st 0 < prob(B) & prob(B) < 1 holds prob(A) = prob(A , B) * prob(B) + prob(A , B`) * prob(B`) proof let E be finite non empty set, A,B be Event of E; assume that A1: 0 < prob(B) and A2: prob(B) < 1; prob(B) -1 < 1 - 1 by A2,REAL_1:54; then - ( 1 - prob(B) ) < 0 by XCMPLX_1:143; then 0 < - ( - ( 1 - prob(B) ) ) by REAL_1:66; then A3: 0 < prob(B`) by Th48; prob(A) = prob(A /\ B) + prob(A /\ B`) by Th53; then prob(A) = prob(A , B) * prob(B) + prob(A /\ B`) by A1,Th60; hence thesis by A3,Th60; end; theorem Th80: for E being finite non empty set, A,B1,B2 being Event of E st 0 < prob(B1) & 0 < prob(B2) & B1 \/ B2 = E & B1 misses B2 holds prob(A) = prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) proof let E be finite non empty set, A,B1,B2 be Event of E; assume that A1: 0 < prob(B1) and A2: 0 < prob(B2) and A3: B1 \/ B2 = E and A4: B1 misses B2; B2 \ B1 = E \ B1 by A3,XBOOLE_1:40; then A5: B2 = E \ B1 by A4,XBOOLE_1:83; then A6: B2 = (B1)` by SUBSET_1:def 5; 0 < prob((B1)`) by A2,A5,SUBSET_1:def 5; then 0 < 1 - prob(B1) by Th48; then 1 - ( 1 - prob(B1) ) < 1 by SQUARE_1:29; then 1 - 1 + prob(B1) < 1 by XCMPLX_1:37; hence thesis by A1,A6,Th79; end; theorem Th81: for E being finite non empty set, A,B1,B2,B3 being Event of E st 0 < prob(B1) & 0 < prob(B2) & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds prob(A) = ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ) + prob(A , B3) * prob(B3) proof let E be finite non empty set, A,B1,B2,B3 be Event of E; assume that A1: 0 < prob(B1) and A2: 0 < prob(B2) and A3: 0 < prob(B3) and A4: B1 \/ B2 \/ B3 = E and A5: B1 /\ B2 = {} and A6: B1 /\ B3 = {} and A7: B2 /\ B3 = {}; (B1 \/ B2 \/ B3) /\ A = A by A4,XBOOLE_1:28; then A8: ((B1 \/ B2) /\ A) \/ (B3 /\ A) = A by XBOOLE_1:23; (B1 /\ B3) \/ (B2 /\ B3) = B2 /\ B3 by A6; then (B1 \/ B2) /\ B3 = {} by A7,XBOOLE_1:23; then (B1 \/ B2) misses B3 by XBOOLE_0:def 7; then (B1 \/ B2) /\ A misses B3 /\ A by XBOOLE_1:76; then prob(A) = prob((B1 \/ B2) /\ A) + prob(B3 /\ A) by A8,Th47; then A9: prob(A) = prob((B1 /\ A) \/ (B2 /\ A)) + prob(B3 /\ A) by XBOOLE_1:23; B1 misses B2 by A5,XBOOLE_0:def 7; then B1 /\ A misses B2 /\ A by XBOOLE_1:76; then prob(A) = prob(A /\ B1) + prob(A /\ B2) + prob(A /\ B3) by A9,Th47; then prob(A) = prob(A , B1) * prob(B1) + prob(A /\ B2) + prob(A /\ B3) by A1,Th60; then prob(A) = prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) + prob(A /\ B3) by A2,Th60; hence thesis by A3,Th60; end; theorem for E being finite non empty set, A,B1,B2 being Event of E st 0 < prob(B1) & 0 < prob(B2) & B1 \/ B2 = E & B1 misses B2 holds prob(B1 , A) = ( prob(A , B1) * prob(B1) ) / ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ) proof let E be finite non empty set, A,B1,B2 be Event of E; assume that A1: 0 < prob(B1) and A2: 0 < prob(B2) and A3: B1 \/ B2 = E and A4: B1 misses B2; A5: prob(A) = prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) by A1,A2,A3,A4,Th80; prob(B1 , A) = prob(A /\ B1) / prob(A) by Def5; hence thesis by A1,A5,Th60; end; theorem for E being finite non empty set, A,B1,B2,B3 being Event of E st 0 < prob(B1) & 0 < prob(B2) & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds prob(B1 , A) = ( prob(A , B1) * prob(B1) ) / ( ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ) + prob(A , B3) * prob(B3) ) proof let E be finite non empty set, A,B1,B2,B3 be Event of E; assume that A1: 0 < prob(B1) and A2: 0 < prob(B2) and A3: 0 < prob(B3) and A4: B1 \/ B2 \/ B3 = E and A5: B1 misses B2 and A6: B1 misses B3 and A7: B2 misses B3; A8: prob(A) = ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ) + prob(A , B3) * prob(B3) by A1,A2,A3,A4,A5,A6,A7,Th81; prob(B1 , A) = prob(A /\ B1) / prob(A) by Def5; hence thesis by A1,A8,Th60; end; definition let E be finite non empty set; let A, B be Event of E; pred A, B are_independent means :Def6: prob(A /\ B) = prob(A) * prob(B); symmetry; end; canceled 2; theorem for E being finite non empty set, A,B being Event of E st 0 < prob(B) & A, B are_independent holds prob(A , B) = prob(A) proof let E be finite non empty set, A,B be Event of E; assume that A1: 0 < prob(B) and A2: A , B are_independent; prob(A /\ B) = prob(A) * prob(B) by A2,Def6; then prob(A , B) = ( prob(A) * prob(B) ) / prob(B) by Def5; then prob(A , B) = prob(A) * ( prob(B) / prob(B) ) by XCMPLX_1:75; then prob(A , B) = prob(A) * 1 by A1,XCMPLX_1:60; hence thesis; end; theorem for E being finite non empty set, A,B being Event of E st prob(B) = 0 holds A , B are_independent proof let E be finite non empty set, A,B be Event of E; assume A1: prob(B) = 0; A /\ B c= B by XBOOLE_1:17; then prob(A /\ B) <= 0 by A1,Th44; then A2: prob(A /\ B) = 0 by Th43; 0 = prob(A) * 0; hence thesis by A1,A2,Def6; end; theorem for E being finite non empty set, A,B being Event of E st A , B are_independent holds A` , B are_independent proof let E be finite non empty set, A,B be Event of E; assume A1: A , B are_independent; prob(A` /\ B) = prob(B \ A) by SUBSET_1:32; then prob(A` /\ B) = prob(B) - prob(A /\ B) by Th49; then prob(A` /\ B) = 1 * prob(B) - prob(A) * prob(B) by A1,Def6; then prob(A` /\ B) = ( 1 - prob(A) ) * prob(B) by XCMPLX_1:40; then prob(A` /\ B) = prob(A`) * prob(B) by Th48; hence thesis by Def6; end; theorem for E being finite non empty set, A,B being Event of E st A misses B & A, B are_independent holds prob(A) = 0 or prob(B) = 0 proof let E be finite non empty set, A,B be Event of E; assume that A1: A misses B and A2: A , B are_independent; prob(A /\ B) = 0 by A1,Th41; then prob(A) * prob(B) = 0 by A2,Def6; hence thesis by XCMPLX_1:6; end;

Back to top