:: PROB_2 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem :: PROB_2:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: PROB_2:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: PROB_2:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th4: :: PROB_2:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th6: :: PROB_2:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines @Intersection PROB_2:def 1 :
theorem :: PROB_2:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: PROB_2:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th9: :: PROB_2:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: PROB_2:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th11: :: PROB_2:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: PROB_2:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: PROB_2:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
Omega being non
empty set for
ASeq,
BSeq being
SetSequence of
Omega st ( for
n being
Nat holds
ASeq . n = BSeq . n ) holds
ASeq = BSeq
theorem Th17: :: PROB_2:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm1:
for Omega being non empty set
for ASeq being SetSequence of Omega holds
( ASeq is non-decreasing iff Complement ASeq is non-increasing )
:: 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-decreasing holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )
theorem :: PROB_2:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: PROB_2:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: PROB_2:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th22: :: PROB_2:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th23: :: PROB_2:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th24: :: PROB_2:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th25: :: PROB_2:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th26: :: PROB_2:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th27: :: PROB_2:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def5 defines are_independent_respect_to PROB_2:def 5 :
:: deftheorem Def6 defines are_independent_respect_to PROB_2:def 6 :
Lm3:
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st A,B are_independent_respect_to P holds
B,A are_independent_respect_to P
theorem :: PROB_2:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: PROB_2:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: PROB_2:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th32: :: PROB_2:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th37: :: PROB_2:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th38: :: PROB_2:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def7 defines .|. PROB_2:def 7 :
theorem :: PROB_2:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th42: :: PROB_2:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th44: :: PROB_2:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th45: :: PROB_2:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th49: :: PROB_2:49
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:50
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:51
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: PROB_2:52
:: Showing IDV graph ... (Click the Palm Tree again to close it) 