:: Probability. Independence of Events and Conditional Probability
:: by Andrzej N\c{e}dzusiak
::
:: Received June 1, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: PROB_2:1
canceled;
theorem :: PROB_2:2
canceled;
theorem :: PROB_2:3
canceled;
theorem Th4: :: PROB_2:4
for
r,
r1,
r2,
r3 being
Real st
r <> 0 &
r1 <> 0 holds
(
r3 / r1 = r2 / r iff
r3 * r = r2 * r1 )
theorem Th5: :: PROB_2:5
:: deftheorem defines @Intersection PROB_2:def 1 :
theorem :: PROB_2:6
canceled;
theorem :: PROB_2:7
canceled;
theorem :: PROB_2:8
canceled;
theorem Th9: :: PROB_2:9
theorem Th10: :: PROB_2:10
theorem :: PROB_2:11
canceled;
theorem Th12: :: PROB_2:12
theorem Th13: :: PROB_2:13
theorem :: PROB_2:14
theorem :: PROB_2:15
theorem :: PROB_2:16
canceled;
theorem Th17: :: PROB_2:17
Lm1:
for Omega being non empty set
for ASeq being SetSequence of Omega holds
( ASeq is non-descending iff Complement ASeq is non-ascending )
:: deftheorem defines @Complement PROB_2:def 2 :
:: deftheorem Def3 defines disjoint_valued PROB_2:def 3 :
:: deftheorem defines disjoint_valued PROB_2:def 4 :
Lm2:
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )
theorem :: PROB_2:18
canceled;
theorem :: PROB_2:19
canceled;
theorem :: PROB_2:20
theorem :: PROB_2:21
theorem :: PROB_2:22
theorem :: PROB_2:23
theorem Th24: :: PROB_2:24
theorem Th25: :: PROB_2:25
theorem Th26: :: PROB_2:26
theorem Th27: :: PROB_2:27
theorem :: PROB_2:28
:: deftheorem Def5 defines are_independent_respect_to PROB_2:def 5 :
:: deftheorem Def6 defines are_independent_respect_to PROB_2:def 6 :
theorem :: PROB_2:29
canceled;
theorem :: PROB_2:30
canceled;
theorem Th31: :: PROB_2:31
theorem Th32: :: PROB_2:32
theorem :: PROB_2:33
theorem :: PROB_2:34
theorem :: PROB_2:35
theorem :: PROB_2:36
theorem Th37: :: PROB_2:37
theorem Th38: :: PROB_2:38
theorem :: PROB_2:39
theorem :: PROB_2:40
:: deftheorem Def7 defines .|. PROB_2:def 7 :
theorem :: PROB_2:41
canceled;
theorem Th42: :: PROB_2:42
theorem :: PROB_2:43
theorem Th44: :: PROB_2:44
theorem Th45: :: PROB_2:45
theorem :: PROB_2:46
theorem :: PROB_2:47
theorem :: PROB_2:48
theorem Th49: :: PROB_2:49
theorem :: PROB_2:50
theorem :: PROB_2:51
theorem :: PROB_2:52