:: Introduction to Probability
:: by Jan Popio{\l}ek
::
:: Received June 13, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: RPR_1:1
theorem :: RPR_1:2
canceled;
theorem :: RPR_1:3
canceled;
theorem :: RPR_1:4
canceled;
theorem :: RPR_1:5
theorem :: RPR_1:6
for
E being non
empty set for
A,
B being
Subset of
E for
e being
El_ev of
E holds
( not
e = A \/ B or (
A = e &
B = e ) or (
A = e &
B = {} ) or (
A = {} &
B = e ) )
theorem Th7: :: RPR_1:7
theorem :: RPR_1:8
canceled;
theorem :: RPR_1:9
canceled;
theorem :: RPR_1:10
theorem Th11: :: RPR_1:11
theorem :: RPR_1:12
theorem :: RPR_1:13
canceled;
theorem :: RPR_1:14
theorem :: RPR_1:15
canceled;
theorem :: RPR_1:16
canceled;
theorem :: RPR_1:17
canceled;
theorem :: RPR_1:18
canceled;
theorem :: RPR_1:19
canceled;
theorem :: RPR_1:20
canceled;
theorem :: RPR_1:21
canceled;
theorem :: RPR_1:22
theorem :: RPR_1:23
canceled;
theorem :: RPR_1:24
canceled;
theorem :: RPR_1:25
theorem :: RPR_1:26
theorem :: RPR_1:27
theorem :: RPR_1:28
canceled;
theorem :: RPR_1:29
canceled;
theorem :: RPR_1:30
canceled;
theorem :: RPR_1:31
canceled;
theorem :: RPR_1:32
canceled;
theorem :: RPR_1:33
canceled;
theorem Th34: :: RPR_1:34
Lm1:
for E being non empty finite set holds 0 < card E
Lm2:
for E being non empty set
for e being El_ev of E holds card e = 1
:: deftheorem RPR_1:def 1 :
canceled;
:: deftheorem RPR_1:def 2 :
canceled;
:: deftheorem RPR_1:def 3 :
canceled;
:: deftheorem defines prob RPR_1:def 4 :
theorem :: RPR_1:35
canceled;
theorem :: RPR_1:36
canceled;
theorem :: RPR_1:37
canceled;
theorem :: RPR_1:38
theorem Th39: :: RPR_1:39
theorem :: RPR_1:40
canceled;
theorem Th41: :: RPR_1:41
theorem :: RPR_1:42
theorem Th43: :: RPR_1:43
theorem Th44: :: RPR_1:44
theorem :: RPR_1:45
canceled;
theorem Th46: :: RPR_1:46
theorem Th47: :: RPR_1:47
theorem Th48: :: RPR_1:48
theorem Th49: :: RPR_1:49
theorem Th50: :: RPR_1:50
theorem :: RPR_1:51
theorem :: RPR_1:52
canceled;
theorem Th53: :: RPR_1:53
theorem :: RPR_1:54
theorem :: RPR_1:55
theorem Th56: :: RPR_1:56
theorem :: RPR_1:57
theorem :: RPR_1:58
:: deftheorem defines prob RPR_1:def 5 :
theorem :: RPR_1:59
canceled;
theorem :: RPR_1:60
canceled;
theorem :: RPR_1:61
theorem :: RPR_1:62
theorem :: RPR_1:63
canceled;
theorem :: RPR_1:64
theorem :: RPR_1:65
theorem Th66: :: RPR_1:66
theorem :: RPR_1:67
theorem Th68: :: RPR_1:68
theorem Th69: :: RPR_1:69
theorem Th70: :: RPR_1:70
theorem Th71: :: RPR_1:71
theorem :: RPR_1:72
theorem :: RPR_1:73
theorem :: RPR_1:74
theorem Th75: :: RPR_1:75
theorem Th76: :: RPR_1:76
theorem :: RPR_1:77
theorem :: RPR_1:78
theorem Th79: :: RPR_1:79
theorem Th80: :: RPR_1:80
theorem Th81: :: RPR_1:81
theorem :: RPR_1:82
theorem :: RPR_1:83
:: deftheorem Def6 defines are_independent RPR_1:def 6 :
theorem :: RPR_1:84
canceled;
theorem :: RPR_1:85
canceled;
theorem :: RPR_1:86
theorem :: RPR_1:87
theorem :: RPR_1:88
theorem :: RPR_1:89