:: by Jan Popio{\l}ek

::

:: Received June 13, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

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 ) ) )

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

registration
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 = {} )

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 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 ) )

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

theorem :: RPR_1:5

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} )

for e being Singleton of E ex a being Element of E st

( a in E & e = {a} )

proof 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 )

for e being Singleton of E ex p being FinSequence st

( p is FinSequence of E & rng p = e & len p = 1 )

proof 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 )

for e being Singleton of E

for A being Event of E holds

( e misses A or e /\ A = e )

proof 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

for A being Event of E st A <> {} holds

ex e being Singleton of E st e c= A

proof 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 ` )

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

Lm1: for E being non empty finite set holds 0 < card E

proof end;

definition
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);

for E being finite set

for A being Event of E holds prob A = (card A) / (card E);

theorem :: RPR_1:14

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))

for A, B being Event of E holds prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B))

proof 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)

for A, B being Event of E st A misses B holds

prob (A \/ B) = (prob A) + (prob B)

proof 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) )

for A being Event of E holds

( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) )

proof 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))

for A, B being Event of E holds prob (A \ B) = (prob A) - (prob (A /\ B))

proof 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)

for A, B being Event of E st B c= A holds

prob (A \ B) = (prob A) - (prob B)

proof 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)

for A, B being Event of E holds prob (A \/ B) <= (prob A) + (prob B)

proof 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 `)))

for A, B being Event of E holds prob A = (prob (A /\ B)) + (prob (A /\ (B `)))

proof 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))

for A, B being Event of E holds prob A = (prob (A \/ B)) - (prob (B \ A))

proof 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))

for A, B being Event of E holds (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A))

proof 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))

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 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)

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 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)

for A, B being Event of E holds (prob A) - (prob B) <= prob (A \ B)

proof end;

definition
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);

for E being finite set

for B, A being Event of E holds prob (A,B) = (prob (A /\ B)) / (prob B);

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))

for A, B being Event of E st 0 < prob B holds

prob (A,B) = 1 - ((prob (B \ A)) / (prob B))

proof 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)

for A, B being Event of E st 0 < prob B & A c= B holds

prob (A,B) = (prob A) / (prob B)

proof 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))

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 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)) )

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

for A, B being Event of E st 0 < prob B & B c= A holds

prob (A,B) = 1

proof end;

theorem :: RPR_1:42

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

for A, B being Event of E st 0 < prob B & A misses B holds

prob ((A `),B) = 1

proof 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))

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 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)))

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 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)

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 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 `)))

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 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))

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 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))

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 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)))

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 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)))

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

definition

let E be finite set ;

let A, B be Event of E;

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;
let A, B be Event of E;

symmetry

for A, B being Event of E st prob (A /\ B) = (prob A) * (prob B) holds

prob (B /\ A) = (prob B) * (prob A) ;

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

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

for A, B being Event of E st 0 < prob B & A,B are_independent holds

prob (A,B) = prob A

proof 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

for A, B being Event of E st A,B are_independent holds

A ` ,B are_independent

proof 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

for A, B being Event of E st A misses B & A,B are_independent & not prob A = 0 holds

prob B = 0

proof end;