In [1]:

```
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import a, b, f, n, x, A, B, C, fa, fb, fx
from proveit import Lambda, Conditional
from proveit.logic import (
And, Forall, Equals, NotEquals, InSet, Disjoint, SubsetEq,
Functions, Image, Injections)
from proveit.numbers import Natural
```

In [2]:

```
%begin theorems
```

In [3]:

```
membership_unfolding = Forall(
(A, B), Forall(
f, And(InSet(f, Functions(A, B)),
Forall((a, b), NotEquals(fa, fb),
domain=A, condition=NotEquals(a, b))),
domain=Injections(A, B)))
```

In [4]:

```
membership_folding = Forall(
(A, B), Forall(
f, InSet(f, Injections(A, B)),
domain=Functions(A, B),
condition=Forall((a, b), NotEquals(fa, fb),
domain=A, condition=NotEquals(a, b))))
```

An injection is a function.

In [5]:

```
injection_is_function = Forall(
(A, B), Forall(f, InSet(f, Functions(A, B)),
domain=Injections(A, B)))
```

In [6]:

```
elim_domain_condition = Forall(
(A, B), Forall(f, InSet(f, Injections(A, B)),
condition=InSet(Lambda(x, Conditional(fx, InSet(x, A))),
Injections(A, B))))
```

In [7]:

```
subset_injection = Forall(
(A, B, C), Forall(f, InSet(f, Injections(A, C)),
domain = Injections(B, C)),
condition=SubsetEq(A, B))
```

In [8]:

```
disjoint_set_images_are_disjoint = Forall(
(A, B, C), Forall(
f, Disjoint(Image(f, A), Image(f, B)),
domain = Injections(A, C)),
condition = Disjoint(A, B))
```

In [9]:

```
%end theorems
```