# 9. Sets

This chapter introduces the language of *sets*, a convenient way to reason about the
objects in a type which have some property. This language includes
the concept of *membership* in a set, the property of a set being a *subset* of
another set, and a whole zoo of set operations, such as *intersection*, *union* and
*complement*, each of which is a wrapper for a logical symbol relating
the underlying properties.

In the last section of the chapter, Section 9.3, we study the collection of sets in a type as a type in its own right.

## 9.1. Introduction

### 9.1.1. Example

In type theory, the logical foundation for this book, a *set* in a type \(X\) is specified
by a predicate on \(X\). For example, “the set of integers \(n\) such that \(n\le 3\)”
is a set in \(\mathbb{Z}\).

There is a standard notation for sets specified by predicates. For example, the set described above is written notationally as \(\{n:\mathbb{Z} \mid n\le 3\}\). Here is that set in Lean.

```
#check {n : ℤ | n ≤ 3}
```

Note that the infoview confirms that the type of the expression is `Set ℤ`

, a set of integers.

A term of type \(X\) *belongs to* a set in \(X\) specified by some predicate, if the
predicate holds for that term.

Problem

Show that the integer 1 belongs to the set of integers \(\{n:\mathbb{Z} \mid n\le 3\}\).

Solution

\(1\le 3\).

Other phrasings you may see for this concept are that 1 *is a member of* the set
\(\{n:\mathbb{Z} \mid n\le 3\}\), or *is in* \(\{n:\mathbb{Z} \mid n\le 3\}\). The notation is
\(1\in \{n:\mathbb{Z} \mid n\le 3\}\).

Here is this proof in Lean:

```
example : 1 ∈ {n : ℤ | n ≤ 3} := by
dsimp
numbers
```

The tactic `dsimp`

unfolds the definition of the set and of membership in that set, reducing it
to the goal

```
⊢ 1 ≤ 3
```

which is resolved by `numbers`

.

### 9.1.2. Example

The symbol \(\notin\) is used for the negation of \(\in\).

Problem

Prove that \(10\notin \{n:\mathbb{N} \mid n\text{ is odd}\}\).

Solution

Since \(10=2\cdot 5\), we have that 10 is even, so it is not odd.

In the Lean proof below, the tactic `dsimp`

cleans up the goal to

```
⊢ ¬Odd 10
```

which can then be solved by general-purpose methods.

```
example : 10 ∉ {n : ℕ | Odd n} := by
dsimp
rw [← even_iff_not_odd]
use 5
numbers
```

### 9.1.3. Example

Definition

Let \(U\) and \(V\) be sets in the type \(X\). The set \(U\) *is a subset of*
the set \(V\), if for all \(x\) of type \(X\), if \(x\in U\), then \(x\in V\).

The statement “\(U\) *is a subset of* \(V\)” is expressed in notation as
\(U \subseteq V\).

In Lean the definition looks like this:

```
def Set.Subset (U V : Set α) : Prop := ∀ ⦃x⦄, x ∈ U → x ∈ V
```

and the notation is `U ⊆ V`

.

Problem

Show that \(\{a:\mathbb{N} \mid 4\mid a\}\subseteq\{b:\mathbb{N} \mid 2\mid b\}\).

Solution

We will show that for all natural numbers \(a\), if \(4\mid a\) then \(2\mid a\). Indeed, let \(a\) be a natural number and suppose that \(4\mid a\). Then there exists a natural number \(k\) such that \(a=4k\), so

so \(2\mid a\).

Here is that solution in Lean. Note that after unfolding the definition using `dsimp`

the goal state is simplified to

```
⊢ ∀ (x : ℕ), 4 ∣ x → 2 ∣ x
```

```
example : {a : ℕ | 4 ∣ a} ⊆ {b : ℕ | 2 ∣ b} := by
dsimp [Set.subset_def] -- optional
intro a ha
obtain ⟨k, hk⟩ := ha
use 2 * k
calc a = 4 * k := hk
_ = 2 * (2 * k) := by ring
```

You can also check that the proof goes through without the `dsimp`

line.

### 9.1.4. Example

The notation \(\not\subseteq\) stands for “not a subset of”.

Problem

Prove that \(\{x:\mathbb{R} \mid 0 \le x^2\}\not\subseteq \{t:\mathbb{R} \mid 0\le t\}\).

Solution

We will show that there exists a real number \(x\), such that \(0\le x^2\) and \(x<0\). Indeed, \(0\le (-3)^2\) and \(-3<0\).

In Lean, after unfolding the definitions and negation-normalizing, the goal shows as

```
⊢ ∃ x, 0 ≤ x ^ 2 ∧ x < 0
```

This is the reformulation we state in the first sentence of the text proof.

```
example : {x : ℝ | 0 ≤ x ^ 2} ⊈ {t : ℝ | 0 ≤ t} := by
dsimp [Set.subset_def]
push_neg
use -3
constructor
· numbers
· numbers
```

### 9.1.5. Example

To show that two sets are equal in Lean, we show that something is a member of one if and only if
it is a member of the other. This is called the *set extensionality* property – compare with the
*functional extensionality* property discussed in Example 8.3.2.

Problem

Prove that \(\{x:\mathbb{Z} \mid x\text{ is odd}\}= \{a:\mathbb{Z} \mid \exists k:\mathbb{Z}, a = 2k - 1\}\).

Solution

Let \(x\) be an integer. We must show that \(x\) is odd if and only if there exists an integer \(k\) such that \(x=2k-1\).

First, suppose that \(x\) is odd. Then there exists an integer \(l\) such that \(x=2l+1\). So

Conversely, suppose that there exists an integer \(k\) such that \(x=2k-1\). Then

so \(x\) is odd.

In Lean, as usual, we invoke an extensionality property using the tactic `ext`

. After unfolding
the definitions, the goal displays as

```
⊢ Int.Odd x ↔ ∃ k, x = 2 * k - 1
```

This is the reformulation of the problem which we had stated in the first paragraph of the text proof.

Here is the full proof in Lean.

```
example : {x : ℤ | Int.Odd x} = {a : ℤ | ∃ k, a = 2 * k - 1} := by
ext x
dsimp
constructor
· intro h
obtain ⟨l, hl⟩ := h
use l + 1
calc x = 2 * l + 1 := by rw [hl]
_ = 2 * (l + 1) - 1 := by ring
· intro h
obtain ⟨k, hk⟩ := h
use k - 1
calc x = 2 * k - 1 := by rw [hk]
_ = 2 * (k - 1) + 1 := by ring
```

### 9.1.6. Example

And to show that two sets are not equal in Lean, we produce an element of one which is not an element of the other.

Problem

Show that \(\{a:\mathbb{N} \mid 4\mid a\}\ne\{b:\mathbb{N} \mid 2\mid b\}\).

Solution

We will show that there exists a natural number \(x\) such that \(2\mid x\) and \(4\not\mid 6\).

Indeed, let us show that \(6\) has this property. We have that \(6=2\cdot 3\), so \(2\mid 6\), and \(4\cdot 1 < 6 < 4 \cdot 2\), so \(4\not\mid 6\).

In Lean, after applying set extensionality, unfolding the definitions and negation-normalizing, the goal state shows as

```
⊢ ∃ x, 4 ∣ x ∧ ¬2 ∣ x ∨ ¬4 ∣ x ∧ 2 ∣ x
```

At this point we indicate our witness, 6, and specify that we will prove the right alternative,
`¬4 ∣ 6 ∧ 2 ∣ 6`

.

```
example : {a : ℕ | 4 ∣ a} ≠ {b : ℕ | 2 ∣ b} := by
ext
dsimp
push_neg
use 6
right
constructor
· apply Nat.not_dvd_of_exists_lt_and_lt
use 1
constructor <;> numbers
· use 3
numbers
```

### 9.1.7. Example

Problem

Prove or disprove that \(\{k:\mathbb{Z} \mid 8\mid 5k\}=\{l:\mathbb{Z} \mid 8\mid l\}\).

Solution

The statement is true.

Let \(n\) be an integer. We will show that \(5n\) is a multiple of 8 if and only if \(n\) is.

First, suppose that \(8\mid 5n\). Then there exists an integer \(a\) such that \(5n=8a\). So

so \(8\mid n\).

Conversely, suppose that \(8\mid n\). Then there exists an integer \(a\) such that \(n=8a\). So

so \(8\mid 5n\).

This problem turned out to be a disguised version of Example 4.2.2!

```
example : {k : ℤ | 8 ∣ 5 * k} = {l : ℤ | 8 ∣ l} := by
ext n
dsimp
constructor
· intro hn
obtain ⟨a, ha⟩ := hn
use -3 * a + 2 * n
calc
n = -3 * (5 * n) + 16 * n := by ring
_ = -3 * (8 * a) + 16 * n := by rw [ha]
_ = 8 * (-3 * a + 2 * n) := by ring
· intro hn
obtain ⟨a, ha⟩ := hn
use 5 * a
calc 5 * n = 5 * (8 * a) := by rw [ha]
_ = 8 * (5 * a) := by ring
```

### 9.1.8. Example

There is a special notation \(\{1,2,3\}\) to refer to a finite set whose only elements are those listed, here 1, 2 and 3. By definition, \(\{1,2,3\}\) means \(\{x \mid x = 1 \lor x = 2 \lor x = 3\}\). (The type, like \(\mathbb{N}\) or \(\mathbb{R}\), is usually inferred from context.)

Problem

Prove that \(\{x:\mathbb{R} \mid x^2-x-2=0\}=\{-1, 2\}\).

Solution

Let \(x\) be a real number. We must show that \(x ^ 2 - x - 2 = 0\) if and only if \(x=-1\) or \(x=2\).

First, suppose that \(x ^ 2 - x - 2 = 0\). Then

so either \(x+1=0\) or \(x-2=0\). If the former, \(x=-1\). If the latter, \(x=2\).

Conversely, suppose that \(x=-1\) or \(x=2\).

**Case 1** (\(x=-1\)): Then

**Case 1** (\(x=2\)): Then

In Lean, after applying set extensionality and unfolding the definitions, the goal is

```
x ^ 2 - x - 2 = 0 ↔ x = -1 ∨ x = 2
```

and we start the written proof by explaining this.

```
example : {x : ℝ | x ^ 2 - x - 2 = 0} = {-1, 2} := by
ext x
dsimp
constructor
· intro h
have hx :=
calc
(x + 1) * (x - 2) = x ^ 2 - x - 2 := by ring
_ = 0 := by rw [h]
rw [mul_eq_zero] at hx
obtain hx | hx := hx
· left
addarith [hx]
· right
addarith [hx]
· intro h
obtain h | h := h
· calc x ^ 2 - x - 2 = (-1) ^ 2 - (-1) - 2 := by rw [h]
_ = 0 := by numbers
· calc x ^ 2 - x - 2 = 2 ^ 2 - 2 - 2 := by rw [h]
_ = 0 := by numbers
```

### 9.1.9. Example

Problem

Prove that \(\{1,3,6\} \subseteq\{x:\mathbb{Q} \mid t<10\}\).

Solution

We must show that for all real numbers \(t\), if \(t=1\) or \(t=3\) or \(t=6\) then \(t<10\). Indeed, \(1<10\), \(3<10\) and \(6<10\).

```
example : {1, 3, 6} ⊆ {t : ℚ | t < 10} := by
dsimp [Set.subset_def]
intro t ht
obtain h1 | h3 | h6 := ht
· addarith [h1]
· addarith [h3]
· addarith [h6]
```

### 9.1.10. Exercises

Prove or disprove that \(4\in \{a:\mathbb{Q} \mid a<3\}\).

example : 4 ∈ {a : ℚ | a < 3} := by sorry example : 4 ∉ {a : ℚ | a < 3} := by sorry

Prove or disprove that \(6\in \{n:\mathbb{N} \mid n\mid 42\}\).

example : 6 ∈ {n : ℕ | n ∣ 42} := by sorry example : 6 ∉ {n : ℕ | n ∣ 42} := by sorry

Prove or disprove that \(8\in \{k:\mathbb{Z} \mid 5\mid k\}\).

example : 8 ∈ {k : ℤ | 5 ∣ k} := by sorry example : 8 ∉ {k : ℤ | 5 ∣ k} := by sorry

Prove or disprove that \(11\in \{n:\mathbb{N} \mid n\text{ is odd}\}\).

example : 11 ∈ {n : ℕ | Odd n} := by sorry example : 11 ∉ {n : ℕ | Odd n} := by sorry

Prove or disprove that \(-3\in \{x:\mathbb{R} \mid \forall y :\mathbb{R}, x\le y^2\}\).

example : -3 ∈ {x : ℝ | ∀ y : ℝ, x ≤ y ^ 2} := by sorry example : -3 ∉ {x : ℝ | ∀ y : ℝ, x ≤ y ^ 2} := by sorry

Prove or disprove that \(\{a:\mathbb{N} \mid 20\mid a\}\subseteq \{x:\mathbb{N} \mid 5 \mid x\}\).

example : {a : ℕ | 20 ∣ a} ⊆ {x : ℕ | 5 ∣ x} := by sorry example : {a : ℕ | 20 ∣ a} ⊈ {x : ℕ | 5 ∣ x} := by sorry

Prove or disprove that \(\{a:\mathbb{N} \mid 5\mid a\}\subseteq \{x:\mathbb{N} \mid 20 \mid x\}\).

example : {a : ℕ | 5 ∣ a} ⊆ {x : ℕ | 20 ∣ x} := by sorry example : {a : ℕ | 5 ∣ a} ⊈ {x : ℕ | 20 ∣ x} := by sorry

Prove or disprove that \(\{r:\mathbb{Z} \mid 3\mid r\}\subseteq \{s:\mathbb{Z} \mid 0 \le s\}\).

example : {r : ℤ | 3 ∣ r} ⊆ {s : ℤ | 0 ≤ s} := by sorry example : {r : ℤ | 3 ∣ r} ⊈ {s : ℤ | 0 ≤ s} := by sorry

Prove or disprove that \(\{m:\mathbb{Z} \mid m\ge 10\}\subseteq \{n:\mathbb{Z} \mid n^3-7n^2\geq 4n\}\).

example : {m : ℤ | m ≥ 10} ⊆ {n : ℤ | n ^ 3 - 7 * n ^ 2 ≥ 4 * n} := by sorry example : {m : ℤ | m ≥ 10} ⊈ {n : ℤ | n ^ 3 - 7 * n ^ 2 ≥ 4 * n} := by sorry

Prove or disprove that \(\{n:\mathbb{Z} n\mid\text{ is even}\}=\{a:\mathbb{Z} \mid a\equiv 6\mod 2\}\).

example : {n : ℤ | Even n} = {a : ℤ | a ≡ 6 [ZMOD 2]} := by sorry example : {n : ℤ | Even n} ≠ {a : ℤ | a ≡ 6 [ZMOD 2]} := by sorry

Prove or disprove that \(\{t:\mathbb{R} \mid t^2-5t+4=0\}=\{4\}\).

example : {t : ℝ | t ^ 2 - 5 * t + 4 = 0} = {4} := by sorry example : {t : ℝ | t ^ 2 - 5 * t + 4 = 0} ≠ {4} := by sorry

Prove or disprove that \(\{k:\mathbb{Z} \mid 8\mid 6k\}=\{l:\mathbb{Z} \mid 8\mid l\}\).

example : {k : ℤ | 8 ∣ 6 * k} = {l : ℤ | 8 ∣ l} := by sorry example : {k : ℤ | 8 ∣ 6 * k} ≠ {l : ℤ | 8 ∣ l} := by sorry

Prove or disprove that \(\{k:\mathbb{Z} \mid 7\mid 9k\}=\{l:\mathbb{Z} \mid 7\mid l\}\).

example : {k : ℤ | 7 ∣ 9 * k} = {l : ℤ | 7 ∣ l} := by sorry example : {k : ℤ | 7 ∣ 9 * k} ≠ {l : ℤ | 7 ∣ l} := by sorry

Prove or disprove that \(\{1,2,3\}=\{1,2\}\).

example : {1, 2, 3} = {1, 2} := by sorry example : {1, 2, 3} ≠ {1, 2} := by sorry

Prove that \(\{x:\mathbb{R} \mid x^2+3x+2=0\}=\{-1, -2\}\).

example : {x : ℝ | x ^ 2 + 3 * x + 2 = 0} = {-1, -2} := by sorry

## 9.2. Set operations

### 9.2.1. Example

Definition

The *union* of two sets \(U\) and \(V\) in a type \(X\), denoted \(U \cup V\),
is \(\{x : X \mid x \in U \lor x \in V\}\).

Problem

Let \(t\) be a real number. Show that \(t∈\{x:\mathbb{R}\mid-1<x\}\cup \{x:\mathbb{R}\mid x < 1\}\).

Solution

We must show that either \(-1<t\) or \(t<1\).

**Case 1** (\(t\le 0\)): Then \(t<1\).

**Case 2** (\(t> 0\)): Then \(-1<t\).

After unfolding the definitions in this problem, the goal is to show that

```
⊢ -1 < t ∨ t < 1
```

Here is the full proof in Lean.

```
example (t : ℝ) : t ∈ {x : ℝ | -1 < x} ∪ {x : ℝ | x < 1} := by
dsimp
obtain h | h := le_or_lt t 0
· right
addarith [h]
· left
addarith [h]
```

### 9.2.2. Example

Problem

Show that \(\{1,2\}\cup\{2,4\}=\{1,2,4\}\).

After applying set extensionality and unfolding definitions in this problem, the goal state is

```
n : ℕ
⊢ (n = 1 ∨ n = 2) ∨ n = 2 ∨ n = 4 ↔ n = 1 ∨ n = 2 ∨ n = 4
```

It’s possible to prove this directly – here’s how the start of such a proof would look.

```
example : {1, 2} ∪ {2, 4} = {1, 2, 4} := by
ext n
dsimp
constructor
· intro h
obtain (h | h) | (h | h) := h
· left
apply h
· right
left
apply h
-- and much, much more
· sorry
· sorry
· sorry
```

But there’s a better way: this is pure propositional logic, the situation the tactic `exhaust`

(see
Example 8.1.8) was designed for.

```
example : {2, 1} ∪ {2, 4} = {1, 2, 4} := by
ext n
dsimp
exhaust
```

### 9.2.3. Example

Definition

The *intersection* of two sets \(U\) and \(V\) in a type \(X\), denoted
\(U \cap V\),
is \(\{x : X \mid x \in U \land x \in V\}\).

Problem

Show that \(\{-2,3\}\cap \{x:\mathbb{Q}\mid x^2=9\}\subseteq \{a:\mathbb{Q}\mid 0<a\}\).

Solution

We will show that for all real numbers \(t\), if \(t\) is -2 or 3 and \(t^2=9\) then \(0<t\).

Indeed, let \(t\) be a real number and suppose that \(t\) is -2 or 3 and \(t^2=9\).

**Case 1** (\(t=-2\)): We then have that

contradiction.

**Case 2** (\(t=3\)): Then \(0<t\) as desired.

```
example : {-2, 3} ∩ {x : ℚ | x ^ 2 = 9} ⊆ {a : ℚ | 0 < a} := by
dsimp [Set.subset_def]
intro t h
obtain ⟨(h1 | h1), h2⟩ := h
· have :=
calc (-2) ^ 2 = t ^ 2 := by rw [h1]
_ = 9 := by rw [h2]
numbers at this
· addarith [h1]
```

### 9.2.4. Example

Problem

Show that \(\{n:\mathbb{N}\mid 4\le n\}\cap \{n:\mathbb{N}\mid n<7\}\subseteq\{4,5,6\}\).

```
example : {n : ℕ | 4 ≤ n} ∩ {n : ℕ | n < 7} ⊆ {4, 5, 6} := by
dsimp [Set.subset_def]
intro n h
obtain ⟨h1, h2⟩ := h
interval_cases n <;> exhaust
```

### 9.2.5. Example

Definition

The *complement* of a set \(U\) in a type \(X\), denoted
\(U^{c}\), is \(\{x : X \mid x \notin U\}\).

Problem

Show that \(\{n:\mathbb{Z}\mid n\text{ even}\}^{c}=\{n:\mathbb{N}\mid n\text{ odd}\}\).

Solution

Let \(n\) be an integer. We must show that \(n\) is odd if and only if it is not even. This is precisely Example 4.5.5.

```
example : {n : ℤ | Even n}ᶜ = {n : ℤ | Odd n} := by
ext n
dsimp
rw [odd_iff_not_even]
```

### 9.2.6. Example

The *empty set* in a type \(X\) is the set which has no elements. That’s a slightly informal
description: here’s the strict definition.

Definition

The *empty set* in a type \(X\), denoted \(\emptyset\), is \(\{x : X \mid \operatorname{False}\}\).

It is true by pure logic that no element of type \(X\) belongs to the empty set in \(X\), and that the empty set in \(X\) is a subset of every set in \(X\).

```
example (x : ℤ) : x ∉ ∅ := by
dsimp
exhaust
example (U : Set ℤ) : ∅ ⊆ U := by
dsimp [Set.subset_def]
intro x
exhaust
```

To show a set \(U\) in \(X\) is equal to the empty set, you must show that \(U\) has no elements.

Problem

Show that \(\{n:\mathbb{Z}\mid n\equiv 1\mod 5\}\cap\{n:\mathbb{N}\mid n\equiv 1\mod 5\}=\emptyset\).

Let’s consider the Lean proof first. We can write something like this:

```
example : {n : ℤ | n ≡ 1 [ZMOD 5]} ∩ {n : ℤ | n ≡ 2 [ZMOD 5]} = ∅ := by
ext x
dsimp
constructor
· intro hx
obtain ⟨hx1, hx2⟩ := hx
have :=
calc 1 ≡ x [ZMOD 5] := by rel [hx1]
_ ≡ 2 [ZMOD 5] := by rel [hx2]
numbers at this
· intro hx
contradiction
```

But a certain amount of that proof (the `constructor`

, and the `intro`

/`contradiction`

in the
second branch of the proof) is just logical messing-around. Now that we are familiar with the full
power of the `exhaust`

tactic it is possible to streamline proofs like this. Have a look at the
goal state after the `dsimp`

: it is

```
⊢ x ≡ 1 [ZMOD 5] ∧ x ≡ 2 [ZMOD 5] ↔ False
```

and you might mentally simplify this to the logically equivalent

```
⊢ ¬ (x ≡ 1 [ZMOD 5] ∧ x ≡ 2 [ZMOD 5])
```

This reformulation can be carried out in Lean using the incantation

```
suffices ¬(x ≡ 1 [ZMOD 5] ∧ x ≡ 2 [ZMOD 5]) by exhaust
```

Here is a full proof in Lean using this approach.

```
example : {n : ℤ | n ≡ 1 [ZMOD 5]} ∩ {n : ℤ | n ≡ 2 [ZMOD 5]} = ∅ := by
ext x
dsimp
suffices ¬(x ≡ 1 [ZMOD 5] ∧ x ≡ 2 [ZMOD 5]) by exhaust
intro hx
obtain ⟨hx1, hx2⟩ := hx
have :=
calc 1 ≡ x [ZMOD 5] := by rel [hx1]
_ ≡ 2 [ZMOD 5] := by rel [hx2]
numbers at this
```

And here is that proof in words. We combine the use of set extensionality, the definition-unfolding, and the logically equivalent reformulation into a single paragraph of setup.

Solution

Let \(x\) be an integer. We will show that it is not true that both \(x\equiv 1\mod 5\) and \(x\equiv 2\mod 5\).

Indeed, suppose that \(x\equiv 1\mod 5\) and \(x\equiv 2\mod 5\). Then

contradiction.

### 9.2.7. Example

The *universe set* in a type \(X\) is the set which contains everything in \(X\).
That’s again a slightly informal description: here’s the strict definition.

Definition

The *universe set* in a type \(X\) is \(\{x : X \mid \operatorname{True}\}\).

It is true by pure logic that all elements of type \(X\) belong to the universe set in \(X\), and that every set in \(X\) is a subset of the universe set in \(X\).

```
example (x : ℤ) : x ∈ univ := by dsimp
example (U : Set ℤ) : U ⊆ univ := by
dsimp [Set.subset_def]
intro x
exhaust
```

Note that in Lean the universe set is denoted `univ`

. On paper we often refer to the universe
set of \(X\) as \(X\), too (even though this is not strictly correct).

To show a set \(U\) in \(X\) is equal to the universe set, you must show that \(U\) contains all elements of \(X\). Here we adapt Example 9.2.1 to be a problem about the universe set.

Problem

Show that \(\{x:\mathbb{R}\mid-1<x\}\cup \{x:\mathbb{R}\mid x < 1\}=\mathbb{R}\).

Solution

We must show that for all real numbers \(t\), either \(-1<t\) or \(t<1\).

**Case 1** (\(t\le 0\)): Then \(t<1\).

**Case 2** (\(t> 0\)): Then \(-1<t\).

```
example : {x : ℝ | -1 < x} ∪ {x : ℝ | x < 1} = univ := by
ext t
dsimp
suffices -1 < t ∨ t < 1 by exhaust
obtain h | h := le_or_lt t 0
· right
addarith [h]
· left
addarith [h]
```

### 9.2.8. Exercises

For the first five problems, I provide a tactic `check_equality_of_explicit_sets`

which will prove
the statement if you have formulated it correctly. This tactic simply runs `ext`

, then `dsimp`

,
then `exhaust`

:

```
macro "check_equality_of_explicit_sets" : tactic => `(tactic| (ext; dsimp; exhaust))
```

Write in an explicitly-listed finite set without repeats, or \(\emptyset\), which is equal to \(\{-1,2,4,4\}\cup\{3,-2,2\}\). When you have the correct answer, the given Lean proof will work.

example : {-1, 2, 4, 4} ∪ {3, -2, 2} = sorry := by check_equality_of_explicit_sets

Write in an explicitly-listed finite set without repeats, or \(\emptyset\), which is equal to \(\{-1,2,4,4\}\cup\{3,-2,2\}\). When you have the correct answer, the given Lean proof will work.

example : {0, 1, 2, 3, 4} ∩ {0, 2, 4, 6, 8} = sorry := by check_equality_of_explicit_sets

Write in an explicitly-listed finite set without repeats, or \(\emptyset\), which is equal to \(\{1,2\}\cap\{3\}\). When you have the correct answer, the given Lean proof will work.

example : {1, 2} ∩ {3} = sorry := by check_equality_of_explicit_sets

Write in an explicitly-listed finite set without repeats, or \(\emptyset\), which is equal to \(\{3,4,5\}^c\cap\{1,3,5,7,9\}\). When you have the correct answer, the given Lean proof will work.

example : {3, 4, 5}ᶜ ∩ {1, 3, 5, 7, 9} = sorry := by check_equality_of_explicit_sets

Prove that \(\{r:\mathbb{Z}\mid r\equiv 7\mod 10\}\subseteq \{s:\mathbb{Z}\mid s\equiv 1\mod 2\}\cap\{t:\mathbb{Z}\mid t\equiv 2\mod 5\}\).

example : {r : ℤ | r ≡ 7 [ZMOD 10] } ⊆ {s : ℤ | s ≡ 1 [ZMOD 2]} ∩ {t : ℤ | t ≡ 2 [ZMOD 5]} := by sorry

Prove that \(\{n:\mathbb{Z}\mid 5\mid n\}\cap \{n:\mathbb{Z}\mid 8\mid n\}⊆\{n:\mathbb{Z}\mid 40\mid n\}\).

example : {n : ℤ | 5 ∣ n} ∩ {n : ℤ | 8 ∣ n} ⊆ {n : ℤ | 40 ∣ n} := by sorry

Prove that \(\{n:\mathbb{Z}\mid 3\mid n\}\cup \{n:\mathbb{Z}\mid 2\mid n\}⊆\{n:\mathbb{Z}\mid n^2\equiv 1\mod 6\}^{c}\).

example : {n : ℤ | 3 ∣ n} ∪ {n : ℤ | 2 ∣ n} ⊆ {n : ℤ | n ^ 2 ≡ 1 [ZMOD 6]}ᶜ := by sorry

Let us define that a set \(s\) in a type \(X\) has

*size at least two*, if there exist \(x_1\) and \(x_2\) in \(s\) which are different, and has*size at least three*, if there exist \(x_1\), \(x_2\) and \(x_3\) in \(s\) which are all different.Let \(s\) and \(t\) be sets of size at least two in some type \(X\), and suppose that \(s \cap t\) does not have size at least two. Show that \(s\cup t\) has size at least three.

This problem features a ton of different cases. Use

`exhaust`

liberally to knock off sub-cases.def SizeAtLeastTwo (s : Set X) : Prop := ∃ x1 x2 : X, x1 ≠ x2 ∧ x1 ∈ s ∧ x2 ∈ s def SizeAtLeastThree (s : Set X) : Prop := ∃ x1 x2 x3 : X, x1 ≠ x2 ∧ x1 ≠ x3 ∧ x2 ≠ x3 ∧ x1 ∈ s ∧ x2 ∈ s ∧ x3 ∈ s example {s t : Set X} (hs : SizeAtLeastTwo s) (ht : SizeAtLeastTwo t) (hst : ¬ SizeAtLeastTwo (s ∩ t)) : SizeAtLeastThree (s ∪ t) := by sorry

## 9.3. The type of sets

### 9.3.1. Definition

Let \(X\) be a type. The collection of all sets in \(X\) can itself be considered as a type. This type is sometimes denoted \(\mathcal{P}(X)\). 1 For example, \(\{3,4,5\}\), \(\{n:\mathbb{N}\mid 8<n\}\), and \(\{k:\mathbb{N}\mid\exists \ a, a^2=k\}\) are all sets of natural numbers, which means they are all of type \(\mathcal{P}(\mathbb{N})\).

In Lean, for a type `X`

, the type of sets in `X`

is denoted `Set X`

. Lean
will confirm that the three objects described above all have type `Set ℕ`

:

```
#check {3, 4, 5} -- `{3, 4, 5} : Set ℕ`
#check {n : ℕ | 8 < n} -- `{n | 8 < n} : Set ℕ`
#check {k : ℕ | ∃ a, a ^ 2 = k} -- `{k | ∃ a, a ^ 2 = k} : Set ℕ`
```

This operation can be iterated: you can have sets in the type of sets, and so on.

```
#check {{3, 4}, {4, 5, 6}} -- `{{3, 4}, {4, 5, 6}} : Set (Set ℕ)`
#check {s : Set ℕ | 3 ∈ s} -- `{s | 3 ∈ s} : Set (Set ℕ)`
```

Exercise: write down an object of type `Set (Set (Set ℕ))`

.

### 9.3.2. Example

Problem

Show that \(\{n:\mathbb{N}\mid n\text{ is even}\}\notin\{s:\mathcal{P}(\mathbb{N})\mid 3 ∈s\}\).

Solution

We must show 3 is not even. It suffices to show that 3 is odd. Indeed, \(3=2\cdot 1+1\).

```
example : {n : ℕ | Nat.Even n} ∉ {s : Set ℕ | 3 ∈ s} := by
dsimp
rw [← Nat.odd_iff_not_even]
use 1
numbers
```

### 9.3.3. Example

Since \(\mathcal{P}(X)\), the type of sets in \(X\), is itself a type, we can consider functions to and from it.

For example, given a set \(s\) of natural numbers, we can build a new set \(\{n:\mathbb{N}\mid n+1 \in s\}\). Lean confirms that this operation (let us call it \(p\)) is a function from \(\mathcal{P}(\mathbb{N})\) to \(\mathcal{P}(\mathbb{N})\).

```
def p (s : Set ℕ) : Set ℕ := {n : ℕ | n + 1 ∈ s}
#check @p -- `p : Set ℕ → Set ℕ`
```

Problem

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

Solution

We must show that there exist sets \(s\) and \(t\), such that (i) \(\{n:\mathbb{N}\mid n+1 \in s\} = \{n:\mathbb{N}\mid n+1 \in t\}\), and (ii) \(s \ne t\).

Indeed, let us show that the sets \(\{0\}\) and \(\emptyset\) have this property. We must show, (i) \(\{n:\mathbb{N}\mid n+1 = 0\} = \emptyset\), and (ii) \(\{0\} \ne \emptyset\).

For the first statement, let \(x\) be a natural number. We must show that \(x+1 \ne 0\), which is true since \(x+1 > 0\).

For the second statement, we must show that there exists a natural number \(k\) such that \(k\in\{0\}\) and \(k\notin\emptyset\), or vice versa. Indeed, \(k=0\) has this property.

```
example : ¬ Injective p := by
dsimp [Injective, p]
push_neg
use {0}, ∅
dsimp
constructor
· ext x
dsimp
suffices x + 1 ≠ 0 by exhaust
apply ne_of_gt
extra
· ext
push_neg
use 0
dsimp
exhaust
```

### 9.3.4. Example

Problem

Consider the function \(q : \mathcal{P}(\mathbb{Z})\to \mathcal{P}(\mathbb{Z})\) defined by, \(q(s)=\{n:\mathbb{Z}\mid n+1\in s\}\). Show that the function \(q\) is injective.

Solution

We must show that for all sets \(s\) and \(t\), if \(\{n:\mathbb{Z}\mid n+1 \in s\} = \{n:\mathbb{Z}\mid n+1 \in t\}\), then \(s = t\).

Indeed, let \(s\) and \(t\) be sets and suppose that \(\{n:\mathbb{Z}\mid n+1 \in s\} = \{n:\mathbb{Z}\mid n+1 \in t\}\).

Let \(k\) be an integer. We must show that \(k\in s\) if and only if \(k\in t\). Indeed, by the assumption, \(k -1\in\{n:\mathbb{Z}\mid n+1 \in s\}\) if and only if \(k-1\in \{n:\mathbb{Z}\mid n+1 \in t\}\). Simplifying, \(k -1+1 \in s\) if and only if \(k-1+1\in t\), and so \(k \in s\) if and only if \(k\in t\).

```
def q (s : Set ℤ) : Set ℤ := {n : ℤ | n + 1 ∈ s}
example : Injective q := by
dsimp [Injective, q]
intro s t hst
ext k
have hk : k - 1 ∈ {n | n + 1 ∈ s} ↔ k - 1 ∈ {n | n + 1 ∈ t} := by rw [hst]
dsimp at hk
conv at hk => ring
apply hk
```

### 9.3.5. Example

Problem

Let \(X\) be a type. Prove that there does not exist a surjective function from \(X\) to \(\mathcal{P}(X)\).

Solution

Suppose for the sake of contradiction that some function \(f:X\to\mathcal{P}(X)\) were surjective. We introduce the following set in \(X\):

Since \(f\) is surjective, there exists some \(x\) of type \(X\) such that \(f(x)=s\). We consider cases according to whether \(x\in s\).

**Case 1** (\(x\in s\)): Then by the definition of \(s\), it is true that
\(x\notin f(x)\), so since \(f(x)=s\), we have \(x\notin s\), contradiction.

**Case 2** (\(x\notin s\)): Then by the definition of \(s\), it is false that
\(x\notin f(x)\), so since \(f(x)=s\), we have that it is false that \(x\notin s\),
contradiction.

```
example : ¬ ∃ f : X → Set X, Surjective f := by
intro h
obtain ⟨f, hf⟩ := h
let s : Set X := {x | x ∉ f x}
obtain ⟨x, hx⟩ := hf s
by_cases hxs : x ∈ s
· have hfx : x ∉ f x := hxs
rw [hx] at hfx
contradiction
· have hfx : ¬ x ∉ f x := hxs
rw [hx] at hfx
contradiction
```

The idea behind this twisty proof is sometimes called the barber paradox. Here is the version featuring barbers. There is a town with a barber, and in this town, the barber shaves all men who don’t shave themselves. Paradox: does the barber shave himself?

### 9.3.6. Exercises

Consider the function \(r : \mathcal{P}(\mathbb{N})\to \mathcal{P}(\mathbb{N})\) defined by, \(r(s)=s\cup \{3\}\). Show that \(r\) is not injective.

def r (s : Set ℕ) : Set ℕ := s ∪ {3} example : ¬ Injective r := by sorry

Consider the sequence \(U_n\) of sets of integers defined recursively by,

\[\begin{split}U_0&=\mathbb{Z} \\ \text{for }n:\mathbb{N},\quad U_{n+1} &=\{x:\mathbb{Z}\mid \exists \ y\in U_n, x = 2y \}\end{split}\]Show that for all natural numbers \(n\), \(U_n=\{x:\mathbb{Z}\mid 2^n\mid x\}\).

def U : ℕ → Set ℤ | 0 => univ | n + 1 => {x : ℤ | ∃ y ∈ U n, x = 2 * y} example (n : ℕ) : U n = {x : ℤ | (2:ℤ) ^ n ∣ x} := by simple_induction n with k hk · rw [U] sorry · rw [U] ext x dsimp sorry

Footnotes

- 1
In set theory, which we

*don’t*use as the logical foundation of this book, \(\mathcal{P}(X)\) is referred to as the*power set*of \(X\). Maybe in type theory we should refer to it as the “power type” of \(X\) …?