# 8. Functions

So far in the book, we have studied properties of numbers (whether a number is odd, positive, prime; whether one number is divisible by another) and operations on numbers (addition, greatest common divisor).

In this chapter we go up a level of abstraction, and study properties of and
operations on functions. These new properties include: whether a function is
*injective*, *surjective*, *bijective*; whether one function is *inverse* to
another; and the operation of *composition*.

We also expand our horizon beyond the numeric types (\(\mathbb{N}\), \(\mathbb{Z}\), \(\mathbb{Q}\), \(\mathbb{R}\)) which have formed the setting of the early part of the book. We now start to work with a broader range of types, including function types, finite inductive types, and product types.

## 8.1. Injectivity and surjectivity

### 8.1.1. Example

We have studied particular functions before. For example, the Fibonacci sequence from Example 6.3.3 is a function from \(\mathbb{N}\) to \(\mathbb{Z}\): it takes in a natural number, for example 5, and gives out an integer, in this case 8 (the index-5 term of the sequence).

```
def F : ℕ → ℤ
| 0 => 1
| 1 => 1
| n + 2 => F (n + 1) + F n
#eval F 5 -- infoview displays `8`
```

The *domain* of a function is the type where it takes its input values, and the *codomain* of a
function is the type where it takes its output values. For example, the domain of the Fibonacci
sequence is \(\mathbb{N}\) and its codomain is \(\mathbb{Z}\). The type of functions with
domain \(\mathbb{N}\) and codomain \(\mathbb{Z}\) is denoted
\(\mathbb{N}\to \mathbb{Z}\). Lean will confirm for us that the Fibonacci sequence `F`

has
this type:

```
#check @F -- infoview displays `F : ℕ → ℤ`
```

Another way to define a function is by a closed formula. For example, “let \(q:\mathbb{R}\to \mathbb{R}\) be the function defined by, \(q(x)=x+3\).” In Lean we can write this as

```
def q (x : ℝ) : ℝ := x + 3
```

This function has domain \(\mathbb{R}\) and codomain \(\mathbb{R}\) – I even said when I was defining it that I was making \(q\) to have type \(\mathbb{R}\to \mathbb{R}\). Let’s check that this is indeed the type of the Lean object:

```
#check @q -- infoview displays `q : ℝ → ℝ`
```

A third way to define a function, if we expect to use it just once and don’t want to waste a name on it, is by using the notation \(\mapsto\): we can refer to “the function \(x \mapsto x ^ 2\) from \(\mathbb{R}\) to \(\mathbb{R}\)”. Here is the same notation in Lean:

```
#check fun (x : ℝ) ↦ x ^ 2 -- infoview displays `fun x ↦ x ^ 2 : ℝ → ℝ`
```

### 8.1.2. Definition

Now that we have the notation \(X\to Y\) for “the type of functions from \(X\) to \(Y\)”, we can introduce properties of functions, in the same way that we have previously introduced properties (like “odd” and “prime”) of numbers. Here is our first one.

Definition

A function \(f : X \to Y\) is *injective*, if for all \(x_1\) and \(x_2\) of type
\(X\), if \(f(x_1)=f(x_2)\), then \(x_1=x_2\).

```
def Injective (f : X → Y) : Prop := ∀ {x1 x2 : X}, f x1 = f x2 → x1 = x2
```

### 8.1.3. Example

Problem

Show that the function \(q:\mathbb{R}\to\mathbb{R}\) from Example 8.1.1 is injective.

Solution

Let \(x_1\) and \(x_2\) be real numbers and suppose that \(q(x_1)=q(x_2)\). Then \(x_1+1=x_2+1\), so \(x_1=x_2\).

Here is this solution in Lean. Note that after unfolding the definition “injective” using the
command `dsimp [Injective]`

, the goal state displays

```
⊢ ∀ ⦃x1 x2 : ℝ⦄, q x1 = q x2 → x1 = x2
```

This is the “injective” definition specialized to the problem at hand.

```
example : Injective q := by
dsimp [Injective]
intro x1 x2 h
dsimp [q] at h
addarith [h]
```

### 8.1.4. Example

Problem

Show that the function \(x \mapsto x ^ 2\) from \(\mathbb{R}\) to \(\mathbb{R}\) is not injective.

Solution

We must show that there exist real numbers \(x_1\) and \(x_2\), such that \(x_1{}^2=x_2{}^2\) and \(x_1\ne x_2\). Indeed, -1 and 1 have these properties.

The first sentence of that proof was a negation-normalization: I unfolded the “injective” definition
and restated its negation in a logically equivalent but more convenient form. Recall that in Lean
we do this using the tactic `push_neg`

. Here is the goal state after the tactic `push_neg`

has
been used:

```
⊢ ∃ x1 x2, x1 ^ 2 = x2 ^ 2 ∧ x1 ≠ x2
```

And here is the full Lean proof.

```
example : ¬ Injective (fun x : ℝ ↦ x ^ 2) := by
dsimp [Injective]
push_neg
use -1, 1
constructor
· numbers
· numbers
```

### 8.1.5. Definition

Definition

A function \(f : X \to Y\) is *surjective*, if for all \(y\) of type \(Y\), there
exists \(x\) of type \(X\), such that \(f(x)=y\).

```
def Surjective (f : X → Y) : Prop := ∀ y : Y, ∃ x : X, f x = y
```

### 8.1.6. Example

Problem

Consider the function \(s:\mathbb{Q}\to\mathbb{Q}\) defined by, \(s(a)=3a+2\). Show that \(s\) is surjective.

Solution

Let \(y\) be a rational number. Then

Here is the solution in Lean. The goal state after unfolding the definition of “surjective” is

```
⊢ ∀ (y : ℚ), ∃ x, s x = y
```

which confirms what we need to prove and why what we wrote in the text proof above is sufficient.

```
def s (a : ℚ) : ℚ := 3 * a + 2
example : Surjective s := by
dsimp [Surjective]
intro y
use (y - 2) / 3
calc s ((y - 2) / 3) = 3 * ((y - 2) / 3) + 2 := by rw [s]
_ = y := by ring
```

### 8.1.7. Example

Problem

Show that the function \(x \mapsto x ^ 2\) from \(\mathbb{R}\) to \(\mathbb{R}\) is not surjective.

Solution

We will show that there exists a real number \(y\), such that for all real numbers \(x\), \(x^2\ne y\).

Indeed, let us show that -1 has this property. Let \(x\) be a real number. Then

so \(x^2\ne -1\).

As in Example 8.1.4, the first sentence constitutes a
negation-normalization of the definition of “surjective” in this context. Effectively we are stating
what would be the goal state in the Lean proof after `push_neg`

.

```
⊢ ∃ y, ∀ (x : ℝ), x ^ 2 ≠ y
```

And here is the full Lean proof.

```
example : ¬ Surjective (fun x : ℝ ↦ x ^ 2) := by
dsimp [Surjective]
push_neg
use -1
intro x
apply ne_of_gt
calc -1 < 0 := by numbers
_ ≤ x ^ 2 := by extra
```

### 8.1.8. Example

We have so far seen numeric types, like the integers \(\mathbb{Z}\) and the real numbers \(\mathbb{R}\), and function types, like \(\mathbb{Z}\to \mathbb{R}\) (the functions from \(\mathbb{Z}\) to \(\mathbb{R}\)).

Another way to make a type is as a finite set of options. Finite types are useful for conceptual examples, because everything is explicit and checkable.

```
inductive Musketeer
| athos
| porthos
| aramis
deriving DecidableEq
```

Here is how to define a function whose domain is a given finite inductive type.

```
def f : Musketeer → Musketeer
| athos => aramis
| porthos => aramis
| aramis => athos
```

Problem

Show that the function \(f\) is not injective.

```
example : ¬ Injective f := by
dsimp [Injective]
push_neg
use athos, porthos
dsimp [f] -- optional
exhaust
```

The tactic `exhaust`

is new here. At the place where it is used, the goal state is

```
aramis = aramis ∧ athos ≠ porthos
```

that is,

```
True ∧ ¬ False
```

which is logically equivalent to `True`

. The tactic `exhaust`

can do this kind of propositional
logic reasoning, up to arbitrary complexity.

In particular, `exhaust`

can prove any (true) variable-free statement in an inductive type, and
that’s how we’ll use it in this chapter. We start making more serious use of `exhaust`

in
Chapter 9.

### 8.1.9. Example

Problem

Show that the function \(f\) defined in Example 8.1.8 is not surjective.

We can case-check on a variable `a`

in a finite inductive type using the tactic `cases`

.

```
example : ¬ Surjective f := by
dsimp [Surjective]
push_neg
use porthos
intro a
cases a
· exhaust
· exhaust
· exhaust
```

Such proofs can become repetitive, and you may wish to use a trick we have seen before (for example
Example 4.4.4, Example 4.5.9,
Example 6.6.2, Example 6.7.2): when a tactic such as
`cases`

generates many goals which can all be proved by the same tactic, you can write
`<;>`

to apply the tactic to all those goals.

```
-- better (more automated) version of the previous proof
example : ¬ Surjective f := by
dsimp [Surjective]
push_neg
use porthos
intro a
cases a <;> exhaust
```

You might also like to check that the `cases a <;> exhaust`

line is necessary; `exhaust`

can’t close
the goal on its own. As discussed in Example 8.1.8, `exhaust`

can prove any
(true) *variable-free* statement in an inductive type, but before the `cases a <;> exhaust`

line the
goal state is

```
a : Musketeer
⊢ f a ≠ porthos
```

which contains a variable, `a`

.

### 8.1.10. Example

Let \(g\) be the following function from the Musketeer type to itself:

```
def g : Musketeer → Musketeer
| athos => porthos
| porthos => aramis
| aramis => athos
```

Problem

Show that the function \(g\) is injective.

There are a lot of cases in this proof – \(3 \times 3 = 9\), to be precise. Fortunately
`exhaust`

can prove all of them!

```
example : Injective g := by
dsimp [Injective]
intro x1 x2 hx
cases x1 <;> cases x2 <;> exhaust
```

### 8.1.11. Example

Problem

Show that the function \(g\) defined in Example 8.1.10 is surjective.

```
example : Surjective g := by
dsimp [Surjective]
intro y
cases y
· use aramis
exhaust
· use athos
exhaust
· use porthos
exhaust
```

### 8.1.12. Example

We finish with a relatively hard example. The proof here is efficient and self-contained but not
particularly well-motivated. For an alternative (perhaps more intuitive) approach, combine the last
exercise in this section (the one about *strictly monotone* functions) with the idea from
Example 2.1.8.

Problem

Show that the function \(x \mapsto x ^ 3\) from \(\mathbb{R}\) to \(\mathbb{R}\) is injective.

Solution

Let \(x_1\) and \(x_2\) be real numbers and suppose that \(x_1{}^3=x_2{}^3\). Then

so either \(x_1-x_2=0\), in which case we are done, or \(x_1{}^2+x_1x_2+x_2{}^2=0\), which we henceforth assume.

We now consider a further case split according to whether \(x_1=0\).

**Case 1** (\(x_1=0\)): Then

so \(x_2=0\) also. Thus \(x_1=0=x_2\) as required.

**Case 2** (\(x_1\ne 0\)): Then

contradiction.

```
example : Injective (fun (x:ℝ) ↦ x ^ 3) := by
intro x1 x2 hx
dsimp at hx
have H : (x1 - x2) * (x1 ^ 2 + x1 * x2 + x2 ^ 2) = 0
· calc (x1 - x2) * (x1 ^ 2 + x1 * x2 + x2 ^ 2) = x1 ^ 3 - x2 ^ 3 := by ring
_ = x1 ^ 3 - x1 ^ 3 := by rw [hx]
_ = 0 := by ring
rw [mul_eq_zero] at H
obtain H1 | H2 := H
· -- case 1: x1 - x2 = 0
addarith [H1]
· -- case 2: x1 ^2 + x1 * x2 + x2 ^ 2 = 0
by_cases hx1 : x1 = 0
· -- case 2a: x1 = 0
have hx2 :=
calc x2 ^ 3 = x1 ^ 3 := by rw [hx]
_ = 0 ^ 3 := by rw [hx1]
_ = 0 := by numbers
cancel 3 at hx2
calc x1 = 0 := by rw [hx1]
_ = x2 := by rw [hx2]
· -- case 2b: x1 ≠ 0
have :=
calc 0 < x1 ^ 2 + ((x1 + x2) ^ 2 + x2 ^ 2) := by extra
_ = 2 * (x1 ^ 2 + x1 * x2 + x2 ^ 2) := by ring
_ = 2 * 0 := by rw [H2]
_ = 0 := by ring
numbers at this -- contradiction!
```

### 8.1.13. Exercises

Prove or disprove that the function \(x \mapsto x-12\) from \(\mathbb{Q}\) to \(\mathbb{Q}\) is injective.

(If you think it’s true, prove it, by solving the first version below. If you think it’s false, solve the second version.)

example : Injective (fun (x : ℚ) ↦ x - 12) := by sorry example : ¬ Injective (fun (x : ℚ) ↦ x - 12) := by sorry

Prove or disprove that the function \(x \mapsto 3\) from \(\mathbb{R}\) to \(\mathbb{R}\) is injective.

(If you think it’s true, prove it, by solving the first version below. If you think it’s false, solve the second version.)

example : Injective (fun (x : ℝ) ↦ 3) := by sorry example : ¬ Injective (fun (x : ℝ) ↦ 3) := by sorry

Prove or disprove that the function \(x \mapsto 3x-1\) from \(\mathbb{ℚ}\) to \(\mathbb{ℚ}\) is injective.

(If you think it’s true, prove it, by solving the first version below. If you think it’s false, solve the second version.)

example : Injective (fun (x : ℚ) ↦ 3 * x - 1) := by sorry example : ¬ Injective (fun (x : ℚ) ↦ 3 * x - 1) := by sorry

Prove or disprove that the function \(x \mapsto 3x-1\) from \(\mathbb{Z}\) to \(\mathbb{Z}\) is injective.

example : Injective (fun (x : ℤ) ↦ 3 * x - 1) := by sorry example : ¬ Injective (fun (x : ℤ) ↦ 3 * x - 1) := by sorry

Prove or disprove that the function \(x \mapsto 2x\) from \(\mathbb{R}\) to \(\mathbb{R}\) is surjective.

example : Surjective (fun (x : ℝ) ↦ 2 * x) := by sorry example : ¬ Surjective (fun (x : ℝ) ↦ 2 * x) := by sorry

Prove or disprove that the function \(x \mapsto 2x\) from \(\mathbb{Z}\) to \(\mathbb{Z}\) is surjective.

example : Surjective (fun (x : ℤ) ↦ 2 * x) := by sorry example : ¬ Surjective (fun (x : ℤ) ↦ 2 * x) := by sorry

Prove or disprove that the function \(n \mapsto n^2\) from \(\mathbb{N}\) to \(\mathbb{N}\) is surjective.

example : Surjective (fun (n : ℕ) ↦ n ^ 2) := by sorry example : ¬ Surjective (fun (n : ℕ) ↦ n ^ 2) := by sorry

Consider the following finite inductive type White, and the following function \(h\) from the Musketeer type (see Example 8.1.8) to the White type. Prove or disprove that the function \(h\) is injective.

inductive White | meg | jack deriving DecidableEq open White def h : Musketeer → White | athos => jack | porthos => meg | aramis => jack example : Injective h := by sorry example : ¬ Injective h := by sorry

Prove or disprove that the function \(h\) from the previous example is surjective.

example : Surjective h := by sorry example : ¬ Surjective h := by sorry

Consider the following function \(l\) from the White type (see the previous two problems) to the Musketeer type (see Example 8.1.8). Prove or disprove that the function \(l\) is injective.

def l : White → Musketeer | meg => aramis | jack => porthos example : Injective l := by sorry example : ¬ Injective l := by sorry

Prove or disprove that the function \(l\) from the previous example is surjective.

example : Surjective l := by sorry example : ¬ Surjective l := by sorry

Let \(f : X \to Y\) be a function. Show that \(f\) is injective if and only if for all \(x_1\) and \(x_2\) of type \(X\), if \(x_1\ne x_2\) then \(f(x_1)\ne f(x_2)\).

You will need to use a tactic (such as

`push_neg`

or`by_cases`

) which is capable of handling the subtler negations.example (f : X → Y) : Injective f ↔ ∀ x1 x2 : X, x1 ≠ x2 → f x1 ≠ f x2 := by sorry

Prove or disprove that for all functions \(f:\mathbb{Q}\to \mathbb{Q}\), if \(f\) is injective, then the function \(x \mapsto f(x)+1\) from \(\mathbb{Q}\) to \(\mathbb{Q}\) is also injective.

example : ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + 1) := by sorry example : ¬ ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + 1) := by sorry

Prove or disprove that for all functions \(f:\mathbb{Q}\to \mathbb{Q}\), if \(f\) is injective, then the function \(x \mapsto f(x)+x\) from \(\mathbb{Q}\) to \(\mathbb{Q}\) is also injective.

example : ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + x) := by sorry example : ¬ ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + x) := by sorry

Prove or disprove that for all functions \(f:\mathbb{Z}\to \mathbb{Z}\), if \(f\) is surjective, then the function \(x \mapsto 2f(x)\) from \(\mathbb{Z}\) to \(\mathbb{Z}\) is also surjective.

example : ∀ (f : ℤ → ℤ), Surjective f → Surjective (fun x ↦ 2 * f x) := by sorry example : ¬ ∀ (f : ℤ → ℤ), Surjective f → Surjective (fun x ↦ 2 * f x) := by sorry

Prove or disprove that for all real numbers \(c\), the function \(x\mapsto cx\) from \(\mathbb{R}\) to \(\mathbb{R}\) is surjective.

example : ∀ c : ℝ, Surjective (fun x ↦ c * x) := by sorry example : ¬ ∀ c : ℝ, Surjective (fun x ↦ c * x) := by sorry

Let \(f:\mathbb{Q}\to\mathbb{Q}\) be a function which is

*strictly monotone*; that is, for all real numbers \(x\) and \(y\) with \(x<y\), it is true that \(f(x)<f(y)\). Prove that \(f\) is injective.You may wish to use the lemma

`lt_trichotomy`

lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ x < y :=

which gives a case division on the relative sizes of two real numbers.

example {f : ℚ → ℚ} (hf : ∀ x y, x < y → f x < f y) : Injective f := by sorry

Let \(f:X\to\mathbb{N}\) be a function, let \(x_0\) be of type \(X\) with \(f(x_0)=0\), and let \(i:X\to X\) be a function such that, for all \(x\), \(f(i(x))=f(x)+1\). Show that \(f\) is surjective. I recommend induction.

We record this theorem for future use under the name

`surjective_of_intertwining`

.example {f : X → ℕ} {x0 : X} (h0 : f x0 = 0) {i : X → X} (hi : ∀ x, f (i x) = f x + 1) : Surjective f := by sorry

## 8.2. Bijectivity

### 8.2.1. Definition

Definition

A function is *bijective*, if it is both injective and surjective.

```
def Bijective (f : X → Y) : Prop := Injective f ∧ Surjective f
```

### 8.2.2. Example

Problem

Let \(p:\mathbb{R}\to\mathbb{R}\) be the function defined by, \(p(x)=2x-5\). Show that \(p\) is bijective.

Solution

We must show that \(p\) is injective and surjective.

For the injectivity, let \(x_1\) and \(x_2\) be real numbers and suppose that \(p(x_1)=p(x_2)\). This means that \(2x_1-5=2x_2-5\). So

For the surjectivity, let \(y\) be a real number. Then

```
def p (x : ℝ) : ℝ := 2 * x - 5
example : Bijective p := by
dsimp [Bijective]
constructor
· dsimp [Injective]
intro x1 x2 hx
dsimp [p] at hx
calc x1 = ((2 * x1 - 5) + 5) / 2 := by ring
_ = ((2 * x2 - 5) + 5) / 2 := by rw [hx]
_ = x2 := by ring
· dsimp [Surjective]
intro y
use (y + 5) / 2
calc p ((y + 5) / 2) = 2 * ((y + 5) / 2) - 5 := by rfl
_ = y := by ring
```

### 8.2.3. Example

Problem

Let \(a:\mathbb{R}\to\mathbb{R}\) be the function defined by, \(a(t)=t^3-t\). Show that \(a\) is not bijective.

Solution

We will show that \(a\) is not injective. Indeed, note that \(0\ne 1\) but

```
def a (t : ℝ) : ℝ := t ^ 3 - t
example : ¬ Bijective a := by
dsimp [Bijective]
push_neg
left
dsimp [Injective]
push_neg
use 0, 1
constructor
· calc a 0 = 0 ^ 3 - 0 := by rfl
_ = 1 ^ 3 - 1 := by numbers
_ = a 1 := by rfl
· numbers
```

### 8.2.4. Example

Consider the following finite inductive types Celestial and Subatomic:

```
inductive Celestial
| sun
| moon
deriving DecidableEq
inductive Subatomic
| proton
| neutron
| electron
deriving DecidableEq
```

Consider the following function \(f\) from the Celestial type to the Subatomic type.

```
def f : Celestial → Subatomic
| sun => proton
| moon => electron
```

Problem

Prove that the function \(f\) is not bijective.

```
example : ¬ Bijective f := by
dsimp [Bijective]
push_neg
right
dsimp [Surjective]
push_neg
use neutron
intro x
cases x <;> exhaust
```

### 8.2.5. Example

Theorem

A function \(f:X\to Y\) is bijective, if and only if for all \(y\) of type \(Y\), there exists a unique \(x\) of type \(X\), such that \(f(x)=y\).

Proof

First, suppose that \(f\) is bijective. Let \(y\) be of type \(Y\). Since \(f\) is surjective, there exists \(x\) of type \(X\), such that \(f(x)=y\). We will show that this \(x\) is unique. Indeed, for any other \(x'\) with \(f(x')=y\), we have that

and so by the injectivity of \(f\), \(x'=x\).

Conversely, suppose that for all \(y\) of type \(Y\), there exists a unique \(x\) of type \(X\), such that \(f(x)=y\). (\(\star\)) We must show that \(f\) is injective and surjective.

For the injectivity, let \(x_1\) and \(x_2\) be of type \(X\), and suppose that \(f(x_1)=f(x_2)\). By (\(\star\)) applied with \(y=f(x_1)\), there exists a unique \(x\) of type \(X\) for which \(f(x)=f(x_1)\). So, by the uniqueness, \(x_1=x\), and also, since \(f(x_2)=f(x_1)=f(x)\), \(x_2=x\). Combining these, \(x_1=x_2\).

For the surjectivity, let \(y\) be of type \(Y\). By (\(\star\)), there exists (a unique) \(x\) of type \(X\) for which \(f(x)=y\).

```
example {f : X → Y} : Bijective f ↔ ∀ y, ∃! x, f x = y := by
constructor
· -- if `f` is bijective then `∀ y, ∃! x, f x = y`
intro h y
obtain ⟨h_inj, h_surj⟩ := h
obtain ⟨x, hx⟩ := h_surj y
use x
dsimp
constructor
· apply hx
· intro x' hx'
apply h_inj
calc f x' = y := by rw [hx']
_ = f x := by rw [hx]
· -- if `∀ y, ∃! x, f x = y` then `f` is bijective
intro h
constructor
· -- `f` is injective
intro x1 x2 hx1x2
obtain ⟨x, hx, hx'⟩ := h (f x1)
have hxx1 : x1 = x
· apply hx'
rfl
have hxx2 : x2 = x
· apply hx'
rw [hx1x2]
calc x1 = x := by rw [hxx1]
_ = x2 := by rw [hxx2]
· -- `f` is surjective
intro y
obtain ⟨x, hx, hx'⟩ := h y
use x
apply hx
```

### 8.2.6. Example

Problem

Show that for all functions \(f\) from the Celestial type (Example 8.2.4) to itself, if \(f\) is injective then it is bijective.

We prove this by an exhaustive analysis of all functions \(f\) from the Celestial type to itself. There are four such functions. I dealt with the first two cases below; fill in the second two cases yourself.

```
example : ∀ f : Celestial → Celestial, Injective f → Bijective f := by
intro f hf
constructor
· -- `f` is injective by assumption
apply hf
-- show that `f` is surjective
match h_sun : f sun, h_moon : f moon with
| sun, sun =>
have : sun = moon
· apply hf
rw [h_sun, h_moon]
contradiction
| sun, moon =>
intro y
cases y
· use sun
apply h_sun
· use moon
apply h_moon
| moon, sun => sorry
| moon, moon => sorry
```

### 8.2.7. Example

Problem

Show that it is not true that for all functions \(f:\mathbb{N}\to \mathbb{N}\), if \(f\) is injective then it is bijective.

Solution

We must show that there exists a function \(f:\mathbb{N}\to \mathbb{N}\), which is injective but not bijective.

Indeed, consider the function \(f(n)=n+1\). This function is injective, since for all natural numbers \(n_1\) and \(n_2\), if \(n_1+1=n_2+1\) then \(n_1=n_2\).

However, this function is not surjective, and therefore not bijective. To see this, observe that for all natural numbers \(n\), we have \(f(n)=n+1>0\) and therefore \(f(n)\ne 0\).

```
example : ¬ ∀ f : ℕ → ℕ, Injective f → Bijective f := by
push_neg
use fun n ↦ n + 1
constructor
· -- the function is injective
intro n1 n2 hn
addarith [hn]
· -- the function is not bijective
dsimp [Bijective]
push_neg
right
-- specifically, it's not surjective
dsimp [Surjective]
push_neg
use 0
intro n
apply ne_of_gt
extra
```

### 8.2.8. Exercises

Prove or disprove that the function \(x \mapsto 4-3x\) from \(\mathbb{R}\) to \(\mathbb{R}\) is bijective.

example : Bijective (fun (x : ℝ) ↦ 4 - 3 * x) := by sorry example : ¬ Bijective (fun (x : ℝ) ↦ 4 - 3 * x) := by sorry

Prove or disprove that the function \(x \mapsto x^2+2x\) from \(\mathbb{R}\) to \(\mathbb{R}\) is bijective.

example : Bijective (fun (x : ℝ) ↦ x ^ 2 + 2 * x) := by sorry example : ¬ Bijective (fun (x : ℝ) ↦ x ^ 2 + 2 * x) := by sorry

Consider the following finite inductive type Element, and the following function \(e\) from the Element type to itself. Prove or disprove that the function \(e\) is bijective.

inductive Element | fire | water | earth | air deriving DecidableEq open Element def e : Element → Element | fire => earth | water => air | earth => fire | air => water example : Bijective e := by sorry example : ¬ Bijective e := by sorry

Show that for all functions \(f\) from the Subatomic type (Example 8.2.4) to itself, if \(f\) is injective then it is bijective.

This is like Example 8.2.6, but with more cases to check.

example : ∀ f : Subatomic → Subatomic, Injective f → Bijective f := by sorry

Consider the finite inductive type Element from a previous exercise. Show that for all functions \(f\) from the Element type to itself, if \(f\) is injective then it is bijective.

This is like Example 8.2.6 and the previous exercise, but with even more (frankly, way too many ….) cases to check.

example : ∀ f : Element → Element, Injective f → Bijective f := by sorry

## 8.3. Composition of functions

### 8.3.1. Definition

Definition

The *composition* of the function \(g : Y \to Z\) with the function \(f : X \to Y\) is the
function from \(X\) to \(Z\) which sends \(x\) to \(g(f(x))\).

```
def comp (f : X → Y) (g : Y → Z) (x : X) : Z := g (f x)
```

The composition of \(g : Y \to Z\) with \(f : X \to Y\) is denoted \(g \circ f\) (in
Lean, `g ∘ f`

).

### 8.3.2. Example

Problem

Let \(f:\mathbb{R}\to\mathbb{R}\) be the function defined by, \(f(a)=a+3\). Let \(g:\mathbb{R}\to\mathbb{R}\) be the function defined by, \(g(b)=2b\). Let \(h:\mathbb{R}\to\mathbb{R}\) be the function defined by, \(h(c)=2c+6\).

Show that \(g \circ f = h\).

Solution

Let \(x\) be a real number. Then

In the Lean proof, note the new tactic `ext`

. To prove two functions are equal, we have to
show that they are equal on every input. This is what the tactic `ext`

does. (The name stands
for “extensionality”.) Before we use it, the goal state is

```
⊢ g ∘ f = h
```

After we use it, the goal state is

```
x : ℝ
⊢ (g ∘ f) x = h x
```

Here is the full Lean proof.

```
def f (a : ℝ) : ℝ := a + 3
def g (b : ℝ) : ℝ := 2 * b
def h (c : ℝ) : ℝ := 2 * c + 6
example : g ∘ f = h := by
ext x
calc (g ∘ f) x = g (f x) := by rfl
_ = 2 * (x + 3) := by rfl
_ = 2 * x + 6 := by ring
_ = h x := by rfl
```

### 8.3.3. Definition

Definition

The *identity function* \(\operatorname{Id}_X:X\to X\) is the function which sends each
\(x\) of type \(X\) to itself.

```
def id (x : X) : X := x
```

### 8.3.4. Example

Problem

Let \(s:\mathbb{R}\to\mathbb{R}\) be the function defined by, \(s(x)=5-x\).

Show that \(s \circ s = \operatorname{Id}_\mathbb{R}\).

Solution

Let \(x\) be a real number. We must show that \(5 - (5 - x) = x\), which is true.

```
def s (x : ℝ) : ℝ := 5 - x
example : s ∘ s = id := by
ext x
dsimp [s]
ring
```

### 8.3.5. Definition

Definition

A function \(g : Y \to X\) is an *inverse* of \(f : X \to Y\), if
\(g \circ f=\operatorname{Id}_X\) and \(f \circ g=\operatorname{Id}_Y\).

```
def Inverse (f : X → Y) (g : Y → X) : Prop := g ∘ f = id ∧ f ∘ g = id
```

### 8.3.6. Example

Consider the following finite inductive type Humour:

```
inductive Humour
| melancholic
| choleric
| phlegmatic
| sanguine
deriving DecidableEq
```

Consider the following function \(p\) from the Humour type to itself.

```
def p : Humour → Humour
| melancholic => choleric
| choleric => sanguine
| phlegmatic => phlegmatic
| sanguine => melancholic
```

Problem

Define a function \(q\) from the Humour type to itself which is inverse to \(p\), and prove this.

```
def q : Humour → Humour
| melancholic => sanguine
| choleric => melancholic
| phlegmatic => phlegmatic
| sanguine => choleric
example : Inverse p q := by
constructor
· ext x
cases x <;> exhaust
· ext x
cases x <;> exhaust
```

### 8.3.7. Example

Proposition

Let \(f : X \to Y\) be a bijective function. Then there exists a function \(g : Y \to X\) which is inverse to \(f\).

Proof

Define a function \(g : Y \to X\) as follows: given \(y\) of type \(Y\), by the surjectivity of \(f\) there exists an \(x\) of type \(X\) such that \(f(x)=y\), and we set \(g(y)\) to be this \(x\). Thus, for all \(y\), it is true that \(f(g(y))=y\). (\(\star\))

This immediately shows that \(f \circ g = \operatorname{Id}_Y\). To show that \(g \circ f = \operatorname{Id}_X\), let \(x\) be of type \(X\). We have, by (\(\star\)), that

so by the injectivity of \(f\), it follows that \((g \circ f)(x) = \operatorname{Id}_X(x)\).

To write this proof in Lean, we need a tactic, `choose`

, 1 which is not used elsewhere in the
book. This tactic constructs the function \(g : Y \to X\)
as described in the first paragraph of the text proof. More precisely, given the hypothesis

```
h_surj: ∀ (b : Y), ∃ a, f a = b
```

the tactic invocation `choose g hg using h_surj`

creates a function consisting of a “choice” of
the `a`

for each `b`

:

```
g : Y → X
hg : ∀ (b : Y), f (g b) = b
```

Here is the full proof in Lean.

```
theorem exists_inverse_of_bijective {f : X → Y} (hf : Bijective f) :
∃ g : Y → X, Inverse f g := by
dsimp [Bijective] at hf
obtain ⟨h_inj, h_surj⟩ := hf
dsimp [Surjective] at h_surj
choose g hg using h_surj
use g
dsimp [Inverse]
constructor
· -- prove `g ∘ f = id`
ext x
dsimp [Injective] at h_inj
apply h_inj
calc f ((g ∘ f) x) = f (g (f x)) := by rfl
_ = f x := by apply hg
_ = f (id x) := by rfl
· -- prove `f ∘ g = id`
ext y
apply hg
```

### 8.3.8. Example

Proposition

Let \(f : X \to Y\) and \(g : Y \to X\) be functions, with \(g : Y \to X\) inverse to \(f : X \to Y\). Then \(f : X \to Y\) is bijective.

Proof

We first show \(f\) is injective. Indeed, let \(x_1\) and \(x_2\) be of type \(X\), and suppose that \(f(x_1)=f(x_2)\). Then

We now show that \(f\) is surjective. Indeed, let \(y\) be of type \(Y\). Then

```
theorem bijective_of_inverse {f : X → Y} {g : Y → X} (h : Inverse f g) :
Bijective f := by
dsimp [Inverse] at h
obtain ⟨hgf, hfg⟩ := h
constructor
· -- `f` is injective
intro x1 x2 hx
calc x1 = id x1 := by rfl
_ = (g ∘ f) x1 := by rw [hgf]
_ = g (f x1) := by rfl
_ = g (f x2) := by rw [hx]
_ = (g ∘ f) x2 := by rfl
_ = id x2 := by rw [hgf]
_ = x2 := by rfl
· -- `f` is surjective
intro y
use g y
calc f (g y) = (f ∘ g) y := by rfl
_ = id y := by rw [hfg]
_ = y := by rfl
```

### 8.3.9. Example

Theorem

Let \(f : X \to Y\) be a function. Then \(f\) is bijective, if and only if there exists a function \(g : Y \to X\) which is inverse to \(f\).

Proof

The first direction is given by Example 8.3.7, and the second direction by Example 8.3.8.

```
theorem bijective_iff_exists_inverse (f : X → Y) :
Bijective f ↔ ∃ g : Y → X, Inverse f g := by
constructor
· apply exists_inverse_of_bijective
· intro h
obtain ⟨g, H⟩ := h
apply bijective_of_inverse H
```

### 8.3.10. Exercises

Consider the following functions \(a\) and \(b\) from the Humour type (see Example 8.3.6) to itself. Write down a function \(c\) from the Humour type to itself, so that \(b \circ a=c\).

When you have the right function written down, the included proof will work.

def a : Humour → Humour | melancholic => sanguine | choleric => choleric | phlegmatic => phlegmatic | sanguine => melancholic def b : Humour → Humour | melancholic => phlegmatic | choleric => phlegmatic | phlegmatic => melancholic | sanguine => sanguine def c : Humour → Humour | melancholic => sorry | choleric => sorry | phlegmatic => sorry | sanguine => sorry example : b ∘ a = c := by ext x cases x <;> exhaust

Consider the function \(u:\mathbb{R}\to\mathbb{R}\) defined by, \(u(x)=5x+1\). Write down a function \(v:\mathbb{R}\to\mathbb{R}\) which is inverse to \(u\), and prove it.

def u (x : ℝ) : ℝ := 5 * x + 1 noncomputable def v (x : ℝ) : ℝ := sorry example : Inverse u v := by sorry

Let \(f : X \to Y\) and \(g : Y \to Z\) be injective functions. Show that \(g \circ f\) is also injective.

example {f : X → Y} (hf : Injective f) {g : Y → Z} (hg : Injective g) : Injective (g ∘ f) := by sorry

Let \(f : X \to Y\) and \(g : Y \to Z\) be surjective functions. Show that \(g \circ f\) is also surjective.

example {f : X → Y} (hf : Surjective f) {g : Y → Z} (hg : Surjective g) : Surjective (g ∘ f) := by sorry

Let \(f : X \to Y\) be a surjective function. Show that there exists a function \(g : Y \to Z\), such that \(f \circ g=\operatorname{Id}_Y\).

example {f : X → Y} (hf : Surjective f) : ∃ g : Y → X, f ∘ g = id := by sorry

Let \(f : X \to Y\) and \(g : Y \to X\) be functions, with \(g\) inverse to \(f\). Show that \(f\) is inverse to \(g\).

example {f : X → Y} {g : Y → X} (h : Inverse f g) : Inverse g f := by sorry

Let \(f : X \to Y\) and \(g_1, g_2 : Y \to X\) be functions, with both \(g_1\) and \(g_1\) inverse to \(f\). Show that \(g_1=g_2\).

This problem says that if a function \(f\) has an inverse, then that inverse is unique.

example {f : X → Y} {g1 g2 : Y → X} (h1 : Inverse f g1) (h2 : Inverse f g2) : g1 = g2 := by sorry

Footnotes

- 1
Experts will recognize this as the axiom of choice.

## 8.4. Product types

### 8.4.1. Example

Problem

Consider the function \(q:\mathbb{Z}\to\mathbb{Z}^2\) defined by, \(q(m)=(m + 1, 2 - m)\). Show that \(q\) is

injective;

not surjective.

Solution

Let \(m_1\) and \(m_2\) be integers and suppose that \(q(m_1)=q(m_2)\). Then by definition

\[(m_1+1,2-m_1)=(m_2+1,2-m_2),\]so \(m_1+1=m_2+1\) and \(2-m_1=2-m_2\), so \(m_1=m_2\).

We will show that there exists \((a,b)\) in \(\mathbb{Z}^2\) such that for all integers \(m\), \(q(m)\ne(a,b)\). Indeed, we will show that \((0,1)\) has this property. Suppose that \(m\) were an integer with \(q(m)=(0,1)\). Then by definition

\[(m+1,2-m)=(0,1),\]so \(m+1=0\) and \(2-m=1\), hence

\[\begin{split}1&=(m+1)+(2-m)-2\\ &=0+1-2\\ &=-1,\end{split}\]contradiction.

To write these proofs in Lean, notice the use of the tactic `obtain`

in the injectivity problem to
convert the hypothesis of a equality in a product type,

```
hm : (m1 + 1, 2 - m1) = (m2 + 1, 2 - m2)
```

to two hypotheses of equality in the two components of the product:

```
hm' : m1 + 1 = m2 + 1
hm'' : 2 - m1 = 2 - m2
```

This is consistent with how you should think about equality in a product type: two ordered pairs are
equal if the two left parts are equal *and* the two right parts are equal. So we use the same
tactic, with the same syntax, as for the logical operator “and”.

```
def q (m : ℤ) : ℤ × ℤ := (m + 1, 2 - m)
example : Injective q := by
dsimp [Injective]
intro m1 m2 hm
dsimp [q] at hm
obtain ⟨hm', hm''⟩ := hm
addarith [hm']
```

The tactic `obtain`

is used similarly in the non-surjectivity problem to break down the hypothesis
of equality in a product type

```
hm : (m + 1, 2 - m) = (0, 1)
```

which arises in that problem.

```
example : ¬ Surjective q := by
dsimp [Surjective]
push_neg
use (0, 1)
intro m hm
dsimp [q] at hm
obtain ⟨hm1, hm2⟩ := hm
have H : 1 = -1 := by addarith [hm1, hm2]
numbers at H
```

### 8.4.2. Example

Problem

Consider the function \((m,n)\mapsto (m + n, m + 2n)\) from \(\mathbb{Z}^2\) to \(\mathbb{Z}^2\). Show that this function is bijective.

Usually, the most efficient way to prove a function is bijective is to produce an inverse for it. This is enough because of the theorem we proved in Example 8.3.9. Coming up with this inverse is something you should do in rough work, probably on paper rather than in Lean. For example, in this problem, you can set up an equation in \((a,b)\) which the inverse has to satisfy:

and simplify to a system of integer equations, and then solve for \(m\) and \(n\):

to conclude that a good candidate for the inverse is the function \((a,b)\mapsto (2a-b, b-a)\) from \(\mathbb{Z}^2\) to \(\mathbb{Z}^2\). But this rough work does not get included in the write-up, either on paper or in Lean. Instead, just produce the inverse out of a hat, and check that it works.

Solution

By Example 8.3.9 it suffices to show that this function has an inverse. We will show that the function \((a,b)\mapsto (2a-b, b-a)\) is inverse to this function.

Firstly, for any \((m,n)\) in \(\mathbb{Z}^2\), we have that

Secondly, for any \((a,b)\) in \(\mathbb{Z}^2\), we have that

In Lean, note

the lemma

`bijective_iff_exists_inverse`

, which is the Lean name for the theorem from Example 8.3.9;the use of the tactic

`ext`

(recall Example 8.3.2) to show that two functions are equal by showing that they are equal on arbitrary input.

```
example : Bijective (fun ((m, n) : ℤ × ℤ) ↦ (m + n, m + 2 * n)) := by
rw [bijective_iff_exists_inverse]
use fun (a, b) ↦ (2 * a - b, b - a)
constructor
· ext ⟨m, n⟩
dsimp
ring
· ext ⟨a, b⟩
dsimp
ring
```

### 8.4.3. Example

The ideas of Example 8.4.2 can be adapted fairly flexibly, particularly over the rationals and over the reals. Try this one yourself.

Problem

Consider the function \((m,n)\mapsto (m + n, m - n)\) from \(\mathbb{R}^2\) to \(\mathbb{R}^2\). Show that this function is bijective.

```
example : Bijective (fun ((m, n) : ℝ × ℝ) ↦ (m + n, m - n)) := by
sorry
```

But over the integers, complications can ensue. You’ll find that the inverse you come up with for
the previous example involves a division, which works fine over \(\mathbb{R}\) but doesn’t work
over \(\mathbb{Z}\). And in fact in this case the function is *not* bijective as a map from
\(\mathbb{Z}^2\) to \(\mathbb{Z}^2\).

Problem

Consider the function \((m,n)\mapsto (m + n, m - n)\) from \(\mathbb{Z}^2\) to \(\mathbb{Z}^2\). Show that this function is not bijective.

Solution

We will show that the function is not surjective. In fact, we will show that for all \((m,n)\) in \(\mathbb{Z}^2\), it is not true that \((m + n, m - n)=(0,1)\). So let \((m,n)\) be in \(\mathbb{Z}^2\) and suppose that \((m + n, m - n)=(0,1)\). Then \(m+n=0\) and \(m-n=1\), so

contradiction.

The last part of the problem could play out in several different ways. The hypotheses \(m+n=0\) and \(m-n=1\) are pretty clearly contradictory (for integers), so there are several variant ways you could produce the contradiction instead of the numeric contradiction \(0\equiv 1\mod 2\) which I produced here.

```
example : ¬ Bijective (fun ((m, n) : ℤ × ℤ) ↦ (m + n, m - n)) := by
dsimp [Bijective, Injective, Surjective]
push_neg
right
use (0, 1)
intro (m, n) h
dsimp at h
obtain ⟨h1, h2⟩ := h
have :=
calc 0 ≡ 2 * m [ZMOD 2] := by extra
_ = (m - n) + (m + n) := by ring
_ = 1 + 0 := by rw [h1, h2]
_ = 1 := by numbers
numbers at this
```

### 8.4.4. Example

Problem

Consider the function \((x,y)\mapsto (x+y,x-y, y)\) from \(\mathbb{R}^2\) to \(\mathbb{R}^3\). Show that this function is injective.

Solution

Let \((x_1,y_1)\) and \((x_2,y_2)\) be points in \(\mathbb{R}^2\) and suppose that

Then, inspecting co-ordinate by co-ordinate, we have that

Subtracting the third equation from the first, we also have that \(x_1=x_2\). So \((x_1,y_1)=(x_2,y_2)\).

In Lean, note the use of the tactic `constructor`

to reduce a goal of equality in a product type,

```
⊢ (x1, y1) = (x2, y2)
```

to two simpler goals, one for each co-ordinate:

```
⊢ x1 = x2
⊢ y1 = y2
```

As with the use of `obtain`

for hypotheses of equality in a product type (recall
Example 8.4.1), the point is that an equality in a product type is
effectively an “and” statement about equality in the first and the second co-ordinates.

```
example : Injective (fun ((x, y) : ℝ × ℝ) ↦ (x + y, x - y, y)) := by
intro (x1, y1) (x2, y2) h
dsimp at h
obtain ⟨h, h', hy⟩ := h
constructor
· addarith [h, hy]
· apply hy
```

### 8.4.5. Example

Problem

Consider the function \((x,y)\mapsto x + y\) from \(\mathbb{R}^2\) to \(\mathbb{R}\). Show that this function is

not injective;

surjective.

Solution

1. We will show that there exist points \((x_1,y_1)\) and \((x_2,y_2)\) in \(\mathbb{R}^2\) such that \(x_1+y_1=x_2+y_2\) and \((x_1,y_1)\ne (x_2,y_2)\). Indeed, consider the points \((0,0)\) and \((1,-1)\). We have that \(0+0=1+-1\) and \((0,0)\ne (1,-1)\).

2. Let \(a\) be a real number. We must show that there exists a point \((x,y)\) in \(\mathbb{R}^2\) such that \(x+y=a\). Indeed, \(a+0=a\), so \((a,0)\) has this property.

```
example : ¬ Injective (fun ((x, y) : ℝ × ℝ) ↦ x + y) := by
dsimp [Injective]
push_neg
use (0, 0), (1, -1)
dsimp
constructor
· numbers
· numbers
example : Surjective (fun ((x, y) : ℝ × ℝ) ↦ x + y) := by
intro a
use (a, 0)
dsimp
ring
```

### 8.4.6. Example

Problem

Consider the function \((m,n)\mapsto 5m+8n\) from \(\mathbb{Z}^2\) to \(\mathbb{Z}\). Show that this function is

not injective;

surjective.

Solution

1. We will show that there exist pairs \((m_1,n_1)\) and \((m_2,n_2)\) in \(\mathbb{Z}^2\) such that \(5m_1+8n_1=5m_2+8n_2\) and \((m_1,n_1)\ne (m_2,n_2)\). Indeed, consider the pairs \((0,0)\) and \((8,-5)\). We have that \(5\cdot 0+8\cdot 0=5\cdot 8+8\cdot -5\) and \((0,0)\ne (8,-5)\).

2. Let \(a\) be an integer. We must show that there exists a pair \((m,n)\) in \(\mathbb{Z}^2\) such that \(5m+8n=a\). Indeed, \(5(-3a)+8(2a)=a\), so \((-3a,2a)\) has this property.

(Where did the idea for the -3 and the 2 come from in the second part of this proof? Compare with Example 3.5.1 and Example 3.5.3.)

```
example : ¬ Injective (fun ((m, n) : ℤ × ℤ) ↦ 5 * m + 8 * n) := by
dsimp [Injective]
push_neg
use (0, 0), (8, -5)
constructor
· numbers
· numbers
example : Surjective (fun ((m, n) : ℤ × ℤ) ↦ 5 * m + 8 * n) := by
intro a
use (-3 * a, 2 * a)
dsimp
ring
```

### 8.4.7. Example

Problem

Consider the function \((m,n)\mapsto 5m+10n\) from \(\mathbb{Z}^2\) to \(\mathbb{Z}\). Show that this function is

not injective;

not surjective.

We leave the non-injectivity proof as an exercise; it is similar to that in the previous two problems.

Solution

(Non-surjectivity) We will show that there exists an integer \(x\) such that for all pairs \((m,n)\) of integers, \(5m+10n\ne x\). Indeed, let us show that 1 has this property. Let \((m,n)\) be a pair of integers and suppose that \(5m+10n=1\). Then

contradiction.

```
example : ¬ Injective (fun ((m, n) : ℤ × ℤ) ↦ 5 * m + 10 * n) := by
sorry
example : ¬ Surjective (fun ((m, n) : ℤ × ℤ) ↦ 5 * m + 10 * n) := by
dsimp [Surjective]
push_neg
use 1
intro (m, n) h
dsimp at h
have :=
calc 0 ≡ 5 * (m + 2 * n) [ZMOD 5] := by extra
_ = 5 * m + 10 * n := by ring
_ = 1 := h
numbers at this
```

### 8.4.8. Example

Problem

Consider the function \(g:\mathbb{R}^2\to \mathbb{R}^2\) defined by, \(g(x,y)=(y,x)\). Show that \(g\circ g=\operatorname{Id}_\mathbb{R}\).

Solution

Let \((x,y)\) be a point in \(\mathbb{R}^2\). Then

```
def g : ℝ × ℝ → ℝ × ℝ
| (x, y) => (y, x)
example : g ∘ g = id := by
ext ⟨x, y⟩
dsimp [g]
```

### 8.4.9. Example

Theorem

There exists a bijection from \(\mathbb{N}^2\) to \(\mathbb{N}\).

First recall the sequence \(A_n\) from Example 6.2.4; we prove a lemma about it.

```
def A : ℕ → ℕ
| 0 => 0
| n + 1 => A n + n + 1
theorem A_mono {n m : ℕ} (h : n ≤ m) : A n ≤ A m := by
induction_from_starting_point m, h with k hk IH
· extra
· calc A n ≤ A k := IH
_ ≤ A k + (k + 1) := by extra
_ = A k + k + 1 := by ring
_ = A (k + 1) := by rw [A]
```

And a corollary, more difficult.

```
theorem of_A_add_mono {a1 a2 b1 b2 : ℕ} (h : A (a1 + b1) + b1 ≤ A (a2 + b2) + b2) :
a1 + b1 ≤ a2 + b2 := by
obtain h' | h' : _ ∨ a2 + b2 + 1 ≤ a1 + b1 := le_or_lt (a1 + b1) (a2 + b2)
· apply h'
rw [← not_lt] at h
have :=
calc A (a2 + b2) + b2
< A (a2 + b2) + b2 + (a2 + 1) := by extra
_ = A (a2 + b2) + (a2 + b2) + 1 := by ring
_ = A ((a2 + b2) + 1) := by rw [A]
_ = A (a2 + b2 + 1) := by ring
_ ≤ A (a1 + b1) := A_mono h'
_ ≤ A (a1 + b1) + b1 := by extra
contradiction
```

We use the sequence \(A_n\) to define the function \(p:\mathbb{N}^2\to \mathbb{N}\) which will be the bijection we seek: \(p(a,b)=A_{a+b}+b\).

```
def p : ℕ × ℕ → ℕ
| (a, b) => A (a + b) + b
```

Finally we prove that this function \(p\) is indeed bijective. We set up an “intertwining”
map \(i\) for \(p\), and invoke the lemma `surjective_of_intertwining`

proved in the exercises
to Section 8.1.

```
def i : ℕ × ℕ → ℕ × ℕ
| (0, b) => (b + 1, 0)
| (a + 1, b) => (a, b + 1)
theorem p_comp_i (x : ℕ × ℕ) : p (i x) = p x + 1 := by
match x with
| (0, b) =>
calc p (i (0, b)) = p (b + 1, 0) := by rw [i]
_ = A ((b + 1) + 0) + 0 := by dsimp [p]
_ = A (b + 1) := by ring
_ = A b + b + 1 := by rw [A]
_ = (A (0 + b) + b) + 1 := by ring
_ = p (0, b) + 1 := by dsimp [p]
| (a + 1, b) =>
calc p (i (a + 1, b)) = p (a, b + 1) := by rw [i] ; rfl -- FIXME
_ = A (a + (b + 1)) + (b + 1) := by dsimp [p]
_ = (A ((a + 1) + b) + b) + 1 := by ring
_ = p (a + 1, b) + 1 := by rw [p]
example : Bijective p := by
constructor
· intro (a1, b1) (a2, b2) hab
dsimp [p] at hab
have H : a1 + b1 = a2 + b2
· apply le_antisymm
· apply of_A_add_mono
rw [hab]
· apply of_A_add_mono
rw [hab]
have hb : b1 = b2
· zify at hab ⊢
calc (b1:ℤ) = A (a2 + b2) + b2 - A (a1 + b1) := by addarith [hab]
_ = A (a2 + b2) + b2 - A (a2 + b2) := by rw [H]
_ = b2 := by ring
constructor
· zify at hb H ⊢
addarith [H, hb]
· apply hb
· apply surjective_of_intertwining (x0 := (0, 0)) (i := i)
· calc p (0, 0) = A (0 + 0) + 0 := by dsimp [p]
_ = A 0 := by ring
_ = 0 := by rw [A]
· intro x
apply p_comp_i
```

### 8.4.10. Exercises

Consider the function \((r,s)\mapsto (s, r-s)\) from \(\mathbb{Q}^2\) to \(\mathbb{Q}^2\). Show that this function is bijective.

example : Bijective (fun ((r, s) : ℚ × ℚ) ↦ (s, r - s)) := by rw [bijective_iff_exists_inverse] sorry

Consider the function \((x,y)\mapsto x-2y-1\) from \(\mathbb{Z}^2\) to \(\mathbb{Z}\). Show that this function is

not injective;

surjective.

example : ¬ Injective (fun ((x, y) : ℤ × ℤ) ↦ x - 2 * y - 1) := by sorry

example : Surjective (fun ((x, y) : ℤ × ℤ) ↦ x - 2 * y - 1) := by sorry

Consider the function \((x,y)\mapsto x^2+y^2\) from \(\mathbb{Q}^2\) to \(\mathbb{Q}\). Show that this function is not surjective.

example : ¬ Surjective (fun ((x, y) : ℚ × ℚ) ↦ x ^ 2 + y ^ 2) := by sorry

Consider the function \((x,y)\mapsto x^2-y^2\) from \(\mathbb{Q}^2\) to \(\mathbb{Q}\). Show that this function is surjective.

example : Surjective (fun ((x, y) : ℚ × ℚ) ↦ x ^ 2 - y ^ 2) := by sorry

Consider the function \((a,b)\mapsto a^b\) from \(\mathbb{Q}× \mathbb{N}\) to \(\mathbb{Q}\). Show that this function is surjective.

example : Surjective (fun ((a, b) : ℚ × ℕ) ↦ a ^ b) := by sorry

Consider the function \((x,y,z)\mapsto (x+y+z,x+2y+3z)\) from \(\mathbb{R}^3\) to \(\mathbb{R}^2\). Show that this function is not injective.

example : ¬ Injective (fun ((x, y, z) : ℝ × ℝ × ℝ) ↦ (x + y + z, x + 2 * y + 3 * z)) := by sorry

Consider the function \((x,y)\mapsto (x+y,x+2y, x+3y)\) from \(\mathbb{R}^2\) to \(\mathbb{R}^3\). Show that this function is injective.

example : Injective (fun ((x, y) : ℝ × ℝ) ↦ (x + y, x + 2 * y, x + 3 * y)) := by sorry

Consider the function \(h:\mathbb{R}^3\to \mathbb{R}^3\) defined by, \(h(x,y,z)=(y,z,x)\). Show that \(h\circ h\circ h=\operatorname{Id}_\mathbb{R}\).

def h : ℝ × ℝ × ℝ → ℝ × ℝ × ℝ | (x, y, z) => (y, z, x) example : h ∘ h ∘ h = id := by sorry