:: $\sigma$-Fields and Probability
:: by Andrzej N\c{e}dzusiak
::
:: Received October 16, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: PROB_1:1
canceled;
theorem :: PROB_1:2
canceled;
theorem Th3: :: PROB_1:3
:: deftheorem Def1 defines compl-closed PROB_1:def 1 :
theorem Th4: :: PROB_1:4
theorem :: PROB_1:5
canceled;
theorem Th6: :: PROB_1:6
theorem :: PROB_1:7
canceled;
theorem :: PROB_1:8
canceled;
theorem Th9: :: PROB_1:9
theorem Th10: :: PROB_1:10
theorem Th11: :: PROB_1:11
theorem Th12: :: PROB_1:12
theorem :: PROB_1:13
theorem :: PROB_1:14
theorem :: PROB_1:15
theorem :: PROB_1:16
theorem :: PROB_1:17
canceled;
theorem :: PROB_1:18
Lm1:
for X being set
for A1 being SetSequence of X holds
( dom A1 = NAT & ( for n being Element of NAT holds A1 . n in bool X ) )
by FUNCT_2:def 1;
theorem :: PROB_1:19
canceled;
theorem :: PROB_1:20
canceled;
theorem :: PROB_1:21
canceled;
theorem :: PROB_1:22
canceled;
theorem Th23: :: PROB_1:23
theorem :: PROB_1:24
canceled;
theorem Th25: :: PROB_1:25
theorem Th26: :: PROB_1:26
:: deftheorem PROB_1:def 2 :
canceled;
:: deftheorem PROB_1:def 3 :
canceled;
:: deftheorem Def4 defines Complement PROB_1:def 4 :
:: deftheorem defines Intersection PROB_1:def 5 :
theorem :: PROB_1:27
canceled;
theorem :: PROB_1:28
canceled;
theorem Th29: :: PROB_1:29
Lmx1:
for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A ` ) followed_by (B ` )
theorem Th30: :: PROB_1:30
:: deftheorem Def6 defines non-ascending PROB_1:def 6 :
:: deftheorem defines non-descending PROB_1:def 7 :
:: deftheorem Def8 defines sigma-multiplicative PROB_1:def 8 :
theorem :: PROB_1:31
canceled;
theorem :: PROB_1:32
theorem :: PROB_1:33
canceled;
theorem :: PROB_1:34
canceled;
theorem Th35: :: PROB_1:35
theorem :: PROB_1:36
canceled;
theorem :: PROB_1:37
canceled;
theorem :: PROB_1:38
theorem :: PROB_1:39
canceled;
theorem :: PROB_1:40
canceled;
theorem :: PROB_1:41
theorem :: PROB_1:42
theorem :: PROB_1:43
theorem :: PROB_1:44
:: deftheorem Def9 defines SetSequence PROB_1:def 9 :
theorem :: PROB_1:45
canceled;
theorem Th46: :: PROB_1:46
theorem :: PROB_1:47
canceled;
theorem :: PROB_1:48
theorem :: PROB_1:49
theorem :: PROB_1:50
theorem :: PROB_1:51
theorem :: PROB_1:52
theorem :: PROB_1:53
theorem :: PROB_1:54
:: deftheorem PROB_1:def 10 :
canceled;
:: deftheorem defines [#] PROB_1:def 11 :
theorem :: PROB_1:55
canceled;
theorem :: PROB_1:56
canceled;
theorem :: PROB_1:57
theorem :: PROB_1:58
theorem Th59: :: PROB_1:59
theorem Th60: :: PROB_1:60
theorem :: PROB_1:61
canceled;
theorem Th62: :: PROB_1:62
:: deftheorem PROB_1:def 12 :
canceled;
:: deftheorem Def13 defines Probability PROB_1:def 13 :
theorem :: PROB_1:63
canceled;
theorem :: PROB_1:64
canceled;
theorem :: PROB_1:65
canceled;
theorem :: PROB_1:66
theorem Th67: :: PROB_1:67
theorem :: PROB_1:68
theorem Th69: :: PROB_1:69
theorem Th70: :: PROB_1:70
theorem :: PROB_1:71
theorem Th72: :: PROB_1:72
theorem Th73: :: PROB_1:73
theorem Th74: :: PROB_1:74
theorem :: PROB_1:75
theorem Th76: :: PROB_1:76
Lm2:
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 :
:: deftheorem defines halfline PROB_1:def 15 :
:: deftheorem defines Family_of_halflines PROB_1:def 16 :
:: deftheorem defines Borel_Sets PROB_1:def 17 :
theorem :: PROB_1:77