:: RPR_1 semantic presentation

registration

let c₁ be non empty set ;
cluster non empty trivial Element of K16(a₁);
existence

proof end;

end;

definition

let c₁ be non empty set ;
mode El_ev of a₁ is non empty trivial Subset of a₁;

end;

theorem Th1: :: RPR_1:1

for b₁ being non empty set
for b₂ being non empty Subset of b₁ holds
( b₂ is El_ev of b₁ iff for b₃ being set holds
( b₃ c= b₂ iff ( b₃ = {} or b₃ = b₂ ) ) )

proof end;

registration

let c₁ be non empty set ;
cluster -> finite Element of K16(a₁);
coherence

proof end;

end;

theorem Th2: :: RPR_1:2

canceled;

theorem Th3: :: RPR_1:3

canceled;

theorem Th4: :: RPR_1:4

canceled;

theorem Th5: :: RPR_1:5

for b₁ being non empty set
for b₂, b₃ being Subset of b₁
for b₄ being El_ev of b₁ st b₄ = b₂ \/ b₃ & b₂ <> b₃ & not ( b₂ = {} & b₃ = b₄ ) holds
( b₂ = b₄ & b₃ = {} )

proof end;

theorem Th6: :: RPR_1:6

for b₁ being non empty set
for b₂, b₃ being Subset of b₁
for b₄ being El_ev of b₁ holds
( not b₄ = b₂ \/ b₃ or ( b₂ = b₄ & b₃ = b₄ ) or ( b₂ = b₄ & b₃ = {} ) or ( b₂ = {} & b₃ = b₄ ) )

proof end;

theorem Th7: :: RPR_1:7

for b₁ being non empty set
for b₂ being Element of b₁ holds {b₂} is El_ev of b₁

proof end;

theorem Th8: :: RPR_1:8

canceled;

theorem Th9: :: RPR_1:9

canceled;

theorem Th10: :: RPR_1:10

for b₁ being non empty set
for b₂, b₃ being El_ev of b₁ st b₂ c= b₃ holds
b₂ = b₃ by Th1;

theorem Th11: :: RPR_1:11

for b₁ being non empty set
for b₂ being El_ev of b₁ ex b₃ being Element of b₁ st
( b₃ in b₁ & b₂ = {b₃} )

proof end;

theorem Th12: :: RPR_1:12

for b₁ being non empty set ex b₂ being El_ev of b₁ st b₂ is El_ev of b₁

proof end;

theorem Th13: :: RPR_1:13

canceled;

theorem Th14: :: RPR_1:14

for b₁ being non empty set
for b₂ being El_ev of b₁ ex b₃ being FinSequence st
( b₃ is FinSequence of b₁ & rng b₃ = b₂ & len b₃ = 1 )

proof end;

definition

let c₁ be set ;
mode Event of a₁ is Subset of a₁;

end;

theorem Th15: :: RPR_1:15

canceled;

theorem Th16: :: RPR_1:16

canceled;

theorem Th17: :: RPR_1:17

canceled;

theorem Th18: :: RPR_1:18

canceled;

theorem Th19: :: RPR_1:19

canceled;

theorem Th20: :: RPR_1:20

canceled;

theorem Th21: :: RPR_1:21

canceled;

theorem Th22: :: RPR_1:22

for b₁ being non empty set
for b₂ being El_ev of b₁
for b₃ being Event of b₁ holds
( b₂ misses b₃ or b₂ /\ b₃ = b₂ )

proof end;

theorem Th23: :: RPR_1:23

canceled;

theorem Th24: :: RPR_1:24

canceled;

theorem Th25: :: RPR_1:25

for b₁ being non empty set
for b₂ being Event of b₁ st b₂ <> {} holds
ex b₃ being El_ev of b₁ st b₃ c= b₂

proof end;

theorem Th26: :: RPR_1:26

for b₁ being non empty set
for b₂ being El_ev of b₁
for b₃ being Event of b₁ holds
( not b₂ c= b₃ \/ (b₃ ` ) or b₂ c= b₃ or b₂ c= b₃ ` )

proof end;

theorem Th27: :: RPR_1:27

for b₁ being non empty set
for b₂, b₃ being El_ev of b₁ holds
( b₂ = b₃ or b₂ misses b₃ )

proof end;

theorem Th28: :: RPR_1:28

canceled;

theorem Th29: :: RPR_1:29

canceled;

theorem Th30: :: RPR_1:30

canceled;

theorem Th31: :: RPR_1:31

canceled;

theorem Th32: :: RPR_1:32

canceled;

theorem Th33: :: RPR_1:33

canceled;

theorem Th34: :: RPR_1:34

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds b₂ /\ b₃ misses b₂ /\ (b₃ ` )

proof end;

Lemma5: for b₁ being non empty finite set holds 0 < card b₁

proof end;

Lemma6: for b₁ being non empty set
for b₂ being El_ev of b₁ holds card b₂ = 1

proof end;

definition

let c₁ be non empty finite set ;
let c₂ be Event of c₁;
canceled;
canceled;
canceled;
func prob c₂ -> Real equals :: RPR_1:def 4
(card a₂) / (card a₁);
coherence ;

end;

:: deftheorem Def1 RPR_1:def 1 :

:: deftheorem Def2 RPR_1:def 2 :

:: deftheorem Def3 RPR_1:def 3 :

:: deftheorem Def4 defines prob RPR_1:def 4 :

theorem Th35: :: RPR_1:35

canceled;

theorem Th36: :: RPR_1:36

canceled;

theorem Th37: :: RPR_1:37

canceled;

theorem Th38: :: RPR_1:38

for b₁ being non empty finite set
for b₂ being El_ev of b₁ holds prob b₂ = 1 / (card b₁) by Lemma6;

theorem Th39: :: RPR_1:39

for b₁ being non empty finite set holds prob ([#] b₁) = 1

proof end;

theorem Th40: :: RPR_1:40

for b₁ being non empty finite set holds prob ({} b₁) = 0 by CARD_1:78;

theorem Th41: :: RPR_1:41

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st b₂ misses b₃ holds
prob (b₂ /\ b₃) = 0

proof end;

theorem Th42: :: RPR_1:42

for b₁ being non empty finite set
for b₂ being Event of b₁ holds prob b₂ <= 1

proof end;

theorem Th43: :: RPR_1:43

for b₁ being non empty finite set
for b₂ being Event of b₁ holds 0 <= prob b₂

proof end;

theorem Th44: :: RPR_1:44

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st b₂ c= b₃ holds
prob b₂ <= prob b₃

proof end;

theorem Th45: :: RPR_1:45

canceled;

theorem Th46: :: RPR_1:46

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ holds prob (b₂ \/ b₃) = ((prob b₂) + (prob b₃)) - (prob (b₂ /\ b₃))

proof end;

theorem Th47: :: RPR_1:47

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st b₂ misses b₃ holds
prob (b₂ \/ b₃) = (prob b₂) + (prob b₃)

proof end;

theorem Th48: :: RPR_1:48

for b₁ being non empty finite set
for b₂ being Event of b₁ holds
( prob b₂ = 1 - (prob (b₂ ` )) & prob (b₂ ` ) = 1 - (prob b₂) )

proof end;

theorem Th49: :: RPR_1:49

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ holds prob (b₂ \ b₃) = (prob b₂) - (prob (b₂ /\ b₃))

proof end;

theorem Th50: :: RPR_1:50

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st b₃ c= b₂ holds
prob (b₂ \ b₃) = (prob b₂) - (prob b₃)

proof end;

theorem Th51: :: RPR_1:51

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ holds prob (b₂ \/ b₃) <= (prob b₂) + (prob b₃)

proof end;

theorem Th52: :: RPR_1:52

canceled;

theorem Th53: :: RPR_1:53

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ holds prob b₂ = (prob (b₂ /\ b₃)) + (prob (b₂ /\ (b₃ ` )))

proof end;

theorem Th54: :: RPR_1:54

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ holds prob b₂ = (prob (b₂ \/ b₃)) - (prob (b₃ \ b₂))

proof end;

theorem Th55: :: RPR_1:55

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ holds (prob b₂) + (prob ((b₂ ` ) /\ b₃)) = (prob b₃) + (prob ((b₃ ` ) /\ b₂))

proof end;

theorem Th56: :: RPR_1:56

for b₁ being non empty finite set
for b₂, b₃, b₄ being Event of b₁ holds prob ((b₂ \/ b₃) \/ b₄) = ((((prob b₂) + (prob b₃)) + (prob b₄)) - (((prob (b₂ /\ b₃)) + (prob (b₂ /\ b₄))) + (prob (b₃ /\ b₄)))) + (prob ((b₂ /\ b₃) /\ b₄))

proof end;

theorem Th57: :: RPR_1:57

for b₁ being non empty finite set
for b₂, b₃, b₄ being Event of b₁ st b₂ misses b₃ & b₂ misses b₄ & b₃ misses b₄ holds
prob ((b₂ \/ b₃) \/ b₄) = ((prob b₂) + (prob b₃)) + (prob b₄)

proof end;

theorem Th58: :: RPR_1:58

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ holds (prob b₂) - (prob b₃) <= prob (b₂ \ b₃)

proof end;

definition

let c₁ be non empty finite set ;
let c₂, c₃ be Event of c₁;
func prob c₃,c₂ -> Real equals :: RPR_1:def 5
(prob (a₃ /\ a₂)) / (prob a₂);
coherence ;

end;

:: deftheorem Def5 defines prob RPR_1:def 5 :

theorem Th59: :: RPR_1:59

canceled;

theorem Th60: :: RPR_1:60

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ holds
prob (b₂ /\ b₃) = (prob b₂,b₃) * (prob b₃) by XCMPLX_1:88;

theorem Th61: :: RPR_1:61

for b₁ being non empty finite set
for b₂ being Event of b₁ holds prob b₂,([#] b₁) = prob b₂

proof end;

theorem Th62: :: RPR_1:62

for b₁ being non empty finite set holds prob ([#] b₁),([#] b₁) = 1

proof end;

theorem Th63: :: RPR_1:63

for b₁ being non empty finite set holds prob ({} b₁),([#] b₁) = 0

proof end;

theorem Th64: :: RPR_1:64

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ holds
prob b₂,b₃ <= 1

proof end;

theorem Th65: :: RPR_1:65

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ holds
0 <= prob b₂,b₃

proof end;

theorem Th66: :: RPR_1:66

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ holds
prob b₂,b₃ = 1 - ((prob (b₃ \ b₂)) / (prob b₃))

proof end;

theorem Th67: :: RPR_1:67

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ & b₂ c= b₃ holds
prob b₂,b₃ = (prob b₂) / (prob b₃)

proof end;

theorem Th68: :: RPR_1:68

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st b₂ misses b₃ holds
prob b₂,b₃ = 0

proof end;

theorem Th69: :: RPR_1:69

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₂ & 0 < prob b₃ holds
(prob b₂) * (prob b₃,b₂) = (prob b₃) * (prob b₂,b₃)

proof end;

theorem Th70: :: RPR_1:70

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ holds
( prob b₂,b₃ = 1 - (prob (b₂ ` ),b₃) & prob (b₂ ` ),b₃ = 1 - (prob b₂,b₃) )

proof end;

theorem Th71: :: RPR_1:71

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ & b₃ c= b₂ holds
prob b₂,b₃ = 1

proof end;

theorem Th72: :: RPR_1:72

for b₁ being non empty finite set
for b₂ being Event of b₁ st 0 < prob b₂ holds
prob ([#] b₁),b₂ = 1

proof end;

theorem Th73: :: RPR_1:73

for b₁ being non empty finite set
for b₂ being Event of b₁ st 0 < prob b₂ holds
prob (b₂ ` ),b₂ = 0

proof end;

theorem Th74: :: RPR_1:74

for b₁ being non empty finite set
for b₂ being Event of b₁ st prob b₂ < 1 holds
prob b₂,(b₂ ` ) = 0

proof end;

theorem Th75: :: RPR_1:75

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ & b₂ misses b₃ holds
prob (b₂ ` ),b₃ = 1

proof end;

theorem Th76: :: RPR_1:76

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₂ & prob b₃ < 1 & b₂ misses b₃ holds
prob b₂,(b₃ ` ) = (prob b₂) / (1 - (prob b₃))

proof end;

theorem Th77: :: RPR_1:77

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₂ & prob b₃ < 1 & b₂ misses b₃ holds
prob (b₂ ` ),(b₃ ` ) = 1 - ((prob b₂) / (1 - (prob b₃)))

proof end;

theorem Th78: :: RPR_1:78

for b₁ being non empty finite set
for b₂, b₃, b₄ being Event of b₁ st 0 < prob (b₃ /\ b₄) & 0 < prob b₄ holds
prob ((b₂ /\ b₃) /\ b₄) = ((prob b₂,(b₃ /\ b₄)) * (prob b₃,b₄)) * (prob b₄)

proof end;

theorem Th79: :: RPR_1:79

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ & prob b₃ < 1 holds
prob b₂ = ((prob b₂,b₃) * (prob b₃)) + ((prob b₂,(b₃ ` )) * (prob (b₃ ` )))

proof end;

theorem Th80: :: RPR_1:80

for b₁ being non empty finite set
for b₂, b₃, b₄ being Event of b₁ st 0 < prob b₃ & 0 < prob b₄ & b₃ \/ b₄ = b₁ & b₃ misses b₄ holds
prob b₂ = ((prob b₂,b₃) * (prob b₃)) + ((prob b₂,b₄) * (prob b₄))

proof end;

theorem Th81: :: RPR_1:81

for b₁ being non empty finite set
for b₂, b₃, b₄, b₅ being Event of b₁ st 0 < prob b₃ & 0 < prob b₄ & 0 < prob b₅ & (b₃ \/ b₄) \/ b₅ = b₁ & b₃ misses b₄ & b₃ misses b₅ & b₄ misses b₅ holds
prob b₂ = (((prob b₂,b₃) * (prob b₃)) + ((prob b₂,b₄) * (prob b₄))) + ((prob b₂,b₅) * (prob b₅))

proof end;

theorem Th82: :: RPR_1:82

for b₁ being non empty finite set
for b₂, b₃, b₄ being Event of b₁ st 0 < prob b₃ & 0 < prob b₄ & b₃ \/ b₄ = b₁ & b₃ misses b₄ holds
prob b₃,b₂ = ((prob b₂,b₃) * (prob b₃)) / (((prob b₂,b₃) * (prob b₃)) + ((prob b₂,b₄) * (prob b₄)))

proof end;

theorem Th83: :: RPR_1:83

for b₁ being non empty finite set
for b₂, b₃, b₄, b₅ being Event of b₁ st 0 < prob b₃ & 0 < prob b₄ & 0 < prob b₅ & (b₃ \/ b₄) \/ b₅ = b₁ & b₃ misses b₄ & b₃ misses b₅ & b₄ misses b₅ holds
prob b₃,b₂ = ((prob b₂,b₃) * (prob b₃)) / ((((prob b₂,b₃) * (prob b₃)) + ((prob b₂,b₄) * (prob b₄))) + ((prob b₂,b₅) * (prob b₅)))

proof end;

definition

let c₁ be non empty finite set ;
let c₂, c₃ be Event of c₁;
pred c₂,c₃ are_independent means :Def6: :: RPR_1:def 6
prob (a₂ /\ a₃) = (prob a₂) * (prob a₃);
symmetry ;

end;

:: deftheorem Def6 defines are_independent RPR_1:def 6 :

theorem Th84: :: RPR_1:84

canceled;

theorem Th85: :: RPR_1:85

canceled;

theorem Th86: :: RPR_1:86

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st 0 < prob b₃ & b₂,b₃ are_independent holds
prob b₂,b₃ = prob b₂

proof end;

theorem Th87: :: RPR_1:87

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st prob b₃ = 0 holds
b₂,b₃ are_independent

proof end;

theorem Th88: :: RPR_1:88

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st b₂,b₃ are_independent holds
b₂ ` ,b₃ are_independent

proof end;

theorem Th89: :: RPR_1:89

for b₁ being non empty finite set
for b₂, b₃ being Event of b₁ st b₂ misses b₃ & b₂,b₃ are_independent & not prob b₂ = 0 holds
prob b₃ = 0

proof end;