begin
theorem
canceled;
theorem
canceled;
theorem Th3:
:: deftheorem Def1 defines compl-closed PROB_1:def 1 :
for X being set
for IT being Subset-Family of X holds
( IT is compl-closed iff for A being Subset of X st A in IT holds
A ` in IT );
theorem Th4:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th23:
theorem
canceled;
theorem Th25:
theorem Th26:
:: deftheorem PROB_1:def 2 :
canceled;
:: deftheorem PROB_1:def 3 :
canceled;
:: deftheorem Def4 defines Complement PROB_1:def 4 :
for X being set
for A1, b3 being SetSequence of X holds
( b3 = Complement A1 iff for n being Element of NAT holds b3 . n = (A1 . n) ` );
:: deftheorem defines Intersection PROB_1:def 5 :
for X being set
for A1 being SetSequence of X holds Intersection A1 = (Union (Complement A1)) ` ;
theorem
canceled;
theorem
canceled;
theorem Th29:
Lm2:
for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)
theorem Th30:
:: deftheorem Def6 defines non-ascending PROB_1:def 6 :
for f being Function holds
( f is non-ascending iff for n, m being Element of NAT st n <= m holds
f . m c= f . n );
:: deftheorem defines non-descending PROB_1:def 7 :
for f being Function holds
( f is non-descending iff for n, m being Element of NAT st n <= m holds
f . n c= f . m );
:: deftheorem Def8 defines sigma-multiplicative PROB_1:def 8 :
for X being set
for F being Subset-Family of X holds
( F is sigma-multiplicative iff for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F );
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem Th35:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th46:
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem PROB_1:def 9 :
canceled;
:: deftheorem PROB_1:def 10 :
canceled;
:: deftheorem defines [#] PROB_1:def 11 :
for X being set
for Si being SigmaField of X holds [#] Si = X;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th59:
theorem Th60:
theorem
canceled;
theorem Th62:
:: deftheorem PROB_1:def 12 :
canceled;
:: deftheorem Def13 defines Probability PROB_1:def 13 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for b3 being Function of Sigma,REAL holds
( b3 is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= b3 . A ) & b3 . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
b3 . (A \/ B) = (b3 . A) + (b3 . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b3 * ASeq is convergent & lim (b3 * ASeq) = b3 . (Intersection ASeq) ) ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th67:
theorem
theorem Th69:
theorem Th70:
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem
theorem
Lm3:
for Omega being non empty set
for X being Subset-Family of Omega ex Y being SigmaField of Omega st
( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z ) )
:: deftheorem defines sigma PROB_1:def 14 :
for Omega being non empty set
for X being Subset-Family of Omega
for b3 being SigmaField of Omega holds
( b3 = sigma X iff ( X c= b3 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b3 c= Z ) ) );
:: deftheorem defines halfline PROB_1:def 15 :
for r being ext-real number holds halfline r = ].-infty,r.[;
:: deftheorem defines Family_of_halflines PROB_1:def 16 :
Family_of_halflines = { (halfline r) where r is Element of REAL : verum } ;
:: deftheorem defines Borel_Sets PROB_1:def 17 :
Borel_Sets = sigma Family_of_halflines;
theorem