:: Introduction to Probability
:: by Jan Popio{\l}ek
::
:: Received June 13, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
theorem
Th1
:
:: RPR_1:1
for
E
being non
empty
set
for
e
being non
empty
Subset
of
E
holds
(
e
is
Singleton
of
E
iff for
Y
being
set
holds
(
Y
c=
e
iff (
Y
=
{}
or
Y
=
e
) ) )
proof
end;
registration
let
E
be non
empty
set
;
cluster
1
-element
->
finite
for
Element
of
K11
(
E
);
coherence
for
b
1
being
Singleton
of
E
holds
b
1
is
finite
;
end;
theorem
:: RPR_1:2
for
E
being non
empty
set
for
A
,
B
being
Subset
of
E
for
e
being
Singleton
of
E
st
e
=
A
\/
B
&
A
<>
B
& not (
A
=
{}
&
B
=
e
) holds
(
A
=
e
&
B
=
{}
)
proof
end;
theorem
:: RPR_1:3
for
E
being non
empty
set
for
A
,
B
being
Subset
of
E
for
e
being
Singleton
of
E
holds
( not
e
=
A
\/
B
or (
A
=
e
&
B
=
e
) or (
A
=
e
&
B
=
{}
) or (
A
=
{}
&
B
=
e
) )
proof
end;
theorem
:: RPR_1:4
for
E
being non
empty
set
for
a
being
Element
of
E
holds
{
a
}
is
Singleton
of
E
;
theorem
:: RPR_1:5
for
E
being non
empty
set
for
e1
,
e2
being
Singleton
of
E
st
e1
c=
e2
holds
e1
=
e2
by
Th1
;
theorem
Th6
:
:: RPR_1:6
for
E
being non
empty
set
for
e
being
Singleton
of
E
ex
a
being
Element
of
E
st
(
a
in
E
&
e
=
{
a
}
)
proof
end;
theorem
:: RPR_1:7
for
E
being non
empty
set
ex
e
being
Singleton
of
E
st
e
is
Singleton
of
E
proof
end;
theorem
:: RPR_1:8
for
E
being non
empty
set
for
e
being
Singleton
of
E
ex
p
being
FinSequence
st
(
p
is
FinSequence
of
E
&
rng
p
=
e
&
len
p
=
1 )
proof
end;
definition
let
E
be
set
;
mode
Event of
E
is
Subset
of
E
;
end;
theorem
:: RPR_1:9
for
E
being non
empty
set
for
e
being
Singleton
of
E
for
A
being
Event
of
E
holds
(
e
misses
A
or
e
/\
A
=
e
)
proof
end;
theorem
:: RPR_1:10
for
E
being non
empty
set
for
A
being
Event
of
E
st
A
<>
{}
holds
ex
e
being
Singleton
of
E
st
e
c=
A
proof
end;
theorem
:: RPR_1:11
for
E
being non
empty
set
for
e
being
Singleton
of
E
for
A
being
Event
of
E
holds
( not
e
c=
A
\/
(
A
`
)
or
e
c=
A
or
e
c=
A
`
)
proof
end;
theorem
:: RPR_1:12
for
E
being non
empty
set
for
e1
,
e2
being
Singleton
of
E
holds
(
e1
=
e2
or
e1
misses
e2
)
proof
end;
theorem
Th13
:
:: RPR_1:13
for
E
being non
empty
set
for
A
,
B
being
Subset
of
E
holds
A
/\
B
misses
A
/\
(
B
`
)
proof
end;
Lm1
:
for
E
being non
empty
finite
set
holds
0
<
card
E
proof
end;
definition
let
E
be
finite
set
;
let
A
be
Event
of
E
;
func
prob
A
->
Real
equals
:: RPR_1:def 1
(
card
A
)
/
(
card
E
)
;
coherence
(
card
A
)
/
(
card
E
)
is
Real
by
XREAL_0:def 1
;
end;
::
deftheorem
defines
prob
RPR_1:def 1 :
for
E
being
finite
set
for
A
being
Event
of
E
holds
prob
A
=
(
card
A
)
/
(
card
E
)
;
theorem
:: RPR_1:14
for
E
being non
empty
finite
set
for
e
being
Singleton
of
E
holds
prob
e
=
1
/
(
card
E
)
by
CARD_1:def 7
;
theorem
:: RPR_1:15
for
E
being non
empty
finite
set
holds
prob
(
[#]
E
)
=
1
by
XCMPLX_1:60
;
theorem
Th16
:
:: RPR_1:16
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
A
misses
B
holds
prob
(
A
/\
B
)
=
0
proof
end;
theorem
:: RPR_1:17
for
E
being non
empty
finite
set
for
A
being
Event
of
E
holds
prob
A
<=
1
proof
end;
theorem
Th18
:
:: RPR_1:18
for
E
being non
empty
finite
set
for
A
being
Event
of
E
holds
0
<=
prob
A
proof
end;
theorem
Th19
:
:: RPR_1:19
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
A
c=
B
holds
prob
A
<=
prob
B
proof
end;
theorem
Th20
:
:: RPR_1:20
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
holds
prob
(
A
\/
B
)
=
(
(
prob
A
)
+
(
prob
B
)
)
-
(
prob
(
A
/\
B
)
)
proof
end;
theorem
Th21
:
:: RPR_1:21
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
A
misses
B
holds
prob
(
A
\/
B
)
=
(
prob
A
)
+
(
prob
B
)
proof
end;
theorem
Th22
:
:: RPR_1:22
for
E
being non
empty
finite
set
for
A
being
Event
of
E
holds
(
prob
A
=
1
-
(
prob
(
A
`
)
)
&
prob
(
A
`
)
=
1
-
(
prob
A
)
)
proof
end;
theorem
Th23
:
:: RPR_1:23
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
holds
prob
(
A
\
B
)
=
(
prob
A
)
-
(
prob
(
A
/\
B
)
)
proof
end;
theorem
Th24
:
:: RPR_1:24
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
B
c=
A
holds
prob
(
A
\
B
)
=
(
prob
A
)
-
(
prob
B
)
proof
end;
theorem
:: RPR_1:25
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
holds
prob
(
A
\/
B
)
<=
(
prob
A
)
+
(
prob
B
)
proof
end;
theorem
Th26
:
:: RPR_1:26
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
holds
prob
A
=
(
prob
(
A
/\
B
)
)
+
(
prob
(
A
/\
(
B
`
)
)
)
proof
end;
theorem
:: RPR_1:27
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
holds
prob
A
=
(
prob
(
A
\/
B
)
)
-
(
prob
(
B
\
A
)
)
proof
end;
theorem
:: RPR_1:28
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
holds
(
prob
A
)
+
(
prob
(
(
A
`
)
/\
B
)
)
=
(
prob
B
)
+
(
prob
(
(
B
`
)
/\
A
)
)
proof
end;
theorem
Th29
:
:: RPR_1:29
for
E
being non
empty
finite
set
for
A
,
B
,
C
being
Event
of
E
holds
prob
(
(
A
\/
B
)
\/
C
)
=
(
(
(
(
prob
A
)
+
(
prob
B
)
)
+
(
prob
C
)
)
-
(
(
(
prob
(
A
/\
B
)
)
+
(
prob
(
A
/\
C
)
)
)
+
(
prob
(
B
/\
C
)
)
)
)
+
(
prob
(
(
A
/\
B
)
/\
C
)
)
proof
end;
theorem
:: RPR_1:30
for
E
being non
empty
finite
set
for
A
,
B
,
C
being
Event
of
E
st
A
misses
B
&
A
misses
C
&
B
misses
C
holds
prob
(
(
A
\/
B
)
\/
C
)
=
(
(
prob
A
)
+
(
prob
B
)
)
+
(
prob
C
)
proof
end;
theorem
:: RPR_1:31
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
holds
(
prob
A
)
-
(
prob
B
)
<=
prob
(
A
\
B
)
proof
end;
definition
let
E
be
finite
set
;
let
B
,
A
be
Event
of
E
;
func
prob
(
A
,
B
)
->
Real
equals
:: RPR_1:def 2
(
prob
(
A
/\
B
)
)
/
(
prob
B
)
;
coherence
(
prob
(
A
/\
B
)
)
/
(
prob
B
)
is
Real
;
end;
::
deftheorem
defines
prob
RPR_1:def 2 :
for
E
being
finite
set
for
B
,
A
being
Event
of
E
holds
prob
(
A
,
B
)
=
(
prob
(
A
/\
B
)
)
/
(
prob
B
)
;
theorem
:: RPR_1:32
for
E
being non
empty
finite
set
for
A
being
Event
of
E
holds
prob
(
A
,
(
[#]
E
)
)
=
prob
A
proof
end;
theorem
:: RPR_1:33
for
E
being non
empty
finite
set
holds
prob
(
(
[#]
E
)
,
(
[#]
E
)
)
=
1
proof
end;
theorem
:: RPR_1:34
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
holds
prob
(
A
,
B
)
<=
1
proof
end;
theorem
:: RPR_1:35
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
holds
0
<=
prob
(
A
,
B
)
proof
end;
theorem
Th36
:
:: RPR_1:36
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
holds
prob
(
A
,
B
)
=
1
-
(
(
prob
(
B
\
A
)
)
/
(
prob
B
)
)
proof
end;
theorem
:: RPR_1:37
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
&
A
c=
B
holds
prob
(
A
,
B
)
=
(
prob
A
)
/
(
prob
B
)
proof
end;
theorem
Th38
:
:: RPR_1:38
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
A
misses
B
holds
prob
(
A
,
B
)
=
0
proof
end;
theorem
Th39
:
:: RPR_1:39
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
A
&
0
<
prob
B
holds
(
prob
A
)
*
(
prob
(
B
,
A
)
)
=
(
prob
B
)
*
(
prob
(
A
,
B
)
)
proof
end;
theorem
Th40
:
:: RPR_1:40
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
holds
(
prob
(
A
,
B
)
=
1
-
(
prob
(
(
A
`
)
,
B
)
)
&
prob
(
(
A
`
)
,
B
)
=
1
-
(
prob
(
A
,
B
)
)
)
proof
end;
theorem
Th41
:
:: RPR_1:41
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
&
B
c=
A
holds
prob
(
A
,
B
)
=
1
proof
end;
theorem
:: RPR_1:42
for
E
being non
empty
finite
set
for
B
being
Event
of
E
st
0
<
prob
B
holds
prob
(
(
[#]
E
)
,
B
)
=
1
by
Th41
;
theorem
:: RPR_1:43
for
E
being non
empty
finite
set
for
A
being
Event
of
E
holds
prob
(
(
A
`
)
,
A
)
=
0
proof
end;
theorem
:: RPR_1:44
for
E
being non
empty
finite
set
for
A
being
Event
of
E
holds
prob
(
A
,
(
A
`
)
)
=
0
proof
end;
theorem
Th45
:
:: RPR_1:45
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
&
A
misses
B
holds
prob
(
(
A
`
)
,
B
)
=
1
proof
end;
theorem
Th46
:
:: RPR_1:46
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
A
&
prob
B
<
1 &
A
misses
B
holds
prob
(
A
,
(
B
`
)
)
=
(
prob
A
)
/
(
1
-
(
prob
B
)
)
proof
end;
theorem
:: RPR_1:47
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
A
&
prob
B
<
1 &
A
misses
B
holds
prob
(
(
A
`
)
,
(
B
`
)
)
=
1
-
(
(
prob
A
)
/
(
1
-
(
prob
B
)
)
)
proof
end;
theorem
:: RPR_1:48
for
E
being non
empty
finite
set
for
A
,
B
,
C
being
Event
of
E
st
0
<
prob
(
B
/\
C
)
&
0
<
prob
C
holds
prob
(
(
A
/\
B
)
/\
C
)
=
(
(
prob
(
A
,
(
B
/\
C
)
)
)
*
(
prob
(
B
,
C
)
)
)
*
(
prob
C
)
proof
end;
theorem
Th49
:
:: RPR_1:49
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
&
prob
B
<
1 holds
prob
A
=
(
(
prob
(
A
,
B
)
)
*
(
prob
B
)
)
+
(
(
prob
(
A
,
(
B
`
)
)
)
*
(
prob
(
B
`
)
)
)
proof
end;
theorem
Th50
:
:: RPR_1:50
for
E
being non
empty
finite
set
for
A
,
B1
,
B2
being
Event
of
E
st
0
<
prob
B1
&
0
<
prob
B2
&
B1
\/
B2
=
E
&
B1
misses
B2
holds
prob
A
=
(
(
prob
(
A
,
B1
)
)
*
(
prob
B1
)
)
+
(
(
prob
(
A
,
B2
)
)
*
(
prob
B2
)
)
proof
end;
theorem
Th51
:
:: RPR_1:51
for
E
being non
empty
finite
set
for
A
,
B1
,
B2
,
B3
being
Event
of
E
st
0
<
prob
B1
&
0
<
prob
B2
&
0
<
prob
B3
&
(
B1
\/
B2
)
\/
B3
=
E
&
B1
misses
B2
&
B1
misses
B3
&
B2
misses
B3
holds
prob
A
=
(
(
(
prob
(
A
,
B1
)
)
*
(
prob
B1
)
)
+
(
(
prob
(
A
,
B2
)
)
*
(
prob
B2
)
)
)
+
(
(
prob
(
A
,
B3
)
)
*
(
prob
B3
)
)
proof
end;
theorem
:: RPR_1:52
for
E
being non
empty
finite
set
for
A
,
B1
,
B2
being
Event
of
E
st
0
<
prob
B1
&
0
<
prob
B2
&
B1
\/
B2
=
E
&
B1
misses
B2
holds
prob
(
B1
,
A
)
=
(
(
prob
(
A
,
B1
)
)
*
(
prob
B1
)
)
/
(
(
(
prob
(
A
,
B1
)
)
*
(
prob
B1
)
)
+
(
(
prob
(
A
,
B2
)
)
*
(
prob
B2
)
)
)
proof
end;
theorem
:: RPR_1:53
for
E
being non
empty
finite
set
for
A
,
B1
,
B2
,
B3
being
Event
of
E
st
0
<
prob
B1
&
0
<
prob
B2
&
0
<
prob
B3
&
(
B1
\/
B2
)
\/
B3
=
E
&
B1
misses
B2
&
B1
misses
B3
&
B2
misses
B3
holds
prob
(
B1
,
A
)
=
(
(
prob
(
A
,
B1
)
)
*
(
prob
B1
)
)
/
(
(
(
(
prob
(
A
,
B1
)
)
*
(
prob
B1
)
)
+
(
(
prob
(
A
,
B2
)
)
*
(
prob
B2
)
)
)
+
(
(
prob
(
A
,
B3
)
)
*
(
prob
B3
)
)
)
proof
end;
definition
let
E
be
finite
set
;
let
A
,
B
be
Event
of
E
;
pred
A
,
B
are_independent
means
:
Def3
:
:: RPR_1:def 3
prob
(
A
/\
B
)
=
(
prob
A
)
*
(
prob
B
)
;
symmetry
for
A
,
B
being
Event
of
E
st
prob
(
A
/\
B
)
=
(
prob
A
)
*
(
prob
B
)
holds
prob
(
B
/\
A
)
=
(
prob
B
)
*
(
prob
A
)
;
end;
::
deftheorem
Def3
defines
are_independent
RPR_1:def 3 :
for
E
being
finite
set
for
A
,
B
being
Event
of
E
holds
(
A
,
B
are_independent
iff
prob
(
A
/\
B
)
=
(
prob
A
)
*
(
prob
B
)
);
theorem
:: RPR_1:54
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
0
<
prob
B
&
A
,
B
are_independent
holds
prob
(
A
,
B
)
=
prob
A
proof
end;
theorem
:: RPR_1:55
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
prob
B
=
0
holds
A
,
B
are_independent
proof
end;
theorem
:: RPR_1:56
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
A
,
B
are_independent
holds
A
`
,
B
are_independent
proof
end;
theorem
:: RPR_1:57
for
E
being non
empty
finite
set
for
A
,
B
being
Event
of
E
st
A
misses
B
&
A
,
B
are_independent
& not
prob
A
=
0
holds
prob
B
=
0
proof
end;