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 f, g, n, x, y, A, B, C, fx, fy, gx
from proveit import Function, Lambda, Conditional
from proveit.relation import total_ordering
from proveit.logic import (
And, Implies, Forall, Equals, NotEquals, InSet, Card,
Functions, Image, Bijections, Injections, Surjections)
from proveit.numbers import Natural
```

In [2]:

```
%begin theorems
```

In [3]:

```
membership_unfolding = Forall(
(A, B), Forall(
f, And(InSet(f, Injections(A, B)),
InSet(f, Surjections(A, B))),
domain=Bijections(A, B)))
```

In [4]:

```
membership_folding = Forall(
(A, B), Forall(
f, InSet(f, Bijections(A, B)),
conditions=[InSet(f, Injections(A, B)),
InSet(f, Surjections(A, B))]))
```

A bijection is a function, an injection, and a surjection.

In [5]:

```
bijection_is_function = Forall(
(A, B), Forall(f, InSet(f, Functions(A, B)),
domain=Bijections(A, B)))
```

In [6]:

```
bijection_is_injection = Forall(
(A, B), Forall(f, InSet(f, Injections(A, B)),
domain=Bijections(A, B)))
```

In [7]:

```
bijection_is_surjection = Forall(
(A, B), Forall(f, InSet(f, Surjections(A, B)),
domain=Bijections(A, B)))
```

In [8]:

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

If mapped unique elements of a function are unique, then the function is a bijection onto its image.

In [9]:

```
bijective_by_uniqueness = Forall(
(f, A),
Implies(Forall((x, y), NotEquals(fx, fy),
domain=A, condition=NotEquals(x, y)),
InSet(f, Bijections(A, Image(f, A)))))
```

In [10]:

```
bijection_transitivity = Forall(
(f, g, A, B, C),
Implies(And(InSet(f, Bijections(A, B)), InSet(g, Bijections(B, C))),
InSet(Lambda(x, Conditional(Function(g, fx), InSet(x, A))),
Bijections(A, C)))
.with_wrap_before_operator())
```

If the domain is finite, we know the function is a bijection if its image covers the codomain and is the same size as the domain.

In [11]:

```
bijective_by_finite_image_size = Forall(
n, Forall(
(f, A), InSet(f, Bijections(A, Image(f, A))),
condition=total_ordering(
Equals(Card(Image(f, A)), Card(A)),
Equals(Card(A), n))),
domain=Natural)
```

In [12]:

```
%end theorems
```