:: RPR_1 semantic presentation begin theorem Th1: :: RPR_1:1 for E being non empty set for e being non empty Subset of E holds ( e is Singleton of E iff for Y being set holds ( Y c= e iff ( Y = {} or Y = e ) ) ) proof let E be non empty set ; ::_thesis: for e being non empty Subset of E holds ( e is Singleton of E iff for Y being set holds ( Y c= e iff ( Y = {} or Y = e ) ) ) let e be non empty Subset of E; ::_thesis: ( e is Singleton of E iff for Y being set holds ( Y c= e iff ( Y = {} or Y = e ) ) ) thus ( e is Singleton of E implies for Y being set holds ( Y c= e iff ( Y = {} or Y = e ) ) ) ::_thesis: ( ( for Y being set holds ( Y c= e iff ( Y = {} or Y = e ) ) ) implies e is Singleton of E ) proof assume A1: e is Singleton of E ; ::_thesis: for Y being set holds ( Y c= e iff ( Y = {} or Y = e ) ) let Y be set ; ::_thesis: ( Y c= e iff ( Y = {} or Y = e ) ) ex x being set st e = {x} by A1, ZFMISC_1:131; hence ( Y c= e iff ( Y = {} or Y = e ) ) by ZFMISC_1:33; ::_thesis: verum end; assume A2: for Y being set holds ( Y c= e iff ( Y = {} or Y = e ) ) ; ::_thesis: e is Singleton of E consider x being set such that A3: x in e by XBOOLE_0:def_1; {x} c= e by A3, ZFMISC_1:31; hence e is Singleton of E by A2; ::_thesis: verum end; registration let E be non empty set ; cluster1 -element -> finite for Element of K11(E); coherence for b1 being Singleton of E holds b1 is finite ; end; theorem :: RPR_1:2 for E being non empty set for A, B being Subset of E for e being Singleton of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds ( A = e & B = {} ) proof let E be non empty set ; ::_thesis: for A, B being Subset of E for e being Singleton of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds ( A = e & B = {} ) let A, B be Subset of E; ::_thesis: for e being Singleton of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds ( A = e & B = {} ) let e be Singleton of E; ::_thesis: ( e = A \/ B & A <> B & not ( A = {} & B = e ) implies ( A = e & B = {} ) ) assume that A1: e = A \/ B and A2: A <> B ; ::_thesis: ( ( A = {} & B = e ) or ( A = e & 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 ( ( A = {} & B = e ) or ( A = e & B = {} ) ) by A2, A3, Th1; ::_thesis: verum end; theorem :: RPR_1:3 for E being non empty set for A, B being Subset of E for e being Singleton of E holds ( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) ) proof let E be non empty set ; ::_thesis: for A, B being Subset of E for e being Singleton of E holds ( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) ) let A, B be Subset of E; ::_thesis: for e being Singleton of E holds ( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) ) let e be Singleton of E; ::_thesis: ( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) ) assume A1: e = A \/ B ; ::_thesis: ( ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) ) 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 ( ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) ) by A1; ::_thesis: verum end; theorem :: RPR_1:4 for E being non empty set for a being Element of E holds {a} is Singleton of E ; theorem :: RPR_1:5 for E being non empty set for e1, e2 being Singleton of E st e1 c= e2 holds e1 = e2 by Th1; theorem Th6: :: RPR_1:6 for E being non empty set for e being Singleton of E ex a being Element of E st ( a in E & e = {a} ) proof let E be non empty set ; ::_thesis: for e being Singleton of E ex a being Element of E st ( a in E & e = {a} ) let e be Singleton of E; ::_thesis: ex a being Element of E st ( a in E & e = {a} ) set x = the Element of e; { the Element of e} = e by Th1; hence ex a being Element of E st ( a in E & e = {a} ) ; ::_thesis: verum end; theorem :: RPR_1:7 for E being non empty set ex e being Singleton of E st e is Singleton of E proof let E be non empty set ; ::_thesis: ex e being Singleton of E st e is Singleton of E take { the Element of E} ; ::_thesis: { the Element of E} is Singleton of E thus { the Element of E} is Singleton of E ; ::_thesis: verum end; theorem :: RPR_1:8 for E being non empty set for e being Singleton of E ex p being FinSequence st ( p is FinSequence of E & rng p = e & len p = 1 ) proof let E be non empty set ; ::_thesis: for e being Singleton of E ex p being FinSequence st ( p is FinSequence of E & rng p = e & len p = 1 ) let e be Singleton of E; ::_thesis: ex p being FinSequence st ( p is FinSequence of E & rng p = e & len p = 1 ) consider a being Element of E such that a in E and A1: e = {a} by Th6; ( rng <*a*> = {a} & len <*a*> = 1 ) by FINSEQ_1:39; hence ex p being FinSequence st ( p is FinSequence of E & rng p = e & len p = 1 ) by A1; ::_thesis: verum end; definition let E be set ; mode Event of E is Subset of E; end; theorem :: RPR_1:9 for E being non empty set for e being Singleton of E for A being Event of E holds ( e misses A or e /\ A = e ) proof let E be non empty set ; ::_thesis: for e being Singleton of E for A being Event of E holds ( e misses A or e /\ A = e ) let e be Singleton of E; ::_thesis: for A being Event of E holds ( e misses A or e /\ A = e ) let A be Event of E; ::_thesis: ( e misses A or e /\ A = 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 ( e misses A or e /\ A = e ) by XBOOLE_0:def_7; ::_thesis: verum end; theorem :: RPR_1:10 for E being non empty set for A being Event of E st A <> {} holds ex e being Singleton of E st e c= A proof let E be non empty set ; ::_thesis: for A being Event of E st A <> {} holds ex e being Singleton of E st e c= A let A be Event of E; ::_thesis: ( A <> {} implies ex e being Singleton of E st e c= A ) set x = the Element of A; assume A1: A <> {} ; ::_thesis: ex e being Singleton of E st e c= A then reconsider x = the Element of A as Element of E by TARSKI:def_3; {x} c= A by A1, ZFMISC_1:31; hence ex e being Singleton of E st e c= A ; ::_thesis: verum end; theorem :: RPR_1:11 for E being non empty set for e being Singleton of E for A being Event of E holds ( not e c= A \/ (A `) or e c= A or e c= A ` ) proof let E be non empty set ; ::_thesis: for e being Singleton of E for A being Event of E holds ( not e c= A \/ (A `) or e c= A or e c= A ` ) let e be Singleton of E; ::_thesis: for A being Event of E holds ( not e c= A \/ (A `) or e c= A or e c= A ` ) let A be Event of E; ::_thesis: ( not e c= A \/ (A `) or e c= A or e c= A ` ) 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 `) ; ::_thesis: ( e c= A or e c= 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 ( e c= A or e c= A ` ) by A1, ZFMISC_1:31; ::_thesis: verum end; theorem :: RPR_1:12 for E being non empty set for e1, e2 being Singleton of E holds ( e1 = e2 or e1 misses e2 ) proof let E be non empty set ; ::_thesis: for e1, e2 being Singleton of E holds ( e1 = e2 or e1 misses e2 ) let e1, e2 be Singleton of E; ::_thesis: ( e1 = e2 or e1 misses e2 ) 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 ( e1 = e2 or e1 misses e2 ) by Th1, XBOOLE_0:def_7; ::_thesis: verum end; theorem Th13: :: RPR_1:13 for E being non empty set for A, B being Subset of E holds A /\ B misses A /\ (B `) proof let E be non empty set ; ::_thesis: for A, B being Subset of E holds A /\ B misses A /\ (B `) let A, B be Subset of E; ::_thesis: A /\ B misses A /\ (B `) A /\ B misses A \ B by XBOOLE_1:89; hence A /\ B misses A /\ (B `) by SUBSET_1:13; ::_thesis: verum end; Lm1: for E being non empty finite set holds 0 < card E proof let E be non empty finite set ; ::_thesis: 0 < card E card { the Element of E} <= card E by NAT_1:43; hence 0 < card E by CARD_1:30; ::_thesis: verum end; definition let E be finite set ; let A be Event of E; func prob A -> Real equals :: RPR_1:def 1 (card A) / (card E); coherence (card A) / (card E) is Real by XREAL_0:def_1; end; :: deftheorem defines prob RPR_1:def_1_:_ for E being finite set for A being Event of E holds prob A = (card A) / (card E); theorem :: RPR_1:14 for E being non empty finite set for e being Singleton of E holds prob e = 1 / (card E) by CARD_1:def_7; theorem :: RPR_1:15 for E being non empty finite set holds prob ([#] E) = 1 by XCMPLX_1:60; theorem Th16: :: RPR_1:16 for E being non empty finite set for A, B being Event of E st A misses B holds prob (A /\ B) = 0 proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st A misses B holds prob (A /\ B) = 0 let A, B be Event of E; ::_thesis: ( A misses B implies prob (A /\ B) = 0 ) assume A misses B ; ::_thesis: prob (A /\ B) = 0 then A /\ B = {} E by XBOOLE_0:def_7; hence prob (A /\ B) = 0 by CARD_1:27; ::_thesis: verum end; theorem :: RPR_1:17 for E being non empty finite set for A being Event of E holds prob A <= 1 proof let E be non empty finite set ; ::_thesis: for A being Event of E holds prob A <= 1 let A be Event of E; ::_thesis: prob A <= 1 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 prob A <= 1 by XCMPLX_1:60; ::_thesis: verum end; theorem Th18: :: RPR_1:18 for E being non empty finite set for A being Event of E holds 0 <= prob A proof let E be non empty finite set ; ::_thesis: for A being Event of E holds 0 <= prob A let A be Event of E; ::_thesis: 0 <= prob A ( 0 < card E & 0 <= card A ) by Lm1, CARD_1:27; hence 0 <= prob A ; ::_thesis: verum end; theorem Th19: :: RPR_1:19 for E being non empty finite set for A, B being Event of E st A c= B holds prob A <= prob B proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st A c= B holds prob A <= prob B let A, B be Event of E; ::_thesis: ( A c= B implies prob A <= prob B ) assume A1: A c= B ; ::_thesis: prob A <= prob 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 prob A <= prob B by XCMPLX_0:def_9; ::_thesis: verum end; theorem Th20: :: RPR_1:20 for E being non empty finite set for A, B being Event of E holds prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) let A, B be Event of E; ::_thesis: prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) set q = (card E) " ; set p = card E; card (A \/ B) = ((card A) + (card B)) - (card (A /\ B)) by CARD_2:45; then (card (A \/ B)) * ((card E) ") = ((card A) * ((card E) ")) + (((card B) * ((card E) ")) - ((card (A /\ B)) * ((card E) "))) ; then (card (A \/ B)) / (card E) = (((card A) * ((card E) ")) + ((card B) * ((card E) "))) - ((card (A /\ B)) * ((card E) ")) by XCMPLX_0:def_9; then (card (A \/ B)) / (card E) = (((card A) / (card E)) + ((card B) * ((card E) "))) - ((card (A /\ B)) * ((card E) ")) by XCMPLX_0:def_9; then (card (A \/ B)) / (card E) = (((card A) / (card E)) + ((card B) / (card E))) - ((card (A /\ B)) * ((card E) ")) by XCMPLX_0:def_9; hence prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) by XCMPLX_0:def_9; ::_thesis: verum end; theorem Th21: :: RPR_1:21 for E being non empty finite set for A, B being Event of E st A misses B holds prob (A \/ B) = (prob A) + (prob B) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st A misses B holds prob (A \/ B) = (prob A) + (prob B) let A, B be Event of E; ::_thesis: ( A misses B implies prob (A \/ B) = (prob A) + (prob B) ) assume A misses B ; ::_thesis: prob (A \/ B) = (prob A) + (prob B) then prob (A /\ B) = 0 by Th16; then prob (A \/ B) = ((prob A) + (prob B)) - 0 by Th20; hence prob (A \/ B) = (prob A) + (prob B) ; ::_thesis: verum end; theorem Th22: :: RPR_1:22 for E being non empty finite set for A being Event of E holds ( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) ) proof let E be non empty finite set ; ::_thesis: for A being Event of E holds ( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) ) let A be Event of E; ::_thesis: ( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) ) 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 ( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) ) ; ::_thesis: verum end; theorem Th23: :: RPR_1:23 for E being non empty finite set for A, B being Event of E holds prob (A \ B) = (prob A) - (prob (A /\ B)) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob (A \ B) = (prob A) - (prob (A /\ B)) let A, B be Event of E; ::_thesis: prob (A \ B) = (prob A) - (prob (A /\ B)) 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 prob (A \ B) = (prob A) - (prob (A /\ B)) ; ::_thesis: verum end; theorem Th24: :: RPR_1:24 for E being non empty finite set for A, B being Event of E st B c= A holds prob (A \ B) = (prob A) - (prob B) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st B c= A holds prob (A \ B) = (prob A) - (prob B) let A, B be Event of E; ::_thesis: ( B c= A implies prob (A \ B) = (prob A) - (prob B) ) assume B c= A ; ::_thesis: prob (A \ B) = (prob A) - (prob B) then prob (A /\ B) = prob B by XBOOLE_1:28; hence prob (A \ B) = (prob A) - (prob B) by Th23; ::_thesis: verum end; theorem :: RPR_1:25 for E being non empty finite set for A, B being Event of E holds prob (A \/ B) <= (prob A) + (prob B) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob (A \/ B) <= (prob A) + (prob B) let A, B be Event of E; ::_thesis: prob (A \/ B) <= (prob A) + (prob B) prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) by Th20; hence prob (A \/ B) <= (prob A) + (prob B) by Th18, XREAL_1:43; ::_thesis: verum end; theorem Th26: :: RPR_1:26 for E being non empty finite set for A, B being Event of E holds prob A = (prob (A /\ B)) + (prob (A /\ (B `))) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob A = (prob (A /\ B)) + (prob (A /\ (B `))) let A, B be Event of E; ::_thesis: prob A = (prob (A /\ B)) + (prob (A /\ (B `))) 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 prob A = (prob (A /\ B)) + (prob (A /\ (B `))) by A1, XBOOLE_1:23; ::_thesis: verum end; theorem :: RPR_1:27 for E being non empty finite set for A, B being Event of E holds prob A = (prob (A \/ B)) - (prob (B \ A)) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob A = (prob (A \/ B)) - (prob (B \ A)) let A, B be Event of E; ::_thesis: prob A = (prob (A \/ B)) - (prob (B \ A)) 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 prob A = (prob (A \/ B)) - (prob (B \ A)) ; ::_thesis: verum end; theorem :: RPR_1:28 for E being non empty finite set for A, B being Event of E holds (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A)) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E holds (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A)) let A, B be Event of E; ::_thesis: (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A)) ( prob A = (prob (A /\ B)) + (prob (A /\ (B `))) & prob B = (prob (A /\ B)) + (prob (B /\ (A `))) ) by Th26; hence (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A)) ; ::_thesis: verum end; theorem Th29: :: RPR_1:29 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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)) let A, B, C be Event of E; ::_thesis: prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C)) 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 prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C)) ; ::_thesis: verum end; theorem :: RPR_1:30 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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) let A, B, C be Event of E; ::_thesis: ( A misses B & A misses C & B misses C implies prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C) ) assume that A1: A misses B and A2: A misses C and A3: B misses C ; ::_thesis: prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob 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 prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C) ; ::_thesis: verum end; theorem :: RPR_1:31 for E being non empty finite set for A, B being Event of E holds (prob A) - (prob B) <= prob (A \ B) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E holds (prob A) - (prob B) <= prob (A \ B) let A, B be Event of E; ::_thesis: (prob A) - (prob B) <= prob (A \ B) 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 (prob A) - (prob B) <= prob (A \ B) by Th23; ::_thesis: verum end; definition let E be finite set ; let B, A be Event of E; func prob (A,B) -> Real equals :: RPR_1:def 2 (prob (A /\ B)) / (prob B); coherence (prob (A /\ B)) / (prob B) is Real ; end; :: deftheorem defines prob RPR_1:def_2_:_ for E being finite set for B, A being Event of E holds prob (A,B) = (prob (A /\ B)) / (prob B); theorem :: RPR_1:32 for E being non empty finite set for A being Event of E holds prob (A,([#] E)) = prob A proof let E be non empty finite set ; ::_thesis: for A being Event of E holds prob (A,([#] E)) = prob A let A be Event of E; ::_thesis: prob (A,([#] E)) = prob A prob ([#] E) = 1 by XCMPLX_1:60; hence prob (A,([#] E)) = prob A by XBOOLE_1:28; ::_thesis: verum end; theorem :: RPR_1:33 for E being non empty finite set holds prob (([#] E),([#] E)) = 1 proof let E be non empty finite set ; ::_thesis: prob (([#] E),([#] E)) = 1 prob ([#] E) = 1 by XCMPLX_1:60; hence prob (([#] E),([#] E)) = 1 ; ::_thesis: verum end; theorem :: RPR_1:34 for E being non empty finite set for A, B being Event of E st 0 < prob B holds prob (A,B) <= 1 proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B holds prob (A,B) <= 1 let A, B be Event of E; ::_thesis: ( 0 < prob B implies prob (A,B) <= 1 ) assume A1: 0 < prob B ; ::_thesis: prob (A,B) <= 1 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 prob (A,B) <= 1 by XCMPLX_0:def_9; ::_thesis: verum end; theorem :: RPR_1:35 for E being non empty finite set for A, B being Event of E st 0 < prob B holds 0 <= prob (A,B) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B holds 0 <= prob (A,B) let A, B be Event of E; ::_thesis: ( 0 < prob B implies 0 <= prob (A,B) ) assume A1: 0 < prob B ; ::_thesis: 0 <= prob (A,B) 0 <= prob (A /\ B) by Th18; hence 0 <= prob (A,B) by A1; ::_thesis: verum end; theorem Th36: :: RPR_1:36 for E being non empty finite set for A, B being Event of E st 0 < prob B holds prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B holds prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) let A, B be Event of E; ::_thesis: ( 0 < prob B implies prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) ) (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 ; ::_thesis: prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) hence prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) by A1, XCMPLX_1:60; ::_thesis: verum end; theorem :: RPR_1:37 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & A c= B holds prob (A,B) = (prob A) / (prob B) let A, B be Event of E; ::_thesis: ( 0 < prob B & A c= B implies prob (A,B) = (prob A) / (prob B) ) assume that A1: 0 < prob B and A2: A c= B ; ::_thesis: prob (A,B) = (prob A) / (prob 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 prob (A,B) = (prob A) / (prob B) ; ::_thesis: verum end; theorem Th38: :: RPR_1:38 for E being non empty finite set for A, B being Event of E st A misses B holds prob (A,B) = 0 proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st A misses B holds prob (A,B) = 0 let A, B be Event of E; ::_thesis: ( A misses B implies prob (A,B) = 0 ) assume A misses B ; ::_thesis: prob (A,B) = 0 then prob (A,B) = 0 / (prob B) by Th16 .= 0 * ((prob B) ") ; hence prob (A,B) = 0 ; ::_thesis: verum end; theorem Th39: :: RPR_1:39 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob A & 0 < prob B holds (prob A) * (prob (B,A)) = (prob B) * (prob (A,B)) let A, B be Event of E; ::_thesis: ( 0 < prob A & 0 < prob B implies (prob A) * (prob (B,A)) = (prob B) * (prob (A,B)) ) assume that A1: 0 < prob A and A2: 0 < prob B ; ::_thesis: (prob A) * (prob (B,A)) = (prob B) * (prob (A,B)) (prob A) * (prob (B,A)) = prob (A /\ B) by A1, XCMPLX_1:87; hence (prob A) * (prob (B,A)) = (prob B) * (prob (A,B)) by A2, XCMPLX_1:87; ::_thesis: verum end; theorem Th40: :: RPR_1:40 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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)) ) let A, B be Event of E; ::_thesis: ( 0 < prob B implies ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) ) ) assume A1: 0 < prob B ; ::_thesis: ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,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 ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) ) ; ::_thesis: verum end; theorem Th41: :: RPR_1:41 for E being non empty finite set for A, B being Event of E st 0 < prob B & B c= A holds prob (A,B) = 1 proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & B c= A holds prob (A,B) = 1 let A, B be Event of E; ::_thesis: ( 0 < prob B & B c= A implies prob (A,B) = 1 ) assume that A1: 0 < prob B and A2: B c= A ; ::_thesis: prob (A,B) = 1 prob (A /\ B) = prob B by A2, XBOOLE_1:28; hence prob (A,B) = 1 by A1, XCMPLX_1:60; ::_thesis: verum end; theorem :: RPR_1:42 for E being non empty finite set for B being Event of E st 0 < prob B holds prob (([#] E),B) = 1 by Th41; theorem :: RPR_1:43 for E being non empty finite set for A being Event of E holds prob ((A `),A) = 0 proof let E be non empty finite set ; ::_thesis: for A being Event of E holds prob ((A `),A) = 0 let A be Event of E; ::_thesis: prob ((A `),A) = 0 A ` misses A by SUBSET_1:24; then prob ((A `) /\ A) = 0 by Th16; hence prob ((A `),A) = 0 ; ::_thesis: verum end; theorem :: RPR_1:44 for E being non empty finite set for A being Event of E holds prob (A,(A `)) = 0 proof let E be non empty finite set ; ::_thesis: for A being Event of E holds prob (A,(A `)) = 0 let A be Event of E; ::_thesis: prob (A,(A `)) = 0 A misses A ` by SUBSET_1:24; then prob (A /\ (A `)) = 0 by Th16; hence prob (A,(A `)) = 0 ; ::_thesis: verum end; theorem Th45: :: RPR_1:45 for E being non empty finite set for A, B being Event of E st 0 < prob B & A misses B holds prob ((A `),B) = 1 proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & A misses B holds prob ((A `),B) = 1 let A, B be Event of E; ::_thesis: ( 0 < prob B & A misses B implies prob ((A `),B) = 1 ) assume that A1: 0 < prob B and A2: A misses B ; ::_thesis: prob ((A `),B) = 1 prob (A,B) = 0 by A2, Th38; then 1 - (prob ((A `),B)) = 0 by A1, Th40; hence prob ((A `),B) = 1 ; ::_thesis: verum end; theorem Th46: :: RPR_1:46 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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)) let A, B be Event of E; ::_thesis: ( 0 < prob A & prob B < 1 & A misses B implies prob (A,(B `)) = (prob A) / (1 - (prob B)) ) assume that A1: 0 < prob A and A2: prob B < 1 and A3: A misses B ; ::_thesis: prob (A,(B `)) = (prob A) / (1 - (prob 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 prob (A,(B `)) = (prob A) / (1 - (prob B)) by A5, XCMPLX_0:def_9; ::_thesis: verum end; theorem :: RPR_1:47 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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))) let A, B be Event of E; ::_thesis: ( 0 < prob A & prob B < 1 & A misses B implies prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B))) ) assume that A1: 0 < prob A and A2: prob B < 1 and A3: A misses B ; ::_thesis: prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob 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 prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B))) by A1, A2, A3, Th46; ::_thesis: verum end; theorem :: RPR_1:48 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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) let A, B, C be Event of E; ::_thesis: ( 0 < prob (B /\ C) & 0 < prob C implies prob ((A /\ B) /\ C) = ((prob (A,(B /\ C))) * (prob (B,C))) * (prob C) ) assume that A1: 0 < prob (B /\ C) and A2: 0 < prob C ; ::_thesis: prob ((A /\ B) /\ C) = ((prob (A,(B /\ C))) * (prob (B,C))) * (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 prob ((A /\ B) /\ C) = ((prob (A,(B /\ C))) * (prob (B,C))) * (prob C) by A3; ::_thesis: verum end; theorem Th49: :: RPR_1:49 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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 `))) let A, B be Event of E; ::_thesis: ( 0 < prob B & prob B < 1 implies prob A = ((prob (A,B)) * (prob B)) + ((prob (A,(B `))) * (prob (B `))) ) assume that A1: 0 < prob B and A2: prob B < 1 ; ::_thesis: prob A = ((prob (A,B)) * (prob B)) + ((prob (A,(B `))) * (prob (B `))) (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 prob A = ((prob (A,B)) * (prob B)) + ((prob (A,(B `))) * (prob (B `))) by A3, XCMPLX_1:87; ::_thesis: verum end; theorem Th50: :: RPR_1:50 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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)) let A, B1, B2 be Event of E; ::_thesis: ( 0 < prob B1 & 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 implies prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) ) assume that A1: 0 < prob B1 and A2: 0 < prob B2 and A3: B1 \/ B2 = E and A4: B1 misses B2 ; ::_thesis: prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob 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 prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) by A1, A6, Th49; ::_thesis: verum end; theorem Th51: :: RPR_1:51 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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)) let A, B1, B2, B3 be Event of E; ::_thesis: ( 0 < prob B1 & 0 < prob B2 & 0 < prob B3 & (B1 \/ B2) \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 implies prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)) ) 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 = {} ; :: according to XBOOLE_0:def_7 ::_thesis: prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)) (B1 /\ B3) \/ (B2 /\ B3) = B2 /\ B3 by A6; then (B1 \/ B2) /\ B3 = {} by A7, XBOOLE_1:23; then A8: B1 \/ B2 misses B3 by XBOOLE_0:def_7; ((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, XBOOLE_0:def_7; 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 prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)) by A3, XCMPLX_1:87; ::_thesis: verum end; theorem :: RPR_1:52 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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))) let A, B1, B2 be Event of E; ::_thesis: ( 0 < prob B1 & 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 implies prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) ) assume that A1: 0 < prob B1 and A2: ( 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 ) ; ::_thesis: prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) by A1, A2, Th50; hence prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) by A1, XCMPLX_1:87; ::_thesis: verum end; theorem :: RPR_1:53 for E being non empty finite set for 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 non empty finite set ; ::_thesis: for 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))) let A, B1, B2, B3 be Event of E; ::_thesis: ( 0 < prob B1 & 0 < prob B2 & 0 < prob B3 & (B1 \/ B2) \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 implies prob (B1,A) = ((prob (A,B1)) * (prob B1)) / ((((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3))) ) 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 ) ; ::_thesis: prob (B1,A) = ((prob (A,B1)) * (prob B1)) / ((((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3))) prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)) by A1, A2, Th51; hence prob (B1,A) = ((prob (A,B1)) * (prob B1)) / ((((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3))) by A1, XCMPLX_1:87; ::_thesis: verum end; definition let E be finite set ; let A, B be Event of E; predA,B are_independent means :Def3: :: RPR_1:def 3 prob (A /\ B) = (prob A) * (prob B); symmetry for A, B being Event of E st prob (A /\ B) = (prob A) * (prob B) holds prob (B /\ A) = (prob B) * (prob A) ; end; :: deftheorem Def3 defines are_independent RPR_1:def_3_:_ for E being finite set for A, B being Event of E holds ( A,B are_independent iff prob (A /\ B) = (prob A) * (prob B) ); theorem :: RPR_1:54 for E being non empty finite set for A, B being Event of E st 0 < prob B & A,B are_independent holds prob (A,B) = prob A proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & A,B are_independent holds prob (A,B) = prob A let A, B be Event of E; ::_thesis: ( 0 < prob B & A,B are_independent implies prob (A,B) = prob A ) assume that A1: 0 < prob B and A2: A,B are_independent ; ::_thesis: prob (A,B) = prob A prob (A /\ B) = (prob A) * (prob B) by A2, Def3; 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 prob (A,B) = prob A ; ::_thesis: verum end; theorem :: RPR_1:55 for E being non empty finite set for A, B being Event of E st prob B = 0 holds A,B are_independent proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st prob B = 0 holds A,B are_independent let A, B be Event of E; ::_thesis: ( prob B = 0 implies A,B are_independent ) A1: 0 = (prob A) * 0 ; assume A2: prob B = 0 ; ::_thesis: A,B are_independent then prob (A /\ B) <= 0 by Th19, XBOOLE_1:17; then prob (A /\ B) = 0 by Th18; hence A,B are_independent by A2, A1, Def3; ::_thesis: verum end; theorem :: RPR_1:56 for E being non empty finite set for A, B being Event of E st A,B are_independent holds A ` ,B are_independent proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st A,B are_independent holds A ` ,B are_independent let A, B be Event of E; ::_thesis: ( A,B are_independent implies A ` ,B are_independent ) 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 ; ::_thesis: A ` ,B are_independent then prob ((A `) /\ B) = (1 * (prob B)) - ((prob A) * (prob B)) by A1, Def3; then prob ((A `) /\ B) = (1 - (prob A)) * (prob B) ; then prob ((A `) /\ B) = (prob (A `)) * (prob B) by Th22; hence A ` ,B are_independent by Def3; ::_thesis: verum end; theorem :: RPR_1:57 for E being non empty finite set for A, B being Event of E st A misses B & A,B are_independent & not prob A = 0 holds prob B = 0 proof let E be non empty finite set ; ::_thesis: for A, B being Event of E st A misses B & A,B are_independent & not prob A = 0 holds prob B = 0 let A, B be Event of E; ::_thesis: ( A misses B & A,B are_independent & not prob A = 0 implies prob B = 0 ) assume that A1: A misses B and A2: A,B are_independent ; ::_thesis: ( prob A = 0 or prob B = 0 ) prob (A /\ B) = 0 by A1, Th16; then (prob A) * (prob B) = 0 by A2, Def3; hence ( prob A = 0 or prob B = 0 ) by XCMPLX_1:6; ::_thesis: verum end;