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

\[\begin{split}a&=4a\\ &=2(2k),\end{split}\]

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

\[\begin{split}x&=2l+1\\ &=2(l+1)-1.\end{split}\]

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

\[\begin{split}x&=2k-1\\ &=2(k-1)+1,\end{split}\]

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

\[\begin{split}n &= -3 (5 n) + 16 n \\ &= -3 (8 a) + 16 n \\ & = 8 (-3 a + 2 n),\end{split}\]

so \(8\mid n\).

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

\[\begin{split}5n &= 5(8a) \\ &= 8(5a),\end{split}\]

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

\[\begin{split}(x+1)(x-2)&=x ^ 2 - x - 2\\ &=0,\end{split}\]

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

\[\begin{split}x^2-x-2&=(-1)^2-(-1)-2\\ &=0.\end{split}\]

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

\[\begin{split}x^2-x-2&=2^2-2-2\\ &=0.\end{split}\]

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

1. 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
   

2. 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
   

3. 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
   

4. 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
   

5. 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
   

6. 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
   

7. 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
   

8. 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
   

9. 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
   

10. 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
    

11. 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
    

12. 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
    

13. 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
    

14. 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
    

15. 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

\[\begin{split}(-2)^2&=t^2\\ &=9,\end{split}\]

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

\[\begin{split}1&\equiv x\mod 5\\ &\equiv 2\mod 5,\end{split}\]

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))

1. 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
   

2. 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
   

3. 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
   

4. 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
   

5. 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
   

6. 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
   

7. 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
   

8. 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\):

\[s :=\{x:X\mid x\notin f(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

1. 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
   

2. 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\) …?