The abstract of the Mizar article:

Introduction to Probability

by

Jan Popiolek

Received June 13, 1990

MML identifier: RPR_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, FINSET_1, BOOLE, RELAT_1, PROB_1, SUBSET_1, CARD_1,
      ARYTM_3, ARYTM_1, RPR_1, REALSET1;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, FUNCT_1, DOMAIN_1, REAL_1,
      FINSEQ_1, FINSET_1, CARD_1, REALSET1;
 constructors DOMAIN_1, REAL_1, NAT_1, REALSET1, XREAL_0, MEMBERED, XBOOLE_0;
 clusters FINSET_1, RELSET_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

 reserve E for non empty set;
 reserve a for Element of E;
 reserve A, B for Subset of E;
 reserve Y for set;
 reserve p for FinSequence;

definition let E be non empty set;
  cluster non empty trivial Subset of E;
end;

definition let E;
  mode El_ev of E is non empty trivial Subset of E;
end;

theorem :: RPR_1:1
  for e being non empty Subset of E holds
  e is El_ev of E iff for Y holds (Y c= e iff Y = {} or Y = e);

definition let E;
  cluster -> finite El_ev of E;
end;

 reserve e, e1, e2 for El_ev of E;

canceled 3;

theorem :: RPR_1:5
    e = A \/ B & A <> B implies
  A = {} & B = e or A = e & B = {};

theorem :: RPR_1:6
    e = A \/ B implies A = e & B = e or
  A = e & B = {} or A = {} & B = e;

theorem :: RPR_1:7
  {a} is El_ev of E;

canceled 2;

theorem :: RPR_1:10
   e1 c= e2 implies e1 = e2;

theorem :: RPR_1:11
  ex a st a in E & e = {a};

theorem :: RPR_1:12
    ex e st e is El_ev of E;

canceled;

theorem :: RPR_1:14
    ex p st p is FinSequence of E & rng p = e & len p = 1;

definition let E be set;
  mode Event of E is Subset of E;
end;

canceled 7;

theorem :: RPR_1:22
    for E being non empty set, e being El_ev of E, A being Event of E
   holds e misses A or e /\ A = e;

canceled 2;

theorem :: RPR_1:25
    for E being non empty set, A being Event of E st A <> {}
       ex e being El_ev of E st e c= A;

theorem :: RPR_1:26
    for E being non empty set, e being El_ev of E, A being Event of E
   st e c= A \/ A` holds e c= A or e c= A`;

theorem :: RPR_1:27
    e1 = e2 or e1 misses e2;

canceled 6;

theorem :: RPR_1:34
  A /\ B misses A /\ B`;

definition
  let E be finite non empty set;
  let A be Event of E;
 canceled 3;

  func prob(A) -> Real equals
:: RPR_1:def 4
     card A / card E;
end;

canceled 3;

theorem :: RPR_1:38
    for E being finite non empty set, e being El_ev of E holds
  prob(e) = 1 / card E;

theorem :: RPR_1:39
  for E being finite non empty set holds prob([#] E) = 1;

theorem :: RPR_1:40
  for E being finite non empty set holds prob({} E) = 0;

theorem :: RPR_1:41
  for E being finite non empty set, A,B being Event of E st A misses B
    holds prob(A /\ B) = 0;

theorem :: RPR_1:42
    for E being finite non empty set, A being Event of E holds prob(A) <= 1;

theorem :: RPR_1:43
  for E being finite non empty set, A being Event of E holds 0 <= prob(A);

theorem :: RPR_1:44
 for E being finite non empty set, A,B being Event of E st A c= B holds
    prob(A) <= prob(B);

canceled;

theorem :: RPR_1:46
 for E being finite non empty set, A,B being Event of E holds
    prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B);

theorem :: RPR_1:47
 for E being finite non empty set, A,B being Event of E st A misses B
   holds prob(A \/ B) = prob(A) + prob(B);

theorem :: RPR_1:48
 for E being finite non empty set, A being Event of E holds
     prob(A) = 1 - prob(A`) & prob(A`) = 1 - prob(A);

theorem :: RPR_1:49
 for E being finite non empty set, A,B being Event of E holds
     prob(A \ B) = prob(A) - prob(A /\ B);

theorem :: RPR_1:50
 for E being finite non empty set, A,B being Event of E st B c= A holds
     prob(A \ B) = prob(A) - prob(B);

theorem :: RPR_1:51
   for E being finite non empty set, A,B being Event of E holds
     prob(A \/ B) <= prob(A) + prob(B);

canceled;

theorem :: RPR_1:53
 for E being finite non empty set, A,B being Event of E holds
     prob(A) = prob(A /\ B) + prob(A /\ B`);

theorem :: RPR_1:54
   for E being finite non empty set, A,B being Event of E holds
     prob(A) = prob(A \/ B) - prob(B \ A);

theorem :: RPR_1:55
   for E being finite non empty set, A,B being Event of E holds
     prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A);

theorem :: RPR_1:56
 for E being finite non empty set, A,B,C being Event of E
   holds prob(A \/ B \/ C) = ( prob(A) + prob(B) + prob(C) ) -
     ( prob(A /\ B) + prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C);

theorem :: RPR_1:57
    for E being finite non empty set, A,B,C being Event of E st
     A misses B & A misses C & B misses C
     holds prob(A \/ B \/ C) = prob(A) + prob(B) + prob(C);

theorem :: RPR_1:58
    for E being finite non empty set, A,B being Event of E holds
     prob(A) - prob(B) <= prob(A \ B);

definition
  let E be finite non empty set;
  let B,A be Event of E;
  func prob(A , B) -> Real equals
:: RPR_1:def 5
   prob(A /\ B) / prob(B);
end;

canceled;

theorem :: RPR_1:60
  for E being finite non empty set, A,B being Event of E st 0 < prob(B)
    holds prob(A /\ B) = prob(A , B) * prob(B);

theorem :: RPR_1:61
  for E being finite non empty set, A being Event of E holds
    prob(A , [#] E ) = prob(A);

theorem :: RPR_1:62
    for E being finite non empty set holds prob([#] E , [#] E) = 1;

theorem :: RPR_1:63
   for E being finite non empty set holds prob({} E , [#] E) = 0;

theorem :: RPR_1:64
   for E being finite non empty set, A,B being Event of E st 0 < prob(B)
   holds prob(A , B) <= 1;

theorem :: RPR_1:65
    for E being finite non empty set, A,B being Event of E st 0 < prob(B)
   holds 0 <= prob(A , B);

theorem :: RPR_1:66
  for E being finite non empty set, A,B being Event of E st 0 < prob(B)
   holds prob(A , B) = 1 - prob(B \ A) / prob(B);

theorem :: RPR_1:67
    for E being finite non empty set, A,B being Event of E st 0 < prob(B)
    & A c= B holds prob(A , B) = prob(A) / prob(B);

theorem :: RPR_1:68
  for E being finite non empty set, A,B being Event of E st
      A misses B holds prob(A , B) = 0;

theorem :: RPR_1:69
 for E being finite non empty set, A,B being Event of E st 0 < prob(A) &
     0 < prob(B) holds prob(A) * prob(B , A) = prob(B) * prob(A , B);

theorem :: RPR_1:70
  for E being finite non empty set, A,B being Event of E st 0 < prob B
    holds prob(A , B) = 1 - prob(A` , B) & prob(A` , B) = 1 - prob(A , B);

theorem :: RPR_1:71
  for E being finite non empty set, A,B being Event of E st 0 < prob(B) &
     B c= A holds prob(A , B) = 1;

theorem :: RPR_1:72
    for E being finite non empty set, B being Event of E st 0 < prob(B)
   holds prob([#] E , B) = 1;

theorem :: RPR_1:73
    for E being finite non empty set, A being Event of E st 0 < prob(A)
    holds prob(A` , A) = 0;

theorem :: RPR_1:74
    for E being finite non empty set, A being Event of E st prob(A) < 1
    holds prob(A , A`) = 0;

theorem :: RPR_1:75
  for E being finite non empty set, A,B being Event of E st 0 < prob(B) &
     A misses B holds prob(A` , B) = 1;

theorem :: RPR_1:76
  for E being finite non empty set, A,B being Event of E st 0 < prob(A) &
     prob(B) < 1 & A misses B holds
     prob(A , B`) = prob(A) / (1 - prob(B));

theorem :: RPR_1:77
    for E being finite non empty set, A,B being Event of E st 0 < prob(A) &
     prob(B) < 1 & A misses B holds
     prob(A` , B`) = 1 - prob(A) / (1 - prob(B));

theorem :: RPR_1:78
    for E being finite non empty set, A,B,C being Event of E st
    0 < prob(B /\ C) & 0 < prob(C) holds
    prob(A /\ B /\ C) = prob(A , B /\ C) * prob(B , C) * prob(C);

theorem :: RPR_1:79
  for E being finite non empty set, A,B being Event of E
     st 0 < prob(B) & prob(B) < 1 holds
     prob(A) = prob(A , B) * prob(B) + prob(A , B`) * prob(B`);

theorem :: RPR_1:80
  for E being finite non empty set, A,B1,B2 being Event of E
    st 0 < prob(B1) & 0 < prob(B2) & B1 \/ B2 = E & B1 misses B2 holds
     prob(A) = prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2);

theorem :: RPR_1:81
 for E being finite non empty set, A,B1,B2,B3 being Event of E
   st 0 < prob(B1) & 0 < prob(B2) & 0 < prob(B3) &
     B1 \/ B2 \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds
     prob(A) = ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ) +
     prob(A , B3) * prob(B3);

theorem :: RPR_1:82
    for E being finite non empty set, A,B1,B2 being Event of E
   st 0 < prob(B1) & 0 < prob(B2) & B1 \/ B2 = E &
     B1 misses B2 holds prob(B1 , A) = ( prob(A , B1) * prob(B1) ) /
     ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) );

theorem :: RPR_1:83
    for E being finite non empty set, A,B1,B2,B3 being Event of E
   st 0 < prob(B1) & 0 < prob(B2)
     & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2 & B1 misses B3 &
     B2 misses B3 holds prob(B1 , A) = ( prob(A , B1) * prob(B1) ) /
     ( ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) )
     + prob(A , B3) * prob(B3) );

definition
  let E be finite non empty set;
  let A, B be Event of E;
  pred A, B are_independent means
:: RPR_1:def 6
  prob(A /\ B) = prob(A) * prob(B);
  symmetry;
end;

canceled 2;

theorem :: RPR_1:86
    for E being finite non empty set, A,B being Event of E st 0 < prob(B)
    & A, B are_independent holds prob(A , B) = prob(A);

theorem :: RPR_1:87
   for E being finite non empty set, A,B being Event of E st
     prob(B) = 0 holds A , B are_independent;

theorem :: RPR_1:88
    for E being finite non empty set, A,B being Event of E st
     A , B are_independent holds A` , B are_independent;

theorem :: RPR_1:89
    for E being finite non empty set, A,B being Event of E st A misses B
     & A, B are_independent holds prob(A) = 0 or prob(B) = 0;