begin
theorem Th1:
theorem
theorem
theorem
theorem
theorem Th11:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th34:
Lm1:
for E being non empty finite set holds 0 < card E
:: deftheorem defines prob RPR_1:def 1 :
for E being non empty finite set
for A being Event of E holds prob A = (card A) / (card E);
theorem
theorem Th39:
theorem Th41:
theorem
theorem Th43:
theorem Th44:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem Th53:
theorem
theorem
theorem Th56:
theorem
theorem
:: deftheorem defines prob RPR_1:def 2 :
for E being non empty finite set
for B, A being Event of E holds prob (A,B) = (prob (A /\ B)) / (prob B);
theorem
theorem
theorem
theorem
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem
theorem
theorem
theorem Th75:
theorem Th76:
theorem
theorem
theorem Th79:
theorem Th80:
theorem Th81:
theorem
theorem
:: deftheorem Def6 defines are_independent RPR_1:def 3 :
for E being non empty finite set
for A, B being Event of E holds
( A,B are_independent iff prob (A /\ B) = (prob A) * (prob B) );
theorem
theorem
theorem
theorem