:: Introduction to Probability :: by Jan Popio{\l}ek :: :: Received June 13, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, TARSKI, FINSET_1, RELAT_1, CARD_1, ARYTM_3, XXREAL_0, REAL_1, ARYTM_1, RPR_1, BSPACE; notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, DOMAIN_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, REAL_1, XREAL_0, FINSEQ_1, FINSET_1, XXREAL_0; constructors XXREAL_0, REAL_1, NAT_1, MEMBERED, FINSEQ_1, DOMAIN_1, XREAL_0; registrations RELSET_1, FINSET_1, XXREAL_0, XREAL_0, CARD_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions XBOOLE_0; equalities XBOOLE_0, SUBSET_1; expansions XBOOLE_0; theorems TARSKI, SUBSET_1, ZFMISC_1, FINSEQ_1, CARD_1, CARD_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, NAT_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; theorem Th1: for e being non empty Subset of E holds e is Singleton 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 Singleton of E implies for Y holds (Y c= e iff Y = {} or Y = e) proof assume A1: e is Singleton of E; let Y; ex x being object st e = {x} by A1,ZFMISC_1:131; hence thesis by ZFMISC_1:33; end; assume A2: for Y holds Y c= e iff Y = {} or Y = e; consider x being object such that A3: x in e by XBOOLE_0:def 1; {x} c= e by A3,ZFMISC_1:31; hence thesis by A2; end; registration let E; cluster -> finite for Singleton of E; coherence; end; reserve e, e1, e2 for Singleton of E; 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 by A1,XBOOLE_1:7; then A3: A = {} or A = e by Th1; B c= e by A1,XBOOLE_1:7; hence thesis by A2,A3,Th1; 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 {a} is Singleton of E; theorem e1 c= e2 implies e1 = e2 by Th1; theorem Th6: ex a st a in E & e = {a} proof set x = the Element of e; {x} = e by Th1; hence thesis; end; theorem ex e st e is Singleton of E proof take {the Element of E}; thus thesis; end; theorem ex p st p is FinSequence of E & rng p = e & len p = 1 proof consider a such that a in E and A1: e = {a} by Th6; rng <*a*> = {a} & len <*a*> = 1 by FINSEQ_1:39; hence thesis by A1; end; definition let E be set; mode Event of E is Subset of E; end; theorem for E being non empty set, e being Singleton of E, A being Event of E holds e misses A or e /\ A = e proof let E be non empty set, e be Singleton of E, A be Event of E; e /\ E = e & A \/ A` = [#] E by SUBSET_1:10,XBOOLE_1:28; then e = e /\ A \/ e /\ A` by XBOOLE_1:23; then e /\ A c= e by XBOOLE_1:7; then e /\ A = {} or e /\ A = e by Th1; hence thesis; end; theorem for E being non empty set, A being Event of E st A <> {} ex e being Singleton of E st e c= A proof let E be non empty set, A be Event of E; set x = the Element of A; assume A1: A <> {}; then reconsider x as Element of E by TARSKI:def 3; {x} c= A by A1,ZFMISC_1:31; hence thesis; end; theorem for E being non empty set, e being Singleton 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 Singleton of E, A be Event of E; ex a being Element of E st a in E & e = {a} by Th6; then consider a being Element of E such that A1: e = {a}; assume e c= A \/ A`; then a in A \/ A` by A1,ZFMISC_1:31; then a in A or a in A` by XBOOLE_0:def 3; hence thesis by A1,ZFMISC_1:31; 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; end; theorem Th13: A /\ B misses A /\ B` proof A /\ B misses A \ B by XBOOLE_1:89; hence thesis by SUBSET_1:13; end; Lm1: for E being finite non empty set holds 0 < card E proof let E be finite non empty set; card {the Element of E} <= card E by NAT_1:43; hence thesis by CARD_1:30; end; definition let E be finite set; let A be Event of E; func prob(A) -> Real equals card A / card E; coherence; end; theorem for E being finite non empty set, e being Singleton of E holds prob(e) = 1 / card E by CARD_1:def 7; theorem for E being finite non empty set holds prob([#] E) = 1 by XCMPLX_1:60; theorem Th16: for E being finite non empty set, A,B being Event of E st A misses B holds prob(A /\ B) = 0 by CARD_1:27; 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; 0 < card E by Lm1; then card A * (card E)" <= card E * (card E)" by NAT_1:43,XREAL_1:64; then card A / card E <= card E * (card E)" by XCMPLX_0:def 9; then prob([#] E) = card E / card E & prob(A) <= card E / card E by XCMPLX_0:def 9; hence thesis by XCMPLX_1:60; end; theorem Th18: 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; 0 < card E & 0 <= card A by Lm1,CARD_1:27; hence thesis; end; theorem Th19: 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 A1: A c= B; 0 < card E by Lm1; then card A * (card E)" <= card B * (card E)" by A1,NAT_1:43,XREAL_1:64; then card A / card E <= card B * (card E)" by XCMPLX_0:def 9; hence thesis by XCMPLX_0:def 9; end; theorem Th20: 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; set q = ( card E )"; set p = card E; card (( A \/ B ) qua Event of E) = card A + card B - card ( A /\ B ) by CARD_2:45; then card ( A \/ B ) * q = card A * q + ( card B * q - card ( A /\ B ) * q ); 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; hence thesis by XCMPLX_0:def 9; end; theorem Th21: 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 Th16; then prob(A \/ B) = prob(A) + prob(B) - 0 by Th20; hence thesis; end; theorem Th22: 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:24; then prob(A \/ A`) = prob(A) + prob(A`) by Th21; then prob( [#] E ) = prob(A) + prob(A`) by SUBSET_1:10; then 1 = prob(A) + prob(A`) by XCMPLX_1:60; hence thesis; end; theorem Th23: 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; prob(A) = prob((A \ B) \/ (A /\ B)) by XBOOLE_1:51; then prob(A) = prob(A \ B) + prob(A /\ B) by Th21,XBOOLE_1:89; hence thesis; end; theorem Th24: 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 Th23; 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; prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B) by Th20; hence thesis by Th18,XREAL_1:43; end; theorem Th26: 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 = A /\ ( A \/ [#] E ) by XBOOLE_1:21; then A = A /\ [#] E by SUBSET_1:11; then A1: A = A /\ ( B \/ B`) by SUBSET_1:10; prob((A /\ B) \/ (A /\ B`)) = prob(A /\ B) + prob(A /\ B`) by Th13,Th21; 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; prob(A \/ (B \ A)) = prob(A \/ B) by XBOOLE_1:39; then prob(A \/ B) = prob(A) + prob(B \ A) by Th21,XBOOLE_1:79; hence thesis; 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`) & prob(B) = prob(A /\ B) + prob(B /\ A`) by Th26; hence thesis; end; theorem Th29: 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 Th20 .= ( ( prob(A) + prob(B) ) - prob(A /\ B) ) + prob(C) - prob((A \/ B) /\ C) by Th20 .= ( 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 Th20 .= ( 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); hence thesis; 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; A4: prob(A /\ (B /\ C)) = 0 by A1,Th16,XBOOLE_1:74; prob(A \/ B \/ C) = ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) by Th29 .= ( 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,Th16 .= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + 0 ) by A2,Th16 .= ( prob(A) + prob(B) + prob(C) ) - 0 by A1,Th16; 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; prob(A /\ B) <= prob(B) by Th19,XBOOLE_1:17; then prob(A) - prob(B) <= prob(A) - prob(A /\ B) by XREAL_1:13; hence thesis by Th23; end; definition let E be finite set; let B,A be Event of E; func prob(A, B) -> Real equals prob(A /\ B) / prob(B); coherence; end; theorem 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 XCMPLX_1:60; hence thesis by 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 XCMPLX_1:60; hence thesis; 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); A /\ B c= B by XBOOLE_1:17; then prob(A /\ B) * (prob(B))" <= prob(B) * (prob(B))" by A1,Th19,XREAL_1:64; then prob(A /\ B) * (prob(B))" <= 1 by A1,XCMPLX_0:def 7; hence thesis by 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 Th18; hence thesis by A1; end; theorem Th36: 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; prob(B \ A) + prob(A /\ B) = ( prob(B) - prob(A /\ B) ) + prob(A /\ B) by Th23; then prob(A, B) = ( prob(B) - prob(B \ A) ) / prob(B); then A1: prob(A, B) = prob(B) / prob(B) - prob(B \ A) / prob(B) by XCMPLX_1:120; assume 0 < prob(B); 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,Th36; then prob(A, B) = 1 - ( prob(B) - prob(A) ) / prob(B) by A2,Th24; then prob(A, B) = 1 - ( prob(B) / prob(B) - prob(A) / prob(B) ) by XCMPLX_1:120; then prob(A, B) = 1 - ( 1 - prob(A) / prob(B) ) by A1,XCMPLX_1:60; hence thesis; end; theorem Th38: 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 / prob(B) by Th16 .= 0 * (prob(B))"; hence thesis; end; theorem Th39: 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,XCMPLX_1:87; hence thesis by A2,XCMPLX_1:87; end; theorem Th40: 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); (A \/ A`) /\ B = [#] E /\ B & [#] E /\ B = B by SUBSET_1:10,XBOOLE_1:28; then (A /\ B) \/ (A` /\ B) = B by XBOOLE_1:23; then prob(A /\ B) + prob(A` /\ B) = prob(B) by Th13,Th21; then prob(A, B) * prob(B) + prob(A` /\ B) = prob(B) by A1,XCMPLX_1:87; then prob(A, B) * prob(B) + prob(A`, B) * prob(B) = prob(B) by A1,XCMPLX_1:87 ; 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; then ( prob(A, B) + prob(A`, B) ) * 1 = 1 by A1,XCMPLX_0:def 7; hence thesis; end; theorem Th41: 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; 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 by Th41; theorem for E being finite non empty set, A being Event of E holds prob(A`, A) = 0 proof let E be finite non empty set, A be Event of E; A` misses A by SUBSET_1:24; then prob(A` /\ A) = 0 by Th16; hence thesis; end; theorem for E being finite non empty set, A being Event of E holds prob(A, A`) = 0 proof let E be finite non empty set, A be Event of E; A misses A` by SUBSET_1:24; then prob(A /\ A`) = 0 by Th16; hence thesis; end; theorem Th45: 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,Th38; then 1 - prob(A`, B) = 0 by A1,Th40; hence thesis; end; theorem Th46: 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; prob(B) - 1 < 1 - 1 by A2,XREAL_1:9; then 0 < - ( - ( 1 - prob(B) ) ); then A4: 0 < prob(B`) by Th22; then prob(A) * prob(B`, A) = prob(B`) * prob(A, B`) by A1,Th39; then prob(A) * 1 = prob(B`) * prob(A, B`) by A1,A3,Th45; then prob(A) * (prob(B`))" = prob(A, B`) * ( prob(B`) * (prob(B`))" ); then A5: prob(A) * (prob(B`))" = prob(A, B`) * 1 by A4,XCMPLX_0:def 7; prob(B`) = 1 - prob(B) by Th22; hence thesis by A5,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 Th22; prob(B) -1 < 1 - 1 by A2,XREAL_1:9; then 0 < - ( - ( 1 - prob(B) ) ); then prob(A` , B`) = 1 - prob(A, B`) by A4,Th40; hence thesis by A1,A2,A3,Th46; 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); A3: prob(B /\ C) = prob(B, C) * prob(C) by A2,XCMPLX_1:87; prob(A /\ B /\ C) = prob(A /\ (B /\ C)) by XBOOLE_1:16; then prob(A /\ B /\ C) = prob(A, B /\ C) * prob(B /\ C) by A1,XCMPLX_1:87; hence thesis by A3; end; theorem Th49: 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,XREAL_1:9; then 0 < - ( - ( 1 - prob(B) ) ); then A3: 0 < prob(B`) by Th22; prob(A) = prob(A /\ B) + prob(A /\ B`) by Th26; then prob(A) = prob(A, B) * prob(B) + prob(A /\ B`) by A1,XCMPLX_1:87; hence thesis by A3,XCMPLX_1:87; end; theorem Th50: 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; A5: B2 \ B1 = E \ B1 by A3,XBOOLE_1:40; then 0 < prob((B1)`) by A2,A4,XBOOLE_1:83; then 0 < 1 - prob(B1) by Th22; then A6: 1 - ( 1 - prob(B1) ) < 1 by XREAL_1:44; B2 = B1` by A4,A5,XBOOLE_1:83; hence thesis by A1,A6,Th49; end; theorem Th51: 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 /\ B3) \/ (B2 /\ B3) = B2 /\ B3 by A6; then (B1 \/ B2) /\ B3 = {} by A7,XBOOLE_1:23; then A8: (B1 \/ B2) misses B3; (B1 \/ B2 \/ B3) /\ A = A by A4,XBOOLE_1:28; then ((B1 \/ B2) /\ A) \/ (B3 /\ A) = A by XBOOLE_1:23; then prob(A) = prob((B1 \/ B2) /\ A) + prob(B3 /\ A) by A8,Th21,XBOOLE_1:76; then A9: prob(A) = prob((B1 /\ A) \/ (B2 /\ A)) + prob(B3 /\ A) by XBOOLE_1:23; B1 misses B2 by A5; then prob(A) = prob(A /\ B1) + prob(A /\ B2) + prob(A /\ B3) by A9,Th21, XBOOLE_1:76; then prob(A) = prob(A, B1) * prob(B1) + prob(A /\ B2) + prob(A /\ B3) by A1, XCMPLX_1:87; then prob(A) = prob(A, B1) * prob(B1) + prob(A, B2) * prob(B2) + prob(A /\ B3) by A2,XCMPLX_1:87; hence thesis by A3,XCMPLX_1:87; 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) & B1 \/ B2 = E & B1 misses B2; prob(A) = prob(A, B1) * prob(B1) + prob(A, B2) * prob(B2) by A1,A2,Th50; hence thesis by A1,XCMPLX_1:87; 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) & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3; prob(A) = ( prob(A, B1) * prob(B1) + prob(A, B2) * prob(B2) ) + prob(A, B3) * prob(B3) by A1,A2,Th51; hence thesis by A1,XCMPLX_1:87; end; definition let E be finite set; let A, B be Event of E; pred A, B are_independent means prob(A /\ B) = prob(A) * prob(B); symmetry; end; 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; then prob(A, B) = prob(A) * ( prob(B) / prob(B) ) by XCMPLX_1:74; 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; then prob(A /\ B) <= 0 by Th19,XBOOLE_1:17; then prob(A /\ B) = 0 by Th18; hence thesis by A1; 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; prob(A` /\ B) = prob(B \ A) by SUBSET_1:13; then A1: prob(A` /\ B) = prob(B) - prob(A /\ B) by Th23; assume A, B are_independent; then prob(A` /\ B) = 1 * prob(B) - prob(A) * prob(B) by A1; then prob(A` /\ B) = ( 1 - prob(A) ) * prob(B); then prob(A` /\ B) = prob(A`) * prob(B) by Th22; hence thesis; 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 by Th16,XCMPLX_1:6;