begin
Lm1:
for A, B, C being set st C c= B holds
A \ C = (A \ B) \/ (A /\ (B \ C))
theorem Th1:
theorem Th2:
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
:: deftheorem defines P2M PROB_4:def 1 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P2M P = P;
theorem Th15:
:: deftheorem defines M2P PROB_4:def 2 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st M . X = R_EAL 1 holds
M2P M = M;
Lm2:
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds (Partial_Union A1) . n = A1 . n
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem
theorem
theorem
:: deftheorem Def3 defines is_complete PROB_4:def 3 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds
( P is_complete Sigma iff for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma );
theorem
:: deftheorem Def4 defines thin PROB_4:def 4 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being Subset of Omega holds
( b4 is thin of P iff ex A being set st
( A in Sigma & b4 c= A & P . A = 0 ) );
theorem Th24:
theorem Th25:
theorem Th26:
:: deftheorem Def5 defines COM PROB_4:def 5 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being non empty Subset-Family of Omega holds
( b4 = COM Sigma,P iff for A being set holds
( A in b4 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) );
theorem Th27:
theorem Th28:
:: deftheorem defines P_COM2M_COM PROB_4:def 6 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM Sigma,P holds P_COM2M_COM A = A;
theorem Th29:
:: deftheorem Def7 defines ProbPart PROB_4:def 7 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM Sigma,P
for b5 being non empty Subset-Family of Omega holds
( b5 = ProbPart A iff for B being set holds
( B in b5 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) );
theorem
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
:: deftheorem Def8 defines COM PROB_4:def 8 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being Probability of COM Sigma,P holds
( b4 = COM P iff for B being set st B in Sigma holds
for C being thin of P holds b4 . (B \/ C) = P . B );
theorem
theorem
theorem Th40:
theorem Th41:
theorem