In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import f, x, Q, X, Omega, fx, Qx
from proveit.logic import (And, Forall, Equals, InSet, InClass,
SubsetEq, SetOfAll, Functions)
from proveit.numbers import zero, one, Sum
from proveit.statistics import (
SampleSpaces, Prob, prob_domain, ProbOfAll)
```

In [2]:

```
%begin axioms
```

A sample space is a set of samples whose probabilities are between 0 and 1 and whose sum of probabilities, over all samples, is equal to 1.

In [3]:

```
samples_space_def = Forall(
Omega,
Equals(InClass(Omega, SampleSpaces),
And(Forall(x, InSet(Prob(x), prob_domain),
domain=Omega),
Equals(Sum(x, Prob(x), domain=Omega),
one))).with_wrap_after_operator())
```

An `event`

is a subset of the sample space. The probability of the event is the sum of probabilities of the samples contained in the event.

In [4]:

```
event_prob_def = Forall(
Omega, Forall(
X, Equals(Prob(X), Sum(x, Prob(x), domain=X)),
condition=SubsetEq(X, Omega)),
domain=SampleSpaces)
```

`ProbOfAll`

is the probability of an event (a sample space subset)¶In [5]:

```
prob_of_all_def = Forall(
Omega, Forall(
X, Forall(
f, Forall(
Q,
Equals(ProbOfAll(x, fx, domain=X, condition=Qx),
Prob(SetOfAll(x, fx, domain=X, condition=Qx)))
.with_wrap_after_operator()),
domain=Functions(X, Omega))),
domain=SampleSpaces)
```

In [6]:

```
%end axioms
```