:: 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;