$$ \newcommand{\setmin}{\mathbin{\backslash}} \newcommand{\symmdiff}{\mathbin{∆}} $$

8  Infinite Sets

8.1. Equinumerous Sets

Chapter 8 of HTPI begins by defining a set \(A\) to be equinumerous with a set \(B\) if there is a function \(f : A \to B\) that is one-to-one and onto. As we will see, in Lean we will need to phrase this definition somewhat differently. However, we begin by considering some examples of functions that are one-to-one and onto.

The first example in HTPI is a one-to-one, onto function from \(\mathbb{Z}^+\) to \(\mathbb{Z}\). We will modify this example slightly to make it a function fnz from Nat to Int:

def fnz (n : Nat) : Int := if 2 ∣ n then ↑(n / 2) else -↑((n + 1) / 2)

Note that, to get a result of type Int, coercion is necessary. We have specified that the coercion should be done after the computation of either n / 2 or (n + 1) / 2, with that computation being done using natural-number arithmetic. Checking a few values of this functions suggests a simple pattern:

#eval [fnz 0, fnz 1, fnz 2, fnz 3, fnz 4, fnz 5, fnz 6]
  --Answer: [0, -1, 1, -2, 2, -3, 3]

Perhaps the easiest way to prove that fnz is one-to-one and onto is to define a function that turns out to be its inverse. This time, in order to get the right type for the value of the function, we use the function Int.toNat to convert a nonnegative integer to a natural number.

def fzn (a : Int) : Nat :=
  if a ≥ 0 then 2 * Int.toNat a else 2 * Int.toNat (-a) - 1

#eval [fzn 0, fzn (-1), fzn 1, fzn (-2), fzn 2, fzn (-3), fzn 3]
  --Answer: [0, 1, 2, 3, 4, 5, 6]

To prove that fzn is the inverse of fnz, we begin by proving lemmas making it easier to compute the values of these functions

lemma fnz_even (k : Nat) : fnz (2 * k) = ↑k := by
  have h1 : 2 ∣ 2 * k := by
    apply Exists.intro k
    rfl
    done
  have h2 : fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2)
    else -↑((2 * k + 1) / 2) := by rfl
  rewrite [if_pos h1] at h2  --h2 : fnz (2 * k) = ↑(2 * k / 2)
  have h3 : 0 < 2 := by linarith
  rewrite [Nat.mul_div_cancel_left k h3] at h2
  show fnz (2 * k) = ↑k from h2
  done

lemma fnz_odd (k : Nat) : fnz (2 * k + 1) = -↑(k + 1) := sorry

lemma fzn_nat (k : Nat) : fzn ↑k = 2 * k := by rfl

lemma fzn_neg_succ_nat (k : Nat) : fzn (-↑(k + 1)) = 2 * k + 1 := by rfl

Using these lemmas and reasoning by cases, it is straightforward to prove lemmas confirming that the composition of these functions, in either order, yields the identity function. The cases for the first lemma are based on an exercise from Section 6.1.

lemma fzn_fnz : fzn ∘ fnz = id := by
  apply funext        --Goal : ∀ (x : Nat), (fzn ∘ fnz) x = id x
  fix n : Nat
  rewrite [comp_def]  --Goal : fzn (fnz n) = id n
  have h1 : nat_even n ∨ nat_odd n := Exercise_6_1_16a1 n
  by_cases on h1
  · -- Case 1. h1 : nat_even n
    obtain (k : Nat) (h2 : n = 2 * k) from h1
    rewrite [h2, fnz_even, fzn_nat]
    rfl
    done
  · -- Case 2. h1 : nat_odd n
    obtain (k : Nat) (h2 : n = 2 * k + 1) from h1
    rewrite [h2, fnz_odd, fzn_neg_succ_nat]
    rfl
    done
  done

lemma fnz_fzn : fnz ∘ fzn = id  := sorry

By theorems from Chapter 5, it follows that both fnz and fzn are one-to-one and onto.

lemma fzn_one_one : one_to_one fzn := Theorem_5_3_3_1 fzn fnz fnz_fzn

lemma fzn_onto : onto fzn := Theorem_5_3_3_2 fzn fnz fzn_fnz

lemma fnz_one_one : one_to_one fnz := Theorem_5_3_3_1 fnz fzn fzn_fnz

lemma fnz_onto : onto fnz := Theorem_5_3_3_2 fnz fzn fnz_fzn

We’ll give one more example: a one-to-one, onto function fnnn from Nat × Nat to Nat, whose definition is modeled on a function from \(\mathbb{Z}^+ \times \mathbb{Z}^+\) to \(\mathbb{Z}^+\) in HTPI. The definition of fnnn will use numbers of the form k * (k + 1) / 2. These numbers are sometimes called triangular numbers, because they count the number of objects in a triangular grid with k rows.

def tri (k : Nat) : Nat := k * (k + 1) / 2

def fnnn (p : Nat × Nat) : Nat := tri (p.1 + p.2) + p.1

lemma fnnn_def (a b : Nat) : fnnn (a, b) = tri (a + b) + a := by rfl

#eval [fnnn (0, 0), fnnn (0, 1), fnnn (1, 0), fnnn (0, 2), fnnn (1, 1)]
  --Answer: [0, 1, 2, 3, 4]

Two simple lemmas about tri will help us prove the important properties of fnnn:

lemma tri_step (k : Nat) : tri (k + 1) = tri k + k + 1 := sorry

lemma tri_incr {j k : Nat} (h1 : j ≤ k) : tri j ≤ tri k := sorry

lemma le_of_fnnn_eq {a1 b1 a2 b2 : Nat}
    (h1 : fnnn (a1, b1) = fnnn (a2, b2)) : a1 + b1 ≤ a2 + b2 := by
  by_contra h2
  have h3 : a2 + b2 + 1 ≤ a1 + b1 := by linarith
  have h4 : fnnn (a2, b2) < fnnn (a1, b1) :=
    calc fnnn (a2, b2)
      _ = tri (a2 + b2) + a2 := by rfl
      _ < tri (a2 + b2) + (a2 + b2) + 1 := by linarith
      _ = tri (a2 + b2 + 1) := (tri_step _).symm
      _ ≤ tri (a1 + b1) := tri_incr h3
      _ ≤ tri (a1 + b1) + a1 := by linarith
      _ = fnnn (a1, b1) := by rfl
  linarith
  done

lemma fnnn_one_one : one_to_one fnnn := by
  fix (a1, b1) : Nat × Nat
  fix (a2, b2) : Nat × Nat
  assume h1 : fnnn (a1, b1) = fnnn (a2, b2)  --Goal : (a1, b1) = (a2, b2)
  have h2 : a1 + b1 ≤ a2 + b2 := le_of_fnnn_eq h1
  have h3 : a2 + b2 ≤ a1 + b1 := le_of_fnnn_eq h1.symm
  have h4 : a1 + b1 = a2 + b2 := by linarith
  rewrite [fnnn_def, fnnn_def, h4] at h1
    --h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
  have h6 : a1 = a2 := Nat.add_left_cancel h1
  rewrite [h6] at h4   --h4 : a2 + b1 = a2 + b2
  have h7 : b1 = b2 := Nat.add_left_cancel h4
  rewrite [h6, h7]
  rfl
  done

lemma fnnn_onto : onto fnnn := by
  define  --Goal : ∀ (y : Nat), ∃ (x : Nat × Nat), fnnn x = y
  by_induc
  · -- Base Case
    apply Exists.intro (0, 0)
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ∃ (x : Nat × Nat), fnnn x = n
    obtain ((a, b) : Nat × Nat) (h1 : fnnn (a, b) = n) from ih
    by_cases h2 : b = 0
    · -- Case 1. h2 : b = 0
      apply Exists.intro (0, a + 1)
      show fnnn (0, a + 1) = n + 1 from
        calc fnnn (0, a + 1)
          _ = tri (0 + (a + 1)) + 0 := by rfl
          _ = tri (a + 1) := by ring
          _ = tri a + a + 1 := tri_step a
          _ = tri (a + 0) + a + 1 := by ring
          _ = fnnn (a, b) + 1 := by rw [h2, fnnn_def]
          _ = n + 1 := by rw [h1]
      done
    · -- Case 2. h2 : b ≠ 0
      obtain (k : Nat) (h3 : b = k + 1) from
        exists_eq_add_one_of_ne_zero h2
      apply Exists.intro (a + 1, k)
      show fnnn (a + 1, k) = n + 1 from
        calc fnnn (a + 1, k)
          _ = tri (a + 1 + k) + (a + 1) := by rfl
          _ = tri (a + (k + 1)) + a + 1 := by ring
          _ = tri (a + b) + a + 1 := by rw [h3]
          _ = fnnn (a, b) + 1 := by rfl
          _ = n + 1 := by rw [h1]
      done
    done
  done

Despite these successes with one-to-one, onto functions, we will use a definition of “equinumerous” in Lean that is different from the definition in HTPI. There are two reasons for this change. First of all, the domain of a function in Lean must be a type, but we want to be able to talk about sets being equinumerous. Secondly, Lean expects functions to be computable; it regards the definition of a function as an algorithm for computing the value of the function on any input. This restriction would cause problems with some of our proofs. While there are ways to overcome these difficulties, they would introduce complications that we can avoid by using a different approach.

Suppose U and V are types, and we have sets A : Set U and B : Set V. We will define A to be equinumerous with B if there is a relation R from U to V that defines a one-to-one correspondence between the elements of A and B. To formulate this precisely, suppose that R has type Rel U V. We will place three requirements on R. First, we require that the relation R should hold only between elements of A and B. We say in this case that R is a relation within A and B:

def rel_within {U V : Type} (R : Rel U V) (A : Set U) (B : Set V) : Prop :=
  ∀ ⦃x : U⦄ ⦃y : V⦄, R x y → x ∈ A ∧ y ∈ B

Notice that in this definition, we have used the same double braces for the quantified variables x and y that were used in the definition of “subset.” This means that x and y are implicit arguments, and therefore if we have h1 : rel_within R A B and h2 : R a b, then h1 h2 is a proof of a ∈ A ∧ b ∈ B. There is no need to specify that a and b are the values to be assigned to x and y; Lean will figure that out for itself. (To type the double braces ⦃ and ⦄, type \{{ and \}}. There were cases in previous chapters where it would have been appropriate to use such implicit arguments, but we chose not to do so to avoid confusion. But by now you should be comfortable enough with Lean that you won’t be confused by this new complication.)

Next, we require that every element of A is related by R to exactly one thing. We say in this case that R is functional on A:

def fcnl_on {U V : Type} (R : Rel U V) (A : Set U) : Prop :=
  ∀ ⦃x : U⦄, x ∈ A → ∃! (y : V), R x y

Finally, we impose the same requirement in the other direction: for every element of B, exactly one thing should be related to it by R. We can express this by saying that the inverse of R is functional on B. In Chapter 4, we defined the inverse of a set of ordered pairs, but we can easily convert this to an operation on relations:

def invRel {U V : Type} (R : Rel U V) : Rel V U :=
  RelFromExt (inv (extension R))

lemma invRel_def {U V : Type} (R : Rel U V) (u : U) (v : V) :
    invRel R v u ↔ R u v := by rfl

We will call R a matching from A to B if it meets the three requirements above:

def matching {U V : Type} (R : Rel U V) (A : Set U) (B : Set V) : Prop :=
  rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B

Finally, we say that A is equinumerous with B if there is a matching from A to B, and, as in HTPI we introduce the notation A ∼ B to indicate that A is equinumerous with B (to enter the symbol ∼, type \sim or \~).

def equinum {U V : Type} (A : Set U) (B : Set V) : Prop :=
  ∃ (R : Rel U V), matching R A B

notation:50  A:50 " ∼ " B:50 => equinum A B

Can the examples at the beginning of this section be used to establish that Int ∼ Nat and Nat × Nat ∼ Nat? Not quite, because Int, Nat, and Nat × Nat are types, not sets. We must talk about the sets of all objects of those types, not the types themselves, so we introduce another definition.

def Univ (U : Type) : Set U := {x : U | True}

lemma elt_Univ {U : Type} (u : U) :
    u ∈ Univ U := by trivial

For any type U, Univ U is the set of all objects of type U; we might call it the universal set for the type U. Now we can use the functions defined earlier to prove that Univ Int ∼ Univ Nat and Univ (Nat × Nat) ∼ Univ Nat. The do this, we must convert the functions into relations and prove that those relations are matchings. The conversion can be done with the following function.

def RelWithinFromFunc {U V : Type} (f : U → V) (A : Set U)
  (x : U) (y : V) : Prop := x ∈ A ∧ f x = y

This definition says that if we have f : U → V and A : Set U, then RelWithinFromFunc f A is a relation from U to V that relates any x that is an element of A to f x.

We will say that a function is one-to-one on a set A if it satisfies the definition of one-to-one when applied to elements of A:

def one_one_on {U V : Type} (f : U → V) (A : Set U) : Prop :=
  ∀ ⦃x1 x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2

With all of this preparation, we can now prove that if f is one-to-one on A, then A is equinumerous with its image under f.

theorem equinum_image {U V : Type} {A : Set U} {B : Set V} {f : U → V}
    (h1 : one_one_on f A) (h2 : image f A = B) : A ∼ B := by
  rewrite [←h2]
  define   --Goal : ∃ (R : Rel U V), matching R A (image f A)
  set R : Rel U V := RelWithinFromFunc f A
  apply Exists.intro R
  define   --Goal : rel_within R A (image f A) ∧
           --fcnl_on R A ∧ fcnl_on (invRel R) (image f A)
  apply And.intro
  · -- Proof of rel_within
    define --Goal : ∀ ⦃x : U⦄ ⦃y : V⦄, R x y → x ∈ A ∧ y ∈ image f A
    fix x : U; fix y : V
    assume h3 : R x y  --Goal : x ∈ A ∧ y ∈ image f A
    define at h3       --h3 : x ∈ A ∧ f x = y
    apply And.intro h3.left
    define
    show ∃ x ∈ A, f x = y from Exists.intro x h3
    done
  · -- Proofs of fcnl_ons
    apply And.intro
    · -- Proof of fcnl_on R A
      define  --Goal : ∀ ⦃x : U⦄, x ∈ A → ∃! (y : V), R x y
      fix x : U
      assume h3 : x ∈ A
      exists_unique
      · -- Existence
        apply Exists.intro (f x)
        define  --Goal : x ∈ A ∧ f x = f x
        apply And.intro h3
        rfl
        done
      · -- Uniqueness
        fix y1 : V; fix y2 : V
        assume h4 : R x y1
        assume h5 : R x y2   --Goal : y1 = y2
        define at h4; define at h5
          --h4 : x ∈ A ∧ f x = y1;  h5 : x ∈ A ∧ f x = y2
        rewrite [h4.right] at h5
        show y1 = y2 from h5.right
        done
      done
    · -- Proof of fcnl_on (invRel R) (image f A)
      define  --Goal : ∀ ⦃x : V⦄, x ∈ image f A → ∃! (y : U), invRel R x y
      fix y : V
      assume h3 : y ∈ image f A
      obtain (x : U) (h4 : x ∈ A ∧ f x = y) from h3
      exists_unique
      · -- Existence
        apply Exists.intro x
        define
        show x ∈ A ∧ f x = y from h4
        done
      · -- Uniqueness
        fix x1 : U; fix x2 : U
        assume h5 : invRel R y x1
        assume h6 : invRel R y x2
        define at h5; define at h6
          --h5 : x1 ∈ A ∧ f x1 = y;  h6 : x2 ∈ A ∧ f x2 = y
        rewrite [←h6.right] at h5
        show x1 = x2 from h1 h5.left h6.left h5.right
        done
      done
    done
  done

To apply this result to the functions introduced at the beginning of this section, we will want to use Univ U for the set A in the theorem equinum_image:

lemma one_one_on_of_one_one {U V : Type} {f : U → V}
    (h : one_to_one f) (A : Set U) : one_one_on f A := sorry

theorem equinum_Univ {U V : Type} {f : U → V}
    (h1 : one_to_one f) (h2 : onto f) : Univ U ∼ Univ V := by
  have h3 : image f (Univ U) = Univ V := by
    apply Set.ext
    fix v : V
    apply Iff.intro
    · -- (→)
      assume h3 : v ∈ image f (Univ U)
      show v ∈ Univ V from elt_Univ v
      done
    · -- (←)
      assume h3 : v ∈ Univ V
      obtain (u : U) (h4 : f u = v) from h2 v
      apply Exists.intro u
      apply And.intro _ h4
      show u ∈ Univ U from elt_Univ u
      done
    done
  show Univ U ∼ Univ V from
    equinum_image (one_one_on_of_one_one h1 (Univ U)) h3
  done

theorem Z_equinum_N : Univ Int ∼ Univ Nat :=
  equinum_Univ fzn_one_one fzn_onto

theorem NxN_equinum_N : Univ (Nat × Nat) ∼ Univ Nat :=
  equinum_Univ fnnn_one_one fnnn_onto

Theorem 8.1.3 in HTPI shows that ∼ is reflexive, symmetric, and transitive. We’ll prove the three parts of this theorem separately. To prove that ∼ is reflexive, we use the identity function.

lemma id_one_one_on {U : Type} (A : Set U) : one_one_on id A := sorry

lemma image_id {U : Type} (A : Set U) : image id A = A := sorry

theorem Theorem_8_1_3_1 {U : Type} (A : Set U) : A ∼ A :=
  equinum_image (id_one_one_on A) (image_id A)

For symmetry, we show that the inverse of a matching is also a matching.

lemma inv_inv {U V : Type} (R : Rel U V) : invRel (invRel R) = R := by rfl

lemma inv_match {U V : Type} {R : Rel U V} {A : Set U} {B : Set V}
    (h : matching R A B) : matching (invRel R) B A := by
  define       --Goal : rel_within (invRel R) B A ∧
               --fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
  define at h  --h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
  apply And.intro
  · -- Proof that rel_within (invRel R) B A
    define     --Goal : ∀ ⦃x : V⦄ ⦃y : U⦄, invRel R x y → x ∈ B ∧ y ∈ A
    fix y : V; fix x : U
    assume h1 : invRel R y x
    define at h1  --h1 : R x y
    have h2 : x ∈ A ∧ y ∈ B := h.left h1
    show y ∈ B ∧ x ∈ A from And.intro h2.right h2.left
    done
  · -- proof that fcnl_on (inv R) B ∧ fcnl_on (inv (inv R)) A
    rewrite [inv_inv]
    show fcnl_on (invRel R) B ∧ fcnl_on R A from
      And.intro h.right.right h.right.left
    done
  done

theorem Theorem_8_1_3_2 {U V : Type} {A : Set U} {B : Set V}
    (h : A ∼ B) : B ∼ A := by
  obtain (R : Rel U V) (h1 : matching R A B) from h
  apply Exists.intro (invRel R)
  show matching (invRel R) B A from inv_match h1
  done

The proof of transitivity is a bit more involved. In this proof, as well as some later proofs, we find it useful to separate out the existence and uniqueness parts of the definition of fcnl_on:

lemma fcnl_exists {U V : Type} {R : Rel U V} {A : Set U} {x : U}
    (h1 : fcnl_on R A) (h2 : x ∈ A) : ∃ (y : V), R x y := by
  define at h1
  obtain (y : V) (h3 : R x y)
    (h4 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2) from h1 h2
  show ∃ (y : V), R x y from Exists.intro y h3
  done

lemma fcnl_unique {U V : Type}
    {R : Rel U V} {A : Set U} {x : U} {y1 y2 : V} (h1 : fcnl_on R A)
    (h2 : x ∈ A) (h3 : R x y1) (h4 : R x y2) : y1 = y2 := by
  define at h1
  obtain (z : V) (h5 : R x z)
    (h6 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2) from h1 h2
  show y1 = y2 from h6 y1 y2 h3 h4
  done

To prove transitivity, we will show that a composition of matchings is a matching. Once again we must convert our definition of composition of sets of ordered pairs into an operation on relations. A few preliminary lemmas help with the proof.

def compRel {U V W : Type} (S : Rel V W) (R : Rel U V) : Rel U W :=
  RelFromExt (comp (extension S) (extension R))

lemma compRel_def {U V W : Type}
    (S : Rel V W) (R : Rel U V) (u : U) (w : W) :
    compRel S R u w ↔ ∃ (x : V), R u x ∧ S x w := by rfl

lemma inv_comp {U V W : Type} (R : Rel U V) (S : Rel V W) :
    invRel (compRel S R) = compRel (invRel R) (invRel S) := 
  calc invRel (compRel S R)
    _ = RelFromExt (inv (comp (extension S) (extension R))) := by rfl
    _ = RelFromExt (comp (inv (extension R)) (inv (extension S))) := by
          rw [Theorem_4_2_5_5]
    _ = compRel (invRel R) (invRel S) := by rfl

lemma comp_fcnl {U V W : Type} {R : Rel U V} {S : Rel V W}
    {A : Set U} {B : Set V} {C : Set W} (h1 : matching R A B)
    (h2 : matching S B C) : fcnl_on (compRel S R) A := by
  define; define at h1; define at h2
  fix a : U
  assume h3 : a ∈ A
  obtain (b : V) (h4 : R a b) from fcnl_exists h1.right.left h3
  have h5 : a ∈ A ∧ b ∈ B := h1.left h4
  obtain (c : W) (h6 : S b c) from fcnl_exists h2.right.left h5.right
  exists_unique
  · -- Existence
    apply Exists.intro c
    rewrite [compRel_def]
    show ∃ (x : V), R a x ∧ S x c from Exists.intro b (And.intro h4 h6)
    done
  · -- Uniqueness
    fix c1 : W; fix c2 : W
    assume h7 : compRel S R a c1
    assume h8 : compRel S R a c2    --Goal : c1 = c2
    rewrite [compRel_def] at h7
    rewrite [compRel_def] at h8
    obtain (b1 : V) (h9 : R a b1 ∧ S b1 c1) from h7
    obtain (b2 : V) (h10 : R a b2 ∧ S b2 c2) from h8
    have h11 : b1 = b := fcnl_unique h1.right.left h3 h9.left h4
    have h12 : b2 = b := fcnl_unique h1.right.left h3 h10.left h4
    rewrite [h11] at h9
    rewrite [h12] at h10
    show c1 = c2 from
      fcnl_unique h2.right.left h5.right h9.right h10.right
    done
  done

lemma comp_match {U V W : Type} {R : Rel U V} {S : Rel V W}
    {A : Set U} {B : Set V} {C : Set W} (h1 : matching R A B)
    (h2 : matching S B C) : matching (compRel S R) A C := by
  define
  apply And.intro
  · -- Proof of rel_within (compRel S R) A C
    define
    fix a : U; fix c : W
    assume h3 : compRel S R a c
    rewrite [compRel_def] at h3
    obtain (b : V) (h4 : R a b ∧ S b c) from h3
    have h5 : a ∈ A ∧ b ∈ B := h1.left h4.left
    have h6 : b ∈ B ∧ c ∈ C := h2.left h4.right
    show a ∈ A ∧ c ∈ C from And.intro h5.left h6.right
    done
  · -- Proof of fcnl_on statements
    apply And.intro
    · -- Proof of fcnl_on (compRel S R) A
      show fcnl_on (compRel S R) A from comp_fcnl h1 h2
      done
    · -- Proof of fcnl_on (invRel (compRel S R)) Z
      rewrite [inv_comp]
      have h3 : matching (invRel R) B A := inv_match h1
      have h4 : matching (invRel S) C B := inv_match h2
      show fcnl_on (compRel (invRel R) (invRel S)) C from comp_fcnl h4 h3
      done
    done
  done

theorem Theorem_8_1_3_3 {U V W : Type} {A : Set U} {B : Set V} {C : Set W}
    (h1 : A ∼ B) (h2 : B ∼ C) : A ∼ C := by
  obtain (R : Rel U V) (h3 : matching R A B) from h1
  obtain (S : Rel V W) (h4 : matching S B C) from h2
  apply Exists.intro (compRel S R)
  show matching (compRel S R) A C from comp_match h3 h4
  done

Now that we have a basic understanding of the concept of equinumerous sets, we can use this concept to make a number of definitions. For any natural number \(n\), HTPI defines \(I_n\) to be the set \(\{1, 2, \ldots, n\}\), and then it defines a set to be finite if it is equinumerous with \(I_n\), for some \(n\). In Lean, it is a bit more convenient to use sets of the form \(\{0, 1, \ldots, n - 1\}\). With that small change, we can repeat the definitions of finite, denumerable, and countable in HTPI.

def I (n : Nat) : Set Nat := {k : Nat | k < n}

lemma I_def (k n : Nat) : k ∈ I n ↔ k < n := by rfl

def finite {U : Type} (A : Set U) : Prop :=
  ∃ (n : Nat), I n ∼ A

def denum {U : Type} (A : Set U) : Prop :=
  Univ Nat ∼ A

lemma denum_def {U : Type} (A : Set U) : denum A ↔ Univ Nat ∼ A := by rfl

def ctble {U : Type} (A : Set U) : Prop :=
  finite A ∨ denum A

Theorem 8.1.5 in HTPI gives two useful ways to characterize countable sets. The proof of the theorem in HTPI uses the fact that every set of natural numbers is countable. HTPI gives an intuitive explanation of why this is true, but of course in Lean an intuitive explanation won’t do. So before proving a version of Theorem 8.1.5, we sketch a proof that every set of natural numbers is countable.

Suppose A has type Set Nat. To prove that A is countable, we will define a relation enum A that “enumerates” the elements of A by relating 0 to the smallest element of A, 1 to the next element of A, 2 to the next, and so on. How do we tell which natural number should be related to any element n of A? Notice that if n is the smallest element of A, then there are 0 elements of A that are smaller than n; if it is second smallest element of A, then there is 1 element of A that is smaller than n; and so on. Thus, enum A should relate a natural number s to n if and only if the number of elements of A that are smaller than n is s. This suggests a plan: First we define a proposition num_elts_below A n s saying that the number of elements of A that are smaller than n is s. Then we use this proposition to define the relation enum A, and finally we show that enum A is a matching that can be used to prove that A is countable.

The definition of num_elts_below is recursive. The recursive step relates the number of elements of A below n + 1 to the number of elements below n. There are two possibilities: either n ∈ A and the number of elements below n + 1 is one larger than the number below n, or n ∉ A and the two numbers are the same. (This may remind you of the recursion we used to define num_rp_below in Chapter 7.)

def num_elts_below (A : Set Nat) (m s : Nat) : Prop :=
  match m with
    | 0 => s = 0
    | n + 1 => (n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1)) ∨
                (n ∉ A ∧ num_elts_below A n s)

def enum (A : Set Nat) (s n : Nat) : Prop := n ∈ A ∧ num_elts_below A n s

The details of the proof that enum A is the required matching are long. We’ll skip them here, but you can find them in the HTPI Lean package.

lemma neb_exists (A : Set Nat) :
    ∀ (n : Nat), ∃ (s : Nat), num_elts_below A n s := sorry

lemma bdd_subset_nat_match {A : Set Nat} {m s : Nat}
    (h1 : ∀ n ∈ A, n < m) (h2 : num_elts_below A m s) :
    matching (enum A) (I s) A := sorry

lemma bdd_subset_nat {A : Set Nat} {m s : Nat}
    (h1 : ∀ n ∈ A, n < m) (h2 : num_elts_below A m s) :
    I s ∼ A := Exists.intro (enum A) (bdd_subset_nat_match h1 h2)

lemma unbdd_subset_nat_match {A : Set Nat}
    (h1 : ∀ (m : Nat), ∃ n ∈ A, n ≥ m) :
    matching (enum A) (Univ Nat) A := sorry

lemma unbdd_subset_nat {A : Set Nat}
    (h1 : ∀ (m : Nat), ∃ n ∈ A, n ≥ m) :
    denum A := Exists.intro (enum A) (unbdd_subset_nat_match h1)

lemma subset_nat_ctble (A : Set Nat) : ctble A := by
  define          --Goal : finite A ∨ denum A
  by_cases h1 : ∃ (m : Nat), ∀ n ∈ A, n < m
  · -- Case 1. h1 : ∃ (m : Nat), ∀ n ∈ A, n < m
    apply Or.inl  --Goal : finite A
    obtain (m : Nat) (h2 : ∀ n ∈ A, n < m) from h1
    obtain (s : Nat) (h3 : num_elts_below A m s) from neb_exists A m
    apply Exists.intro s
    show I s ∼ A from bdd_subset_nat h2 h3
    done
  · -- Case 2. h1 : ¬∃ (m : Nat), ∀ n ∈ A, n < m
    apply Or.inr  --Goal : denum A
    push_neg at h1
      --This tactic converts h1 to ∀ (m : Nat), ∃ n ∈ A, m ≤ n
    show denum A from unbdd_subset_nat h1
    done
  done

As a consequence of our last lemma, we get another characterization of countable sets: a set is countable if and only if it is equinumerous with some subset of the natural numbers:

lemma ctble_of_equinum_ctble {U V : Type} {A : Set U} {B : Set V}
    (h1 : A ∼ B) (h2 : ctble A) : ctble B := sorry

lemma ctble_iff_equinum_set_nat {U : Type} (A : Set U) : 
    ctble A ↔ ∃ (I : Set Nat), I ∼ A := by
  apply Iff.intro
  · -- (→)
    assume h1 : ctble A
    define at h1  --h1 : finite A ∨ denum A
    by_cases on h1
    · -- Case 1. h1 : finite A
      define at h1  --h1 : ∃ (n : Nat), I n ∼ A
      obtain (n : Nat) (h2 : I n ∼ A) from h1
      show ∃ (I : Set Nat), I ∼ A from Exists.intro (I n) h2
      done
    · -- Case 2. h1 : denum A
      rewrite [denum_def] at h1  --h1 : Univ Nat ∼ A
      show ∃ (I : Set Nat), I ∼ A from Exists.intro (Univ Nat) h1
      done
    done
  · -- (←)
    assume h1 : ∃ (I : Set Nat), I ∼ A
    obtain (I : Set Nat) (h2 : I ∼ A) from h1
    have h3 : ctble I := subset_nat_ctble I
    show ctble A from ctble_of_equinum_ctble h2 h3
    done
  done

We are now ready to turn to Theorem 8.1.5 in HTPI. The theorem gives two statements that are equivalent to the countability of a set \(A\). The first involves a function from the natural numbers to \(A\) that is onto. In keeping with our approach in this section, we state a similar characterization involving a relation rather than a function.

def unique_val_on_N {U : Type} (R : Rel Nat U) : Prop :=
  ∀ ⦃n : Nat⦄ ⦃x1 x2 : U⦄, R n x1 → R n x2 → x1 = x2

def nat_rel_onto {U : Type} (R : Rel Nat U) (A : Set U) : Prop :=
  ∀ ⦃x : U⦄, x ∈ A → ∃ (n : Nat), R n x

def fcnl_onto_from_nat {U : Type} (R : Rel Nat U) (A : Set U) : Prop :=
  unique_val_on_N R ∧ nat_rel_onto R A

Intuitively, you might think of fcnl_onto_from_nat R A as meaning that the relation R defines a function whose domain is a subset of the natural numbers and whose range contains A.

The second characterization of the countability of \(A\) in Theorem 8.1.5 involves a function from \(A\) to the natural numbers that is one-to-one. Once again, we rephrase this in terms of relations. We define fcnl_one_one_to_nat R A to mean that R defines a function from A to the natural numbers that is one-to-one:

def fcnl_one_one_to_nat {U : Type} (R : Rel U Nat) (A : Set U) : Prop :=
  fcnl_on R A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : Nat⦄,
    (x1 ∈ A ∧ R x1 n) → (x2 ∈ A ∧ R x2 n) → x1 = x2

Our plan is to prove that if A has type Set U then the following statements are equivalent:

1. ctble A
2. ∃ (R : Rel Nat U), fcnl_onto_from_nat R A
3. ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A

As in HTPI, we will do this by proving 1 → 2 → 3 → 1. Here is the proof of 1 → 2.

theorem Theorem_8_1_5_1_to_2 {U : Type} {A : Set U} (h1 : ctble A) :
    ∃ (R : Rel Nat U), fcnl_onto_from_nat R A := by
  rewrite [ctble_iff_equinum_set_nat] at h1
  obtain (I : Set Nat) (h2 : I ∼ A) from h1
  obtain (R : Rel Nat U) (h3 : matching R I A) from h2
  define at h3
    --h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
  apply Exists.intro R
  define  --Goal : unique_val_on_N R ∧ nat_rel_onto R A
  apply And.intro
  · -- Proof of unique_val_on_N R
    define
    fix n : Nat; fix x1 : U; fix x2 : U
    assume h4 : R n x1
    assume h5 : R n x2      --Goal : x1 = x2
    have h6 : n ∈ I ∧ x1 ∈ A := h3.left h4
    show x1 = x2 from fcnl_unique h3.right.left h6.left h4 h5
    done
  · -- Proof of nat_rel_onto R A
    define
    fix x : U
    assume h4 : x ∈ A  --Goal : ∃ (n : Nat), R n x
    show ∃ (n : Nat), R n x from fcnl_exists h3.right.right h4
    done
  done

For the proof of 2 → 3, suppose we have A : Set U and S : Rel Nat U, and the statement fcnl_onto_from_nat S A is true. We need to come up with a relation R : Rel U Nat for which we can prove fcnl_one_one_to_nat R A. You might be tempted to try R = invRel S, but there is a problem with this choice: if x ∈ A, there might be multiple natural numbers n such that S n x holds, but we must make sure that there is only one n for which R x n holds. Our solution to this problem will be to define R x n to mean that n is the smallest natural number for which S n x holds. (The proof in HTPI uses a similar idea.) The well-ordering principle guarantees that there always is such a smallest element.

def least_rel_to {U : Type} (S : Rel Nat U) (x : U) (n : Nat) : Prop :=
  S n x ∧ ∀ (m : Nat), S m x → n ≤ m

lemma exists_least_rel_to {U : Type} {S : Rel Nat U} {x : U}
    (h1 : ∃ (n : Nat), S n x) : ∃ (n : Nat), least_rel_to S x n := by
  set W : Set Nat := {n : Nat | S n x}
  have h2 : ∃ (n : Nat), n ∈ W := h1
  show ∃ (n : Nat), least_rel_to S x n from well_ord_princ W h2
  done

theorem Theorem_8_1_5_2_to_3 {U : Type} {A : Set U}
    (h1 : ∃ (R : Rel Nat U), fcnl_onto_from_nat R A) :
    ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A := by
  obtain (S : Rel Nat U) (h2 : fcnl_onto_from_nat S A) from h1
  define at h2  --h2 : unique_val_on_N S ∧ nat_rel_onto S A
  set R : Rel U Nat := least_rel_to S
  apply Exists.intro R
  define
  apply And.intro
  · -- Proof of fcnl_on R A
    define
    fix x : U
    assume h4 : x ∈ A  --Goal : ∃! (y : Nat), R x y
    exists_unique
    · -- Existence
      have h5 : ∃ (n : Nat), S n x := h2.right h4
      show ∃ (n : Nat), R x n from exists_least_rel_to h5
      done
    · -- Uniqueness
      fix n1 : Nat; fix n2 : Nat
      assume h5 : R x n1
      assume h6 : R x n2      --Goal : n1 = n2
      define at h5    --h5 : S n1 x ∧ ∀ (m : Nat), S m x → n1 ≤ m
      define at h6    --h6 : S n2 x ∧ ∀ (m : Nat), S m x → n2 ≤ m
      have h7 : n1 ≤ n2 := h5.right n2 h6.left
      have h8 : n2 ≤ n1 := h6.right n1 h5.left
      linarith
      done
    done
  · -- Proof of one-to-one
    fix x1 : U; fix x2 : U; fix n : Nat
    assume h4 : x1 ∈ A ∧ R x1 n
    assume h5 : x2 ∈ A ∧ R x2 n
    have h6 : R x1 n := h4.right
    have h7 : R x2 n := h5.right
    define at h6   --h6 : S n x1 ∧ ∀ (m : Nat), S m x1 → n ≤ m
    define at h7   --h7 : S n x2 ∧ ∀ (m : Nat), S m x2 → n ≤ m
    show x1 = x2 from h2.left h6.left h7.left
    done
  done

Finally, for the proof of 3 → 1, suppose we have A : Set U, S : Rel U Nat, and fcnl_one_one_to_nat S A holds. Our plan is to restrict S to elements of A and then show that the inverse of the resulting relation is a matching from some set of natural numbers to A. By ctble_iff_equinum_set_nat, this implies that A is countable.

def restrict_to {U V : Type} (S : Rel U V) (A : Set U)
  (x : U) (y : V) : Prop := x ∈ A ∧ S x y

theorem Theorem_8_1_5_3_to_1 {U : Type} {A : Set U}
    (h1 : ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A) :
    ctble A := by
  obtain (S : Rel U Nat) (h2 : fcnl_one_one_to_nat S A) from h1
  define at h2  --h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : Nat⦄,
                --x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
  rewrite [ctble_iff_equinum_set_nat]  --Goal : ∃ (I : Set Nat), I ∼ A
  set R : Rel Nat U := invRel (restrict_to S A)
  set I : Set Nat := {n : Nat | ∃ (x : U), R n x}
  apply Exists.intro I
  define        --Goal : ∃ (R : Rel Nat U), matching R I A
  apply Exists.intro R
  define
  apply And.intro
  · -- Proof of rel_within R I A
    define
    fix n : Nat; fix x : U
    assume h3 : R n x   --Goal : n ∈ I ∧ x ∈ A
    apply And.intro
    · -- Proof that n ∈ I
      define            --Goal : ∃ (x : U), R n x
      show ∃ (x : U), R n x from Exists.intro x h3
      done
    · -- Proof that x ∈ A
      define at h3      --h3 : x ∈ A ∧ S x n
      show x ∈ A from h3.left
      done
    done
  · -- Proofs of fcnl_ons
    apply And.intro
    · -- Proof of fcnl_on R I
      define
      fix n : Nat
      assume h3 : n ∈ I   --Goal : ∃! (y : U), R n y
      exists_unique
      · -- Existence
        define at h3      --h3 : ∃ (x : U), R n x
        show ∃ (y : U), R n y from h3
        done
      · -- Uniqueness
        fix x1 : U; fix x2 : U
        assume h4 : R n x1
        assume h5 : R n x2
        define at h4      --h4 : x1 ∈ A ∧ S x1 n; 
        define at h5      --h5 : x2 ∈ A ∧ S x2 n
        show x1 = x2 from h2.right h4 h5
        done
      done
    · -- Proof of fcnl_on (invRel R) A
      define
      fix x : U
      assume h3 : x ∈ A  --Goal : ∃! (y : Nat), invRel R x y
      exists_unique
      · -- Existence
        obtain (y : Nat) (h4 : S x y) from fcnl_exists h2.left h3
        apply Exists.intro y
        define
        show x ∈ A ∧ S x y from And.intro h3 h4
        done
      · -- Uniqueness
        fix n1 : Nat; fix n2 : Nat
        assume h4 : invRel R x n1
        assume h5 : invRel R x n2  --Goal : n1 = n2
        define at h4     --h4 : x ∈ A ∧ S x n1
        define at h5     --h5 : x ∈ A ∧ S x n2
        show n1 = n2 from fcnl_unique h2.left h3 h4.right h5.right
        done
      done
    done
  done

We now know that statements 1–3 are equivalent, which means that statements 2 and 3 can be thought of as alternative ways to think about countability:

theorem Theorem_8_1_5_2 {U : Type} (A : Set U) :
    ctble A ↔ ∃ (R : Rel Nat U), fcnl_onto_from_nat R A := by
  apply Iff.intro
  · -- (→)
    assume h1 : ctble A
    show ∃ (R : Rel Nat U), fcnl_onto_from_nat R A from
      Theorem_8_1_5_1_to_2 h1
    done
  · -- (←)
    assume h1 : ∃ (R : Rel Nat U), fcnl_onto_from_nat R A
    have h2 : ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A :=
      Theorem_8_1_5_2_to_3 h1
    show ctble A from Theorem_8_1_5_3_to_1 h2
    done
  done

theorem Theorem_8_1_5_3 {U : Type} (A : Set U) :
    ctble A ↔ ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A := sorry

In the exercises, we ask you to show that countability of a set can be proven using functions of the kind considered in Theorem 8.1.5 of HTPI.

We end this section with a proof of Theorem 8.1.6 in HTPI, which says that the set of rational numbers is denumerable. Our strategy is to define a one-to-one function from Rat (the type of rational numbers) to Nat. We will need to know a little bit about the way rational numbers are represented in Lean. If q has type Rat, then q.num is the numerator of q, which is an integer, and q.den is the denominator, which is a nonzero natural number. The theorem Rat.ext says that if two rational numbers have the same numerator and denominator, then they are equal. And we will also use the theorem Prod.mk.inj, which says that if two ordered pairs are equal, then their first coordinates are equal, as are their second coordinates.

def fqn (q : Rat) : Nat := fnnn (fzn q.num, q.den)

lemma fqn_def (q : Rat) : fqn q = fnnn (fzn q.num, q.den) := by rfl

lemma fqn_one_one : one_to_one fqn := by
  define
  fix q1 : Rat; fix q2 : Rat
  assume h1 : fqn q1 = fqn q2
  rewrite [fqn_def, fqn_def] at h1
    --h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
  have h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den) :=
    fnnn_one_one _ _ h1
  have h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den :=
    Prod.mk.inj h2
  have h4 : q1.num = q2.num := fzn_one_one _ _ h3.left
  show q1 = q2 from Rat.ext h4 h3.right
  done

lemma image_fqn_unbdd :
    ∀ (m : Nat), ∃ n ∈ image fqn (Univ Rat), n ≥ m := by
  fix m : Nat
  set n : Nat := fqn ↑m
  apply Exists.intro n
  apply And.intro
  · -- Proof that n ∈ image fqn (Univ Rat)
    define
    apply Exists.intro ↑m
    apply And.intro (elt_Univ (↑m : Rat))
    rfl
    done
  · -- Proof that n ≥ m
    show n ≥ m from
      calc n
        _ = tri (2 * m + 1) + 2 * m := by rfl
        _ ≥ m := by linarith
    done
  done

theorem Theorem_8_1_6 : denum (Univ Rat) := by
  set I : Set Nat := image fqn (Univ Rat)
  have h1 : Univ Nat ∼ I := unbdd_subset_nat image_fqn_unbdd
  have h2 : image fqn (Univ Rat) = I := by rfl
  have h3 : Univ Rat ∼ I :=
    equinum_image (one_one_on_of_one_one fqn_one_one (Univ Rat)) h2
  have h4 : I ∼ Univ Rat := Theorem_8_1_3_2 h3
  show denum (Univ Rat) from Theorem_8_1_3_3 h1 h4
  done

Exercises

--Hint:  Use Exercise_6_1_16a2 from the exercises of Section 6.1
lemma fnz_odd (k : Nat) : fnz (2 * k + 1) = -↑(k + 1) := sorry

lemma fnz_fzn : fnz ∘ fzn = id  := sorry

lemma tri_step (k : Nat) : tri (k + 1) = tri k + k + 1 := sorry

lemma tri_incr {j k : Nat} (h1 : j ≤ k) : tri j ≤ tri k := sorry

lemma ctble_of_equinum_ctble {U V : Type} {A : Set U} {B : Set V}
    (h1 : A ∼ B) (h2 : ctble A) : ctble B := sorry

theorem Exercise_8_1_1_b : denum {n : Int | even n} := sorry

The next four exercises use the following definition:

def Rel_image {U V : Type} (R : Rel U V) (A : Set U) : Set V :=
  {y : V | ∃ x ∈ A, R x y}

Note that if R has type Rel U V, then Rel_image R has type Set U → Set V.

lemma Rel_image_on_power_set {U V : Type} {R : Rel U V}
    {A C : Set U} {B : Set V} (h1 : matching R A B) (h2 : C ∈ 𝒫 A) :
    Rel_image R C ∈ 𝒫 B := sorry

lemma Rel_image_inv {U V : Type} {R : Rel U V}
    {A C : Set U} {B : Set V} (h1 : matching R A B) (h2 : C ∈ 𝒫 A) :
    Rel_image (invRel R) (Rel_image R C) = C := sorry

lemma Rel_image_one_one_on {U V : Type} {R : Rel U V}
    {A : Set U} {B : Set V} (h1 : matching R A B) :
    one_one_on (Rel_image R) (𝒫 A) := sorry

lemma Rel_image_image {U V : Type} {R : Rel U V}
    {A : Set U} {B : Set V} (h1 : matching R A B) :
    image (Rel_image R) (𝒫 A) = 𝒫 B := sorry

--Hint:  Use the previous two exercises.
theorem Exercise_8_1_5 {U V : Type} {A : Set U} {B : Set V}
    (h1 : A ∼ B) : 𝒫 A ∼ 𝒫 B := sorry

theorem Exercise_8_1_17 {U : Type} {A B : Set U}
    (h1 : B ⊆ A) (h2 : ctble A) : ctble B := sorry

theorem ctble_of_onto_func_from_N {U : Type} {A : Set U} {f : Nat → U}
    (h1 : ∀ x ∈ A, ∃ (n : Nat), f n = x) : ctble A := sorry

theorem ctble_of_one_one_func_to_N {U : Type} {A : Set U} {f : U → Nat}
    (h1 : one_one_on f A) : ctble A := sorry

8.1½. Debts Paid

It is time to fulfill promises we made in two earlier chapters.

In Section 6.2, we promised to define a proposition numElts A n to express the idea that the set A has n elements. It should now be clear how to define this proposition:

def numElts {U : Type} (A : Set U) (n : Nat) : Prop := I n ∼ A

lemma numElts_def {U : Type} (A : Set U) (n : Nat) :
    numElts A n ↔ I n ∼ A := by rfl

It is sometimes convenient to phrase the definition of finite in terms of numElts, so we state that version of the definition as a lemma.

lemma finite_def {U : Type} (A : Set U) :
    finite A ↔ ∃ (n : Nat), numElts A n := by rfl

We also owe you the proofs of several theorems about numElts. We begin with the fact that a set has zero elements if and only if it is empty. To prove this, we will need to produce a relation that is a matching between two sets if the sets are empty. The natural choice for this relation is what we will call the empty relation—the relation that is always false.

def emptyRel (U V : Type) (x : U) (y : V) : Prop := False

lemma fcnl_on_empty {U V : Type}
    (R : Rel U V) {A : Set U} (h1 : empty A) : fcnl_on R A := by
  define
  fix a : U
  assume h2 : a ∈ A      --Goal : ∃! (y : V), R a y
  contradict h1 with h3  --Goal : ∃ (x : U), x ∈ A
  show ∃ (x : U), x ∈ A from Exists.intro a h2
  done

lemma empty_match {U V : Type} {A : Set U} {B : Set V}
    (h1 : empty A) (h2 : empty B) : matching (emptyRel U V) A B := by
  define
  apply And.intro
  · -- Proof of rel_within
    define
    fix a : U; fix b : V
    assume h3 : emptyRel U V a b   --Goal : a ∈ A ∧ b ∈ B
    by_contra h4                   --Goal : False
    define at h3
    show False from h3
    done
  · -- Proof of fcnl_ons
    apply And.intro
    · -- Proof of fcnl_on emptyRel
      show fcnl_on (emptyRel U V) A from fcnl_on_empty (emptyRel U V) h1
      done
    · -- Proof of fcnl_on (invRel emptyRel)
      show fcnl_on (invRel (emptyRel U V)) B from
        fcnl_on_empty (invRel (emptyRel U V)) h2
      done
  done

lemma I_0_empty : empty (I 0) := by
  define
  by_contra h1    --h1 : ∃ (x : Nat), x ∈ I 0
  obtain (x : Nat) (h2 : x ∈ I 0) from h1
  define at h2    --h2 : x < 0
  linarith
  done

theorem zero_elts_iff_empty {U : Type} (A : Set U) :
    numElts A 0 ↔ empty A := by
  apply Iff.intro
  · -- (→)
    assume h1 : numElts A 0
    define
    by_contra h2         --h2 : ∃ (x : U), x ∈ A
    obtain (x : U) (h3 : x ∈ A) from h2
    define at h1
    obtain (R : Rel Nat U) (h4 : matching R (I 0) A) from h1
    define at h4
      --h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
    obtain (j : Nat) (h5 : invRel R x j) from
      fcnl_exists h4.right.right h3
    define at h5         --h5 : R j x
    have h6 : j ∈ I 0 ∧ x ∈ A := h4.left h5
    contradict I_0_empty --Goal : ∃ (x : Nat), x ∈ I 0
    show ∃ (x : Nat), x ∈ I 0 from Exists.intro j h6.left
    done
  · -- (←)
    assume h1 : empty A
    show ∃ (R : Rel Nat U), matching R (I 0) A from
      Exists.intro (emptyRel Nat U) (empty_match I_0_empty h1)
    done
  done

Next, we prove that if a set has a positive number of elements then it is not empty. The proof is straightforward.

theorem nonempty_of_pos_numElts {U : Type} {A : Set U} {n : Nat}
    (h1 : numElts A n) (h2 : n > 0) : ∃ (x : U), x ∈ A := by
  define at h1
  obtain (R : Rel Nat U) (h3 : matching R (I n) A) from h1
  define at h3
  have h4 : 0 ∈ I n := h2
  obtain (x : U) (h5 : R 0 x) from fcnl_exists h3.right.left h4
  have h6 : 0 ∈ I n ∧ x ∈ A := h3.left h5
  show ∃ (x : U), x ∈ A from Exists.intro x h6.right
  done

To prove our next theorem about numElts, we will need to prove that two relations are equal. How can we do that? To prove that two sets are equal, we usually start by applying Set.ext, and to prove that two functions are equal we apply funext. We’ll need a similar extensionality principle for relations. If R and S are relations from U to V, the principle will say that if we have h : ∀ (u : U) (v : V), R u v ↔︎ S u v, then we can conclude that R = S. To prove it, we’ll use h to prove extension R = extension S, and then go on to deduce R = S.

theorem relext {U V : Type} {R S : Rel U V}
    (h : ∀ (u : U) (v : V), R u v ↔ S u v) : R = S := by
  have h2 : extension R = extension S := by
    apply Set.ext
    fix (u, v) : U × V --Goal : (u, v) ∈ extension R ↔ (u, v) ∈ extension S
    rewrite [ext_def, ext_def]  --Goal : R u v ↔ S u v
    show R u v ↔ S u v from h u v
    done
  show R = S from
    calc R
      _ = RelFromExt (extension R) := by rfl
      _ = RelFromExt (extension S) := by rw [h2]
      _ = S := by rfl
  done

Now we are ready to prove that if A has n + 1 elements and we remove one element, then the resulting set has n elements. The key lemma for this proof says that if A ∼ B, u ∈ A, and v ∈ B, then A \ {u} ∼ B \ {v}. To see how to prove this lemma, suppose that R is a matching from A to B. We must find a way to modify R to get a matching from A \ {u} to B \ {v}. If we’re lucky, R u v will be true, in which case if we simply eliminate the pairing of u with v from R, the resulting relation will be a matching from A \ {u} to B \ {v}. But it may happen that R u v is not true. In that case, there must be some x ∈ A \ {u} and some y ∈ B \ {v} such that R x v and R u y. When we remove u from A and v from B, x and y will be left unpaired. The obvious solution is to pair them with each other! This motivates the definition of a new relation remove_one R u v:

def remove_one {U V : Type} (R : Rel U V) (u : U) (v : V)
  (x : U) (y : V) : Prop := x ≠ u ∧ y ≠ v ∧ (R x y ∨ (R x v ∧ R u y))

lemma remove_one_def {U V : Type} (R : Rel U V) (u x : U) (v y : V) :
    remove_one R u v x y ↔
      x ≠ u ∧ y ≠ v ∧ (R x y ∨ (R x v ∧ R u y)) := by rfl

Our strategy now is to prove that remove_one R u v is a matching from A \ {u} to B \ {v}. The proof is long but not hard, so we skip some of the details.

lemma remove_one_rel_within {U V : Type}
    {R : Rel U V} {A : Set U} {B : Set V} {x u : U} {y v : V}
    (h1 : matching R A B) (h2 : remove_one R u v x y) :
    x ∈ A \ {u} ∧ y ∈ B \ {v} := sorry

lemma remove_one_inv {U V : Type} (R : Rel U V) (u : U) (v : V) :
    invRel (remove_one R u v) = remove_one (invRel R) v u := by
  apply relext
  fix y : V; fix x : U
    --Goal : invRel (remove_one R u v) y x ↔ remove_one (invRel R) v u y x
  rewrite [invRel_def, remove_one_def, remove_one_def]
  rewrite [invRel_def, invRel_def, invRel_def]
  rewrite [←and_assoc, ←and_assoc]
    --Goal : (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔
    --       (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
  have h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u := and_comm
  have h2 : R x v ∧ R u y ↔ R u y ∧ R x v := and_comm
  rewrite [h1, h2]
  rfl
  done

lemma remove_one_iff {U V : Type}
    {A : Set U} {B : Set V} {R : Rel U V} (h1 : matching R A B)
    {u : U} (h2 : u ∈ A) (v : V) {x : U} (h3 : x ∈ A \ {u}) :
    ∃ w ∈ A, ∀ (y : V), remove_one R u v x y ↔ R w y := sorry

theorem remove_one_fcnl {U V : Type}
    {R : Rel U V} {A : Set U} {B : Set V} {u : U}
    (h1 : matching R A B) (h2 : u ∈ A) (v : V) :
    fcnl_on (remove_one R u v) (A \ {u}) := by
  define
  fix x : U
  assume h3 : x ∈ A \ {u}  --Goal : ∃! (y : V), remove_one R u v x y
  obtain (w : U) (h4 : w ∈ A ∧ ∀ (y : V),
    remove_one R u v x y ↔ R w y) from remove_one_iff h1 h2 v h3
  define at h1
  exists_unique
  · -- Existence
    obtain (y : V) (h5 : R w y) from fcnl_exists h1.right.left h4.left
    apply Exists.intro y
    rewrite [h4.right]
    show R w y from h5
    done
  · -- Uniqueness
    fix y1 : V; fix y2 : V
    rewrite [h4.right, h4.right]
    assume h5 : R w y1
    assume h6 : R w y2
    show y1 = y2 from fcnl_unique h1.right.left h4.left h5 h6
    done
  done

theorem remove_one_match {U V : Type}
    {R : Rel U V} {A : Set U} {B : Set V} {u : U} {v : V}
    (h1 : matching R A B) (h2 : u ∈ A) (h3 : v ∈ B) :
    matching (remove_one R u v) (A \ {u}) (B \ {v}) := by
  define
  apply And.intro
  · -- Proof of rel_within
    define
    fix x : U; fix y : V
    assume h4 : remove_one R u v x y
    show x ∈ A \ {u} ∧ y ∈ B \ {v} from remove_one_rel_within h1 h4
    done
  · -- Proof of fcnl_ons
    apply And.intro (remove_one_fcnl h1 h2 v)
    rewrite [remove_one_inv]
    show fcnl_on (remove_one (invRel R) v u) (B \ {v}) from
      remove_one_fcnl (inv_match h1) h3 u
  done

theorem remove_one_equinum {U V : Type}
    {A : Set U} {B : Set V} {u : U} {v : V}
    (h1 : A ∼ B) (h2 : u ∈ A) (h3 : v ∈ B) : A \ {u} ∼ B \ {v} := by
  define
  obtain (R : Rel U V) (h4 : matching R A B) from h1
  apply Exists.intro (remove_one R u v)
  show matching (remove_one R u v) (A \ {u}) (B \ {v}) from
    remove_one_match h4 h2 h3
  done

lemma I_max (n : Nat) : n ∈ I (n + 1) := sorry

lemma I_diff (n : Nat) : I (n + 1) \ {n} = I n := sorry

theorem remove_one_numElts {U : Type} {A : Set U} {n : Nat} {a : U}
    (h1 : numElts A (n + 1)) (h2 : a ∈ A) : numElts (A \ {a}) n := by
  have h3 : n ∈ I (n + 1) := I_max n
  rewrite [numElts_def] at h1     --h1 : I (n + 1) ∼ X
  have h4 : I (n + 1) \ {n} ∼ A \ {a} := remove_one_equinum h1 h3 h2
  rewrite [I_diff] at h4          --h4 : I n ∼ A \ {a}
  show numElts (A \ {a}) n from h4
  done

Finally, we prove that a set has one element if and only if it is a singleton set. For this proof, we need to be able to produce a relation that is a matching between two singleton sets. Suppose we have a : U and b : V. Of course, a matching from {a} to {b} must pair a with b, so we make the following definition:

def one_match {U V : Type} (a : U) (b : V)
  (x : U) (y : V) : Prop := x = a ∧ y = b
  
lemma one_match_def {U V : Type} (a x : U) (b y : V) :
    one_match a b x y ↔ x = a ∧ y = b := by rfl

We prove the theorem using a few lemmas, whose proofs we leave to you.

lemma one_match_match {U V : Type} (a : U) (b : V) :
    matching (one_match a b) {a} {b} := sorry

lemma I_1_singleton : I 1 = {0} := sorry

lemma singleton_of_diff_empty {U : Type} {A : Set U} {a : U}
    (h1 : a ∈ A) (h2 : empty (A \ {a})) : A = {a} := sorry

lemma singleton_one_elt {U : Type} (u : U) : numElts {u} 1 := by
  define
  rewrite [I_1_singleton]
  show ∃ (R : Rel Nat U), matching R {0} {u} from
    Exists.intro (one_match 0 u) (one_match_match 0 u)
  done

theorem one_elt_iff_singleton {U : Type} (A : Set U) :
    numElts A 1 ↔ ∃ (x : U), A = {x} := by
  apply Iff.intro
  · -- (→)
    assume h1 : numElts A 1  --Goal : ∃ (x : U), A = {x}
    have h2 : 1 > 0 := by decide
    obtain (x : U) (h3 : x ∈ A) from nonempty_of_pos_numElts h1 h2
    have h4 : numElts (A \ {x}) 0 := remove_one_numElts h1 h3
    rewrite [zero_elts_iff_empty] at h4
    show ∃ (x : U), A = {x} from
      Exists.intro x (singleton_of_diff_empty h3 h4)
    done
  · -- (←)
    assume h1 : ∃ (x : U), A = {x}
    obtain (x : U) (h2 : A = {x}) from h1
    rewrite [h2]
    show numElts {x} 1 from singleton_one_elt x
    done
  done

We have now proven all of the theorems about numElts whose proofs were promised in Section 6.2. However, there is still one important issue that we have not addressed. Could there be a set A such that, say, numElts A 5 and numElts A 6 are both true? Surely the answer is no—a set can’t have five elements and also have six elements! But it requires proof.

lemma eq_zero_of_I_zero_equinum {n : Nat} (h1 : I 0 ∼ I n) : n = 0 := by
  rewrite [←numElts_def, zero_elts_iff_empty] at h1
    --h1 : empty (I n)
  contradict h1 with h2       --Goal : ∃ (x : Nat), x ∈ I n
  apply Exists.intro 0
  define
  show 0 < n from Nat.pos_of_ne_zero h2
  done

theorem eq_of_I_equinum : ∀ ⦃m n : Nat⦄, I m ∼ I n → m = n := by
  by_induc
  · -- Base Case
    fix n : Nat
    assume h1 : I 0 ∼ I n
    show 0 = n from (eq_zero_of_I_zero_equinum h1).symm
    done
  · -- Induction Step
    fix m : Nat
    assume ih : ∀ ⦃n : Nat⦄, I m ∼ I n → m = n
    fix n : Nat
    assume h1 : I (m + 1) ∼ I n      --Goal : m + 1 = n
    have h2 : n ≠ 0 := by
      by_contra h2
      have h3 : I n ∼ I (m + 1) := Theorem_8_1_3_2 h1
      rewrite [h2] at h3
      have h4 : m + 1 = 0 := eq_zero_of_I_zero_equinum h3
      linarith
      done
    obtain (k : Nat) (h3 : n = k + 1) from exists_eq_add_one_of_ne_zero h2
    rewrite [h3] at h1               --h1 : I (m + 1) ∼ I (k + 1)
    rewrite [h3]                     --Goal : m + 1 = k + 1
    have h4 : m ∈ I (m + 1) := I_max m
    have h5 : k ∈ I (k + 1) := I_max k
    have h6 : I (m + 1) \ {m} ∼ I (k + 1) \ {k} :=
      remove_one_equinum h1 h4 h5
    rewrite [I_diff, I_diff] at h6   --h6 : I m ∼ I k
    have h7 : m = k := ih h6
    rewrite [h7]
    rfl
    done
  done

theorem numElts_unique {U : Type} {A : Set U} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts A n) : m = n := by
  rewrite [numElts_def] at h1      --h1 : I m ∼ A
  rewrite [numElts_def] at h2      --h2 : I n ∼ A
  have h3 : A ∼ I n := Theorem_8_1_3_2 h2
  have h4 : I m ∼ I n := Theorem_8_1_3_3 h1 h3
  show m = n from eq_of_I_equinum h4
  done

Next, we turn to our promise, at the end of Section 7.4, to prove Theorem 7.4.4 of HTPI, which says that the totient function \(\varphi\) is multiplicative.

To define the totient function in Lean, in Chapter 7 we defined phi m to be num_rp_below m m, where num_rp_below m k is the number of natural numbers less than k that are relatively prime to m. But in this chapter we have developed new methods for counting things. Our first task is to show that these new methods agree with the method used in Chapter 7.

We have already remarked that the definition of num_elts_below in this chapter bears some resemblance to the definition of num_rp_below in Chapter 7. It should not be surprising, therefore, that these two counting methods give results that agree.

def Set_rp_below (m : Nat) : Set Nat := {n : Nat | rel_prime m n ∧ n < m}

lemma Set_rp_below_def (a m : Nat) :
    a ∈ Set_rp_below m ↔ rel_prime m a ∧ a < m := by rfl

lemma neb_nrpb (m : Nat) : ∀ ⦃k : Nat⦄, k ≤ m →
    num_elts_below (Set_rp_below m) k (num_rp_below m k) := sorry

lemma neb_phi (m : Nat) :
    num_elts_below (Set_rp_below m) m (phi m) := by
  rewrite [phi_def]
  have h1 : m ≤ m := by linarith
  show num_elts_below (Set_rp_below m) m (num_rp_below m m) from
    neb_nrpb m h1
  done

lemma phi_is_numElts (m : Nat) :
    numElts (Set_rp_below m) (phi m) := by
  rewrite [numElts_def]    --Goal : I (phi m) ∼ Set_rp_below m
  have h1 : ∀ n ∈ Set_rp_below m, n < m := by
    fix n : Nat
    assume h2 : n ∈ Set_rp_below m
    define at h2
    show n < m from h2.right
    done
  have h2 : num_elts_below (Set_rp_below m) m (phi m) := neb_phi m
  show I (phi m) ∼ Set_rp_below m from bdd_subset_nat h1 h2
  done

According to the last lemma, we can now think of phi m as the number of elements of the set Set_rp_below m.

We will need one more number-theoretic fact: Lemma 7.4.7 from HTPI. We follow the strategy of the proof in HTPI, separating out one calculation as an auxiliary lemma before giving the main proof.

lemma Lemma_7_4_7_aux {m n : Nat} {s t : Int}
    (h : s * m + t * n = 1) (a b : Nat) :
    t * n * a + s * m * b ≡ a (MOD m) := by
  define
  apply Exists.intro (s * (b - a))
  show t * n * a + s * m * b - a = m * (s * (b - a)) from
    calc t * n * a + s * m * b - a
      _ = (t * n - 1) * a + s * m * b := by ring
      _ = (t * n - (s * m + t * n)) * a + s * m * b := by rw [h]
      _ = m * (s * (b - a)) := by ring
  done

lemma Lemma_7_4_7 {m n : Nat} [NeZero m] [NeZero n]
    (h1 : rel_prime m n) (a b : Nat) :
    ∃ (r : Nat), r < m * n ∧ r ≡ a (MOD m) ∧ r ≡ b (MOD n) := by
  set s : Int := gcd_c1 m n
  set t : Int := gcd_c2 m n
  have h4 : s * m + t * n = gcd m n := gcd_lin_comb n m
  define at h1                      --h1 : gcd m n = 1
  rewrite [h1, Nat.cast_one] at h4  --h4 : s * m + t * n = 1
  set x : Int := t * n * a + s * m * b
  have h5 : x ≡ a (MOD m) := Lemma_7_4_7_aux h4 a b
  rewrite [add_comm] at h4          --h4 : t * n + s * m = 1
  have h6 : s * m * b + t * n * a ≡ b (MOD n) :=
    Lemma_7_4_7_aux h4 b a
  have h7 : s * m * b + t * n * a = x := by ring
  rewrite [h7] at h6                --h6 : x ≡ b (MOD n)
  have h8 : m * n ≠ 0 := mul_ne_zero (NeZero.ne m) (NeZero.ne n)
  rewrite [←neZero_iff] at h8       --h8 : NeZero (m * n)
  have h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧
    x ≡ x % ↑(m * n) (MOD m * n) := mod_cmpl_res (m * n) x
  have h10 : x % ↑(m * n) < ↑(m * n) ∧
    x ≡ x % ↑(m * n) (MOD m * n) := h9.right
  set r : Nat := Int.toNat (x % ↑(m * n))
  have h11 : x % ↑(m * n) = ↑r := (Int.toNat_of_nonneg h9.left).symm
  rewrite [h11, Nat.cast_lt] at h10 --h10 : r < m * n ∧ x ≡ r (MOD m * n)
  apply Exists.intro r
  apply And.intro h10.left
  have h12 : r ≡ x (MOD (m * n)) := congr_symm h10.right
  rewrite [Lemma_7_4_5 _ _ h1] at h12 --h12 : r ≡ x (MOD m) ∧ r ≡ x (MOD n)
  apply And.intro
  · -- Proof that r ≡ a (MOD m)
    show r ≡ a (MOD m) from congr_trans h12.left h5
    done
  · -- Proof that r ≡ b (MOD n)
    show r ≡ b (MOD n) from congr_trans h12.right h6
    done
  done

The next fact we need is part 1 of Theorem 8.1.2 in HTPI, which says that if \(A\), \(B\), \(C\), and \(D\) are sets such that \(A \sim B\) and \(C \sim D\), then \(A \times C \sim B \times D\). We would like to prove this in Lean, but how do we state the theorem? In Lean, Cartesian product is an operation on types, not sets. However, we can define a Cartesian product operation on sets:

def Set_prod {U V : Type} (A : Set U) (B : Set V) : Set (U × V) :=
  {(a, b) : U × V | a ∈ A ∧ b ∈ B}

notation:75 A:75 " ×ₛ " B:75 => Set_prod A B

lemma Set_prod_def {U V : Type} (A : Set U) (B : Set V) (a : U) (b : V) :
    (a, b) ∈ A ×ₛ B ↔ a ∈ A ∧ b ∈ B := by rfl

To type the subscript s after ×, type \_s. Thus, to type ×ₛ, you can type \times\_s or \x\_s. Notice that in the notation command that introduces the symbol ×ₛ, we have used the number 75 in positions where we used 50 when defining the notation ∼. Without going into detail about exactly what the three occurrences of 50 and 75 mean, we will just say that this tells Lean that ×ₛ is to be given higher precedence than ∼, and as a result an expression like A ∼ B ×ₛ C will be interpreted as A ∼ (B ×ₛ C) rather than (A ∼ B) ×ₛ C.

We can now state the theorem corresponding to the first part of Theorem 8.1.2 in HTPI.

theorem Theorem_8_1_2_1
    {U V W X : Type} {A : Set U} {B : Set V} {C : Set W} {D : Set X}
    (h1 : A ∼ B) (h2 : C ∼ D) : A ×ₛ C ∼ B ×ₛ D

To see how to prove this theorem, suppose that R is a matching from A to B and S is a matching from C to D. We must produce a matching from A ×ₛ C to B ×ₛ D. The following definition is motivated by the proof in HTPI:

def Rel_prod {U V W X : Type} (R : Rel U V) (S : Rel W X)
  (p : U × W) (q : V × X) : Prop := R p.1 q.1 ∧ S p.2 q.2

notation:75 R:75 " ×ᵣ " S:75 => Rel_prod R S

lemma Rel_prod_def {U V W X : Type} (R : Rel U V) (S : Rel W X)
    (u : U) (v : V) (w : W) (x : X) :
    (R ×ᵣ S) (u, w) (v, x) ↔ R u v ∧ S w x := by rfl

With this definition, R ×ᵣ S is a relation from U × W to V × X. (Of course, to type the subscript r after ×, you should type \_r.) We leave the proof that R ×ᵣ S is a matching from A ×ₛ C to B ×ₛ D as an exercise for you.

lemma prod_match {U V W X : Type}
    {A : Set U} {B : Set V} {C : Set W} {D : Set X}
    {R : Rel U V} {S : Rel W X}
    (h1 : matching R A B) (h2 : matching S C D) :
    matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D) := sorry

theorem Theorem_8_1_2_1
    {U V W X : Type} {A : Set U} {B : Set V} {C : Set W} {D : Set X}
    (h1 : A ∼ B) (h2 : C ∼ D) : A ×ₛ C ∼ B ×ₛ D := by
  obtain (R : Rel U V) (h3 : matching R A B) from h1
  obtain (S : Rel W X) (h4 : matching S C D) from h2
  apply Exists.intro (R ×ᵣ S)
  show matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D) from prod_match h3 h4
  done

As explained in Section 7.4 of HTPI, a key fact used in the proof of Theorem 7.4.4 is that if \(A\) is a set with \(m\) elements and \(B\) is a set with \(n\) elements, then \(A \times B\) has \(mn\) elements. Section 7.4 of HTPI gives an intuitive explanation of this fact, but we’ll need to prove it in Lean. In other words, we need to prove the following theorem:

theorem numElts_prod {U V : Type} {A : Set U} {B : Set V} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts B n) : numElts (A ×ₛ B) (m * n)

Here’s our plan for this proof: The hypotheses numElts A m and numElts B n mean I m ∼ A and I n ∼ B. Applying Theorem_8_1_2_1 to these hypotheses, we can infer I m ×ₛ I n ∼ A ×ₛ B. If we can prove that I (m * n) ∼ I m ×ₛ I n, then we’ll be able to conclude I (m * n) ∼ A ×ₛ B, or in other words numElts (A ×ₛ B) (m * n), as required. Thus, the key to the proof is to show that I (m * n) ∼ I m ×ₛ I n.

To prove this, we’ll define a function from Nat to Nat × Nat that maps I (m * n) to I m ×ₛ I n. The function we will use maps a natural number a to the quotient and remainder when a is divided by n.

def qr (n a : Nat) : Nat × Nat := (a / n, a % n)

lemma qr_def (n a : Nat) : qr n a = (a / n, a % n) := by rfl

lemma qr_one_one (n : Nat) : one_to_one (qr n) := by
  define
  fix a1 : Nat; fix a2 : Nat
  assume h1 : qr n a1 = qr n a2       --Goal : a1 = a2
  rewrite [qr_def, qr_def] at h1
  have h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n := Prod.mk.inj h1
  show a1 = a2 from
    calc a1
      _ = n * (a1 / n) + a1 % n := (Nat.div_add_mod a1 n).symm
      _ = n * (a2 / n) + a2 % n := by rw [h2.left, h2.right]
      _ = a2 := Nat.div_add_mod a2 n
  done

lemma qr_image (m n : Nat) : image (qr n) (I (m * n)) = I m ×ₛ I n := sorry

lemma I_prod (m n : Nat) : I (m * n) ∼ I m ×ₛ I n := equinum_image
  (one_one_on_of_one_one (qr_one_one n) (I (m * n))) (qr_image m n)

theorem numElts_prod {U V : Type} {A : Set U} {B : Set V} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts B n) : numElts (A ×ₛ B) (m * n) := by
  rewrite [numElts_def] at h1     --h1 : I m ∼ A
  rewrite [numElts_def] at h2     --h2 : I n ∼ B
  rewrite [numElts_def]           --Goal : I (m * n) ∼ A ×ₛ B
  have h3 : I m ×ₛ I n ∼ A ×ₛ B := Theorem_8_1_2_1 h1 h2
  have h4 : I (m * n) ∼ I m ×ₛ I n := I_prod m n
  show I (m * n) ∼ A ×ₛ B from Theorem_8_1_3_3 h4 h3
  done

Our strategy for proving Theorem 7.4.4 will be to show that if m and n are relatively prime, then Set_rp_below (m * n) ∼ Set_rp_below m ×ₛ Set_rp_below n. Once again, we use a function from Nat to Nat × Nat to show that these sets are equinumerous. This time, the function will map a to (a % m, a % n).

def mod_mod (m n a : Nat) : Nat × Nat := (a % m, a % n)

lemma mod_mod_def (m n a : Nat) : mod_mod m n a = (a % m, a % n) := by rfl

Our proof will make use of several theorems from the exercises of Sections 7.3 and 7.4:

theorem congr_rel_prime {m a b : Nat} (h1 : a ≡ b (MOD m)) :
    rel_prime m a ↔ rel_prime m b := sorry

theorem rel_prime_mod (m a : Nat) :
    rel_prime m (a % m) ↔ rel_prime m a := sorry

theorem congr_iff_mod_eq_Nat (m a b : Nat) [NeZero m] :
    ↑a ≡ ↑b (MOD m) ↔ a % m = b % m := sorry

lemma Lemma_7_4_6 {a b c : Nat} :
    rel_prime (a * b) c ↔ rel_prime a c ∧ rel_prime b c := sorry

Combining these with other theorems from Chapter 7, we can now use mod_mod m n to show that Set_rp_below (m * n) ∼ Set_rp_below m ×ₛ Set_rp_below n.

lemma left_NeZero_of_mul {m n : Nat} (h : m * n ≠ 0) : NeZero m :=
  neZero_iff.rtl (left_ne_zero_of_mul h)

lemma right_NeZero_of_mul {m n : Nat} (h : m * n ≠ 0) : NeZero n :=
  neZero_iff.rtl (right_ne_zero_of_mul h)

lemma mod_mod_one_one_on {m n : Nat} (h1 : rel_prime m n) :
    one_one_on (mod_mod m n) (Set_rp_below (m * n)) := by
  define
  fix a1 : Nat; fix a2 : Nat
  assume h2 : a1 ∈ Set_rp_below (m * n)
  assume h3 : a2 ∈ Set_rp_below (m * n)
  assume h4 : mod_mod m n a1 = mod_mod m n a2   --Goal : a1 = a2
  define at h2; define at h3
  rewrite [mod_mod_def, mod_mod_def] at h4
  have h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n := Prod.mk.inj h4
  have h6 : m * n ≠ 0 := by linarith
  have h7 : NeZero m := left_NeZero_of_mul h6
  have h8 : NeZero n := right_NeZero_of_mul h6
  rewrite [←congr_iff_mod_eq_Nat, ←congr_iff_mod_eq_Nat] at h5
      --h5 : ↑a1 ≡ ↑a2 (MOD m) ∧ ↑a1 ≡ ↑a2 (MOD n)
  rewrite [←Lemma_7_4_5 _ _ h1] at h5  --h5 : ↑a1 ≡ ↑a2 (MOD m * n)
  rewrite [congr_iff_mod_eq_Nat] at h5 --h5 : a1 % (m * n) = a2 % (m * n)
  rewrite [Nat.mod_eq_of_lt h2.right, Nat.mod_eq_of_lt h3.right] at h5
  show a1 = a2 from h5
  done

lemma mod_elt_Set_rp_below {a m : Nat} [NeZero m] (h1 : rel_prime m a) :
    a % m ∈ Set_rp_below m := by
  define                  --Goal : rel_prime m (a % m) ∧ a % m < m
  rewrite [rel_prime_mod] --Goal : rel_prime m a ∧ a % m < m
  show rel_prime m a ∧ a % m < m from
    And.intro h1 (mod_nonzero_lt a (NeZero.ne m))
  done

lemma mod_mod_image {m n : Nat} (h1 : rel_prime m n) :
    image (mod_mod m n) (Set_rp_below (m * n)) =
      (Set_rp_below m) ×ₛ (Set_rp_below n) := by
  apply Set.ext
  fix (b, c) : Nat × Nat
  apply Iff.intro
  · -- (→)
    assume h2 : (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))
    define at h2
    obtain (a : Nat)
      (h3 : a ∈ Set_rp_below (m * n) ∧ mod_mod m n a = (b, c)) from h2
    rewrite [Set_rp_below_def, mod_mod_def] at h3
    have h4 : rel_prime (m * n) a := h3.left.left
    rewrite [Lemma_7_4_6] at h4   --h4 : rel_prime m a ∧ rel_prime n a
    have h5 : a % m = b ∧ a % n = c := Prod.mk.inj h3.right
    define
    rewrite [←h5.left, ←h5.right]
      --Goal : a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n
    have h6 : m * n ≠ 0 := by linarith
    have h7 : NeZero m := left_NeZero_of_mul h6
    have h8 : NeZero n := right_NeZero_of_mul h6
    apply And.intro
    · -- Proof that a % m ∈ Set_rp_below m
      show a % m ∈ Set_rp_below m from mod_elt_Set_rp_below h4.left
      done
    · -- Proof that a % n ∈ Set_rp_below n
      show a % n ∈ Set_rp_below n from mod_elt_Set_rp_below h4.right
      done
    done
  · -- (←)
    assume h2 : (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
    rewrite [Set_prod_def, Set_rp_below_def, Set_rp_below_def] at h2
      --h2 : (rel_prime m b ∧ b < m) ∧ (rel_prime n c ∧ c < n)
    define
    have h3 : m ≠ 0 := by linarith
    have h4 : n ≠ 0 := by linarith
    rewrite [←neZero_iff] at h3
    rewrite [←neZero_iff] at h4
    obtain (a : Nat) (h5 : a < m * n ∧ a ≡ b (MOD m) ∧ a ≡ c (MOD n))
      from Lemma_7_4_7 h1 b c
    apply Exists.intro a
    apply And.intro
    · -- Proof of a ∈ Set_rp_below (m * n)
      define                  --Goal : rel_prime (m * n) a ∧ a < m * n
      apply And.intro _ h5.left
      rewrite [Lemma_7_4_6]   --Goal : rel_prime m a ∧ rel_prime n a
      rewrite [congr_rel_prime h5.right.left,
        congr_rel_prime h5.right.right]
      show rel_prime m b ∧ rel_prime n c from
        And.intro h2.left.left h2.right.left
      done
    · -- Proof of mod_mod m n a = (b, c)
      rewrite [congr_iff_mod_eq_Nat, congr_iff_mod_eq_Nat] at h5
      rewrite [mod_mod_def, h5.right.left, h5.right.right]
        --Goal : (b % m, c % n) = (b, c)
      rewrite [Nat.mod_eq_of_lt h2.left.right,
        Nat.mod_eq_of_lt h2.right.right]
      rfl
      done
    done
  done

lemma Set_rp_below_prod {m n : Nat} (h1 : rel_prime m n) :
    Set_rp_below (m * n) ∼ (Set_rp_below m) ×ₛ (Set_rp_below n) :=
  equinum_image (mod_mod_one_one_on h1) (mod_mod_image h1)

We finally have everything we need to prove Theorem 7.4.4.

lemma eq_numElts_of_equinum {U V : Type} {A : Set U} {B : Set V} {n : Nat}
    (h1 : A ∼ B) (h2 : numElts A n) : numElts B n := by
  rewrite [numElts_def] at h2   --h2 : I n ∼ A
  rewrite [numElts_def]         --Goal : I n ∼ B
  show I n ∼ B from Theorem_8_1_3_3 h2 h1
  done

theorem Theorem_7_4_4 {m n : Nat} (h1 : rel_prime m n) :
    phi (m * n) = (phi m) * (phi n) := by
  have h2 : numElts (Set_rp_below m) (phi m) := phi_is_numElts m
  have h3 : numElts (Set_rp_below n) (phi n) := phi_is_numElts n
  have h4 : numElts (Set_rp_below (m * n)) (phi (m * n)) :=
    phi_is_numElts (m * n)
  have h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n)) :=
    eq_numElts_of_equinum (Set_rp_below_prod h1) h4
  have h6 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi m * phi n) :=
    numElts_prod h2 h3
  show phi (m * n) = phi m * phi n from numElts_unique h5 h6
  done

Exercises

lemma remove_one_iff {U V : Type}
    {A : Set U} {B : Set V} {R : Rel U V} (h1 : matching R A B)
    {u : U} (h2 : u ∈ A) (v : V) {x : U} (h3 : x ∈ A \ {u}) :
    ∃ w ∈ A, ∀ (y : V), remove_one R u v x y ↔ R w y := sorry

lemma inv_one_match {U V : Type} (a : U) (b : V) :
    invRel (one_match a b) = one_match b a := sorry

theorem one_match_fcnl {U V : Type} (a : U) (b : V) :
    fcnl_on (one_match a b) {a} := sorry

--Hint:  Use the previous two exercises.
lemma one_match_match {U V : Type} (a : U) (b : V) :
    matching (one_match a b) {a} {b} := sorry

lemma neb_nrpb (m : Nat) : ∀ ⦃k : Nat⦄, k ≤ m →
    num_elts_below (Set_rp_below m) k (num_rp_below m k) := sorry

lemma prod_fcnl {U V W X : Type} {R : Rel U V} {S : Rel W X}
    {A : Set U} {C : Set W} (h1 : fcnl_on R A) (h2 : fcnl_on S C) :
    fcnl_on (R ×ᵣ S) (A ×ₛ C) := sorry

--Hint:  Use the previous exercise.
lemma prod_match {U V W X : Type}
    {A : Set U} {B : Set V} {C : Set W} {D : Set X}
    {R : Rel U V} {S : Rel W X}
    (h1 : matching R A B) (h2 : matching S C D) :
    matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D) := sorry

--Hint:  You might find it helpful to apply the theorem div_mod_char
--from the exercises of Section 6.4.
lemma qr_image (m n : Nat) :
    image (qr n) (I (m * n)) = I m ×ₛ I n := sorry

theorem Theorem_8_1_2_2
    {U V : Type} {A C : Set U} {B D : Set V}
    (h1 : empty (A ∩ C)) (h2 : empty (B ∩ D))
    (h3 : A ∼ B) (h4 : C ∼ D) : A ∪ C ∼ B ∪ D := sorry

lemma shift_I_equinum (n m : Nat) : I m ∼ I (n + m) \ I n := sorry

theorem Theorem_8_1_7 {U : Type} {A B : Set U} {n m : Nat}
    (h1 : empty (A ∩ B)) (h2 : numElts A n) (h3 : numElts B m) :
    numElts (A ∪ B) (n + m) := sorry

theorem equinum_sub {U V : Type} {A C : Set U} {B : Set V}
    (h1 : A ∼ B) (h2 : C ⊆ A) : ∃ (D : Set V), D ⊆ B ∧ C ∼ D := sorry

theorem Exercise_8_1_8b {U : Type} {A B : Set U}
    (h1 : finite A) (h2 : B ⊆ A) : finite B := sorry

--Hint:  Use Like_Exercise_6_2_16 from the exercises of Section 6.2
lemma N_not_finite : ¬finite (Univ Nat) := sorry

theorem denum_not_finite {U : Type} {A : Set U}
    (h : denum A) : ¬finite A := sorry

8.2. Countable and Uncountable Sets

Section 8.2 of HTPI shows that many set-theoretic operations, when applied to countable sets, produce results that are countable. For example, the first part of Theorem 8.2.1 shows that a Cartesian product of countable sets is countable. Our proof of this statement in Lean is based on Theorem_8_1_2_1 and the countability of Univ (Nat × Nat). We also use an exercise from Section 8.1.

theorem Exercise_8_1_17 {U : Type} {A B : Set U}
    (h1 : B ⊆ A) (h2 : ctble A) : ctble B := sorry

theorem Theorem_8_2_1_1 {U V : Type} {A : Set U} {B : Set V}
    (h1 : ctble A) (h2 : ctble B) : ctble (A ×ₛ B) := by
  rewrite [ctble_iff_equinum_set_nat] at h1
  rewrite [ctble_iff_equinum_set_nat] at h2
  obtain (I : Set Nat) (h3 : I ∼ A) from h1
  obtain (J : Set Nat) (h4 : J ∼ B) from h2
  have h5 : I ×ₛ J ∼ A ×ₛ B := Theorem_8_1_2_1 h3 h4
  have h6 : I ×ₛ J ⊆ Univ (Nat × Nat) := by
    fix p : Nat × Nat
    assume h6 : p ∈ I ×ₛ J
    show p ∈ Univ (Nat × Nat) from elt_Univ p
    done
  have h7 : ctble (Univ (Nat × Nat)) := by
    define   --Goal : finite (Univ (Nat × Nat)) ∨ denum (Univ (Nat × Nat))
    apply Or.inr
    rewrite [denum_def]
    show Univ Nat ∼ Univ (Nat × Nat) from Theorem_8_1_3_2 NxN_equinum_N
    done
  have h8 : ctble (I ×ₛ J) := Exercise_8_1_17 h6 h7
  show ctble (A ×ₛ B) from ctble_of_equinum_ctble h5 h8
  done

The second part of Theorem 8.2.1 shows that a union of two countable sets is countable, but, as we ask you to show in the exercises, it is superseded by Theorem 8.2.2, which says that a union of a countable family of countable sets is countable. So we will skip ahead to Theorem 8.2.2. Here’s how we state the theorem in Lean:

theorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}
    (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F)

In our proof, we will use the characterization of countability from Theorem_8_1_5_2. Thus, we will use the hypotheses h1 and h2 to conclude that there is a relation R : Rel Nat (Set U) such that fcnl_onto_from_nat R F, and also that for each A ∈ F there is a relation SA : Rel Nat U such that fcnl_onto_from_nat SA A. We begin by proving an easier version of the theorem, where we assume that we have a function f : Set U → Rel Nat U that supplies, for each A ∈ F, the required relation SA. Imitating the proof in HTPI, we can use R and f to construct the relation needed to prove that ⋃₀ F is countable.

def enum_union_fam {U : Type}
  (F : Set (Set U)) (f : Set U → Rel Nat U) (R : Rel Nat (Set U))
  (n : Nat) (a : U) : Prop := ∃ (p : Nat × Nat), fnnn p = n ∧
    ∃ A ∈ F, R p.1 A ∧ (f A) p.2 a

lemma Lemma_8_2_2_1 {U : Type} {F : Set (Set U)} {f : Set U → Rel Nat U}
    (h1 : ctble F) (h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A) :
    ctble (⋃₀ F) := by
  rewrite [Theorem_8_1_5_2] at h1
  rewrite [Theorem_8_1_5_2]
  obtain (R : Rel Nat (Set U)) (h3 : fcnl_onto_from_nat R F) from h1
  define at h3
  have Runiqueval : unique_val_on_N R := h3.left
  have Ronto : nat_rel_onto R F := h3.right
  set S : Rel Nat U := enum_union_fam F f R
  apply Exists.intro S
  define
  apply And.intro
  · -- Proof of unique_val_on_N S
    define
    fix n : Nat; fix a1 : U; fix a2 : U
    assume Sna1 : S n a1
    assume Sna2 : S n a2         --Goal : a1 = a2
    define at Sna1; define at Sna2
    obtain ((i1, j1) : Nat × Nat) (h4 : fnnn (i1, j1) = n ∧
      ∃ A ∈ F, R i1 A ∧ f A j1 a1) from Sna1
    obtain (A1 : Set U) (Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1)
      from h4.right
    obtain ((i2, j2) : Nat × Nat) (h5 : fnnn (i2, j2) = n ∧
      ∃ A ∈ F, R i2 A ∧ f A j2 a2) from Sna2
    obtain (A2 : Set U) (Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2)
      from h5.right
    rewrite [←h5.left] at h4
    have h6 : (i1, j1) = (i2, j2) :=
      fnnn_one_one (i1, j1) (i2, j2) h4.left
    have h7 : i1 = i2 ∧ j1 = j2 := Prod.mk.inj h6
    rewrite [h7.left, h7.right] at Aija1
      --Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1
    define at Runiqueval
    have h8 : A1 = A2 := Runiqueval Aija1.right.left Aija2.right.left
    rewrite [h8] at Aija1       --Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
    have fA2fcnlonto : fcnl_onto_from_nat (f A2) A2 := h2 A2 Aija2.left
    define at fA2fcnlonto
    have fA2uniqueval : unique_val_on_N (f A2) := fA2fcnlonto.left
    define at fA2uniqueval
    show a1 = a2 from fA2uniqueval Aija1.right.right Aija2.right.right
    done
  · -- Proof of nat_rel_onto S (⋃₀ F)
    define
    fix x : U
    assume h4 : x ∈ ⋃₀ F    --Goal : ∃ (n : Nat), S n x
    define at h4
    obtain (A : Set U) (h5 : A ∈ F ∧ x ∈ A) from h4
    define at Ronto
    obtain (i : Nat) (h6 : R i A) from Ronto h5.left
    have fAfcnlonto : fcnl_onto_from_nat (f A) A := h2 A h5.left
    define at fAfcnlonto
    have fAonto : nat_rel_onto (f A) A := fAfcnlonto.right
    define at fAonto
    obtain (j : Nat) (h7 : f A j x) from fAonto h5.right
    apply Exists.intro (fnnn (i, j))
    define    --Goal : ∃ (p : Nat × Nat), fnnn p = fnnn (i, j) ∧
              --       ∃ A ∈ F, R p.1 A ∧ f A p.2 x
    apply Exists.intro (i, j)
    apply And.intro
    · -- Proof that fnnn (i, j) = fnnn (i, j)
      rfl
      done
    · -- Proof that ∃ A ∈ F, R (i, j).1 A ∧ f A (i, j).2 x
      apply Exists.intro A
      show A ∈ F ∧ R (i, j).1 A ∧ f A (i, j).2 x from
        And.intro h5.left (And.intro h6 h7)
      done
    done
  done

How can we use Lemma_8_2_2_1 to prove Theorem_8_2_2? We must use the hypothesis h2 : ∀ A ∈ F, ctble A in Theorem_8_2_2 to produce the function f required in Lemma_8_2_2_1. As we have already observed, Theorem_8_1_5_2 guarantees that for each A ∈ F, an appropriate relation SA : Rel Nat U exists. We need a function f that will choose such a relation SA for each A. A function with this property is often called a choice function. And now we come to a delicate point that was skipped over in HTPI: to prove the existence of a choice function, we must use a statement called the axiom of choice.¹

The distinction between the existence of an appropriate relation SA for each A and the existence of a function that chooses such a relation for each A is a subtle one. Perhaps for this reason, many people find the axiom of choice to be intuitively obvious. HTPI took advantage of this intuition to skip over this step in the proof without comment. But of course Lean won’t let us skip anything!

To implement the axiom of choice, Lean uses a function called Classical.choose. Given a proof h of a statement of the form ∃ (x : U), P x, the expression Classical.choose h produces (“chooses”) some u : U such that P u is true. There is also a theorem Classical.choose_spec that guarantees that the Classical.choose function meets its specification—that is, P (Classical.choose h) is true. Using these, we can prove a lemma that will bridge the gap between Lemma_8_2_2_1 and Theorem_8_2_2.

lemma Lemma_8_2_2_2 {U : Type} {F : Set (Set U)} (h : ∀ A ∈ F, ctble A) :
    ∃ (f : Set U → Rel Nat U), ∀ A ∈ F, fcnl_onto_from_nat (f A) A := by
  have h1 : ∀ (A : Set U), ∃ (SA : Rel Nat U),
      A ∈ F → fcnl_onto_from_nat SA A := by
    fix A : Set U
    by_cases h2 : A ∈ F
    · -- Case 1. h2 : A ∈ F
      have h3 : ctble A := h A h2
      rewrite [Theorem_8_1_5_2] at h3
      obtain (SA : Rel Nat U) (h4 : fcnl_onto_from_nat SA A) from h3
      apply Exists.intro SA
      assume h5 : A ∈ F
      show fcnl_onto_from_nat SA A from h4
      done
    · -- Case 2. h2 : A ∉ F
      apply Exists.intro (emptyRel Nat U)
      assume h3 : A ∈ F
      show fcnl_onto_from_nat (emptyRel Nat U) A from absurd h3 h2
      done
    done
  set f : Set U → Rel Nat U := fun (A : Set U) => Classical.choose (h1 A)
  apply Exists.intro f
  fix A : Set U
  show A ∈ F → fcnl_onto_from_nat (f A) A from Classical.choose_spec (h1 A)
  done

Notice that the domain of the function f in Lemma_8_2_2_2 is Set U, not F. Thus, we must produce a relation SA for every A : Set U, but it is only when A ∈ F that we care what SA is. Thus, the proof above just picks a default value (emptyRel Nat U) when A ∉ F.

We now have everything in place to prove Theorem_8_2_2:

theorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}
    (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F) := by
  obtain (f : Set U → Rel Nat U) (h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A)
    from Lemma_8_2_2_2 h2
  show ctble (⋃₀ F) from Lemma_8_2_2_1 h1 h3
  done

By the way, we can now explain a mystery from Section 5.1. The reason we skipped the proof of the right-to-left direction of func_from_graph is that the proof uses Classical.choose and Classical.choose_spec. Now that you know about this function and theorem, we can show you the proof.

theorem func_from_graph_rtl {A B : Type} (F : Set (A × B)) :
    is_func_graph F → (∃ (f : A → B), graph f = F) := by
  assume h1 : is_func_graph F
  define at h1    --h1 : ∀ (x : A), ∃! (y : B), (x, y) ∈ F
  have h2 : ∀ (x : A), ∃ (y : B), (x, y) ∈ F := by
    fix x : A
    obtain (y : B) (h3 : (x, y) ∈ F)
      (h4 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
    show ∃ (y : B), (x, y) ∈ F from Exists.intro y h3
    done
  set f : A → B := fun (x : A) => Classical.choose (h2 x)
  apply Exists.intro f
  apply Set.ext
  fix (x, y) : A × B
  have h3 : (x, f x) ∈ F := Classical.choose_spec (h2 x)
  apply Iff.intro
  · -- (→)
    assume h4 : (x, y) ∈ graph f
    define at h4        --h4 : f x = y
    rewrite [h4] at h3
    show (x, y) ∈ F from h3
    done
  · -- (←)
    assume h4 : (x, y) ∈ F
    define              --Goal : f x = y
    obtain (z : B) (h5 : (x, z) ∈ F)
      (h6 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
    show f x = y from h6 (f x) y h3 h4
    done
  done

There is one more theorem in Section 8.2 of HTPI showing that a set-theoretic operation, when applied to a countable set, gives a countable result. Theorem 8.2.4 says that if a set \(A\) is countable, then the set of all finite sequences of elements of \(A\) is also countable. In HTPI, finite sequences are represented by functions, but in Lean it is easier to use lists. Thus, if A has type Set U, then we define a finite sequence of elements of A to be a list l : List U with the property that every entry of l is an element of A. Letting seq A denote the set of all finite sequences of elements of A, our version of Theorem 8.2.4 will say that if A is countable, then so is seq A.

def seq {U : Type} (A : Set U) : Set (List U) :=
  {l : List U | ∀ x ∈ l, x ∈ A}

lemma seq_def {U : Type} (A : Set U) (l : List U) :
    l ∈ seq A ↔ ∀ x ∈ l, x ∈ A := by rfl

theorem Theorem_8_2_4 {U : Type} {A : Set U}
    (h1 : ctble A) : ctble (seq A)

Our proof of Theorem_8_2_4 will use exactly the same strategy as the proof in HTPI. We begin by showing that, for every natural number n, the set of sequences of elements of A of length n is countable. The proof is by mathematical induction. The base case is easy, because the only sequence of length 0 is the nil list.

def seq_by_length {U : Type} (A : Set U) (n : Nat) : Set (List U) :=
  {l : List U | l ∈ seq A ∧ l.length = n}

lemma sbl_base {U : Type} (A : Set U) : seq_by_length A 0 = {[]} := by
  apply Set.ext
  fix l : List U
  apply Iff.intro
  · -- (→)
    assume h1 : l ∈ seq_by_length A 0
    define at h1   --h1 : l ∈ seq A ∧ l.length = 0
    rewrite [List.length_eq_zero] at h1
    define
    show l = [] from h1.right
    done
  · -- (←)
    assume h1 : l ∈ {[]}
    define at h1     --h1 : l = []
    define           --Goal : l ∈ seq A ∧ l.length = 0
    apply And.intro _ (List.length_eq_zero.rtl h1)
    define           --Goal : ∀ x ∈ l, x ∈ A
    fix x : U
    assume h2 : x ∈ l
    contradict h2 with h3
    rewrite [h1]
    show x ∉ [] from List.not_mem_nil x
    done
  done

For the induction step, the key idea is that A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1). To prove this, we define a function seq_cons U that matches up A ×ₛ (seq_by_length A n) with seq_by_length A (n + 1).

def seq_cons (U : Type) (p : U × (List U)) : List U := p.1 :: p.2

lemma seq_cons_def {U : Type} (x : U) (l : List U) :
    seq_cons U (x, l) = x :: l := by rfl

lemma seq_cons_one_one (U : Type) : one_to_one (seq_cons U) := by
  fix (a1, l1) : U × List U; fix (a2, l2) : U × List U
  assume h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)
  rewrite [seq_cons_def, seq_cons_def] at h1  --h1 : a1 :: l1 = a2 :: l2
  rewrite [List.cons_eq_cons] at h1           --h1 : a1 = a2 ∧ l1 = l2
  rewrite [h1.left, h1.right]
  rfl
  done

lemma seq_cons_image {U : Type} (A : Set U) (n : Nat) :
    image (seq_cons U) (A ×ₛ (seq_by_length A n)) =
      seq_by_length A (n + 1) := sorry

lemma Lemma_8_2_4_1 {U : Type} (A : Set U) (n : Nat) :
    A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) :=
  equinum_image (one_one_on_of_one_one (seq_cons_one_one U)
    (A ×ₛ (seq_by_length A n))) (seq_cons_image A n)

With this preparation, we can now use singleton_one_elt to justify the base case of our induction proof and Theorem_8_2_1_1 for the induction step.

lemma Lemma_8_2_4_2 {U : Type} {A : Set U} (h1 : ctble A) :
    ∀ (n : Nat), ctble (seq_by_length A n) := by
  by_induc
  · -- Base Case
    rewrite [sbl_base]   --Goal : ctble {[]}
    define
    apply Or.inl         --Goal : finite {[]}
    rewrite [finite_def]
    apply Exists.intro 1 --Goal : numElts {[]} 1
    show numElts {[]} 1 from singleton_one_elt []
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ctble (seq_by_length A n)
    have h2 : A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) :=
      Lemma_8_2_4_1 A n
    have h3 : ctble (A ×ₛ (seq_by_length A n)) := Theorem_8_2_1_1 h1 ih
    show ctble (seq_by_length A (n + 1)) from ctble_of_equinum_ctble h2 h3
    done
  done

Our next step is to show that the union of all of the sets seq_by_length A n, for n : Nat, is seq A.

def sbl_set {U : Type} (A : Set U) : Set (Set (List U)) :=
  {S : Set (List U) | ∃ (n : Nat), seq_by_length A n = S}

lemma Lemma_8_2_4_3 {U : Type} (A : Set U) : ⋃₀ (sbl_set A) = seq A := by
  apply Set.ext
  fix l : List U
  apply Iff.intro
  · -- (→)
    assume h1 : l ∈ ⋃₀ (sbl_set A)
    define at h1
    obtain (S : Set (List U)) (h2 :  S ∈ sbl_set A ∧ l ∈ S) from h1
    have h3 : S ∈ sbl_set A := h2.left
    define at h3
    obtain (n : Nat) (h4 : seq_by_length A n = S) from h3
    have h5 : l ∈ S := h2.right
    rewrite [←h4] at h5
    define at h5
    show l ∈ seq A from h5.left
    done
  · -- (←)
    assume h1 : l ∈ seq A
    define
    set n : Nat := l.length
    apply Exists.intro (seq_by_length A n)
    apply And.intro
    · -- Proof of seq_by_length A n ∈ sbl_set A
      define
      apply Exists.intro n
      rfl
      done
    · -- Proof of l ∈ seq_by_length A n
      define
      apply And.intro h1
      rfl
      done
    done
  done

Of course, sbl_set A is countable. The easiest way to prove this is to apply an exercise from Section 8.1.

theorem ctble_of_onto_func_from_N {U : Type} {A : Set U} {f : Nat → U}
    (h1 : ∀ x ∈ A, ∃ (n : Nat), f n = x) : ctble A := sorry

lemma Lemma_8_2_4_4 {U : Type} (A : Set U) : ctble (sbl_set A) := by
  have h1 : ∀ S ∈ sbl_set A, ∃ (n : Nat), seq_by_length A n = S := by
    fix S : Set (List U)
    assume h1 : S ∈ sbl_set A
    define at h1
    show ∃ (n : Nat), seq_by_length A n = S from h1
    done
  show ctble (sbl_set A) from ctble_of_onto_func_from_N h1
  done

We now have everything we need to prove Theorem_8_2_4 as an application of Theorem_8_2_2.

theorem Theorem_8_2_4 {U : Type} {A : Set U}
    (h1 : ctble A) : ctble (seq A) := by
  set F : Set (Set (List U)) := sbl_set A
  have h2 : ctble F := Lemma_8_2_4_4 A
  have h3 : ∀ S ∈ F, ctble S := by
    fix S : Set (List U)
    assume h3 : S ∈ F
    define at h3
    obtain (n : Nat) (h4 : seq_by_length A n = S) from h3
    rewrite [←h4]
    show ctble (seq_by_length A n) from Lemma_8_2_4_2 h1 n
    done
  rewrite [←Lemma_8_2_4_3 A]
  show ctble (⋃₀ sbl_set A) from Theorem_8_2_2 h2 h3
  done

There is a set-theoretic operation that can produce an uncountable set from a countable set: the power set operation. HTPI demonstrates this by proving Cantor’s theorem (Theorem 8.2.5), which says that \(\mathscr{P}(\mathbb{Z}^+)\) is uncountable. The strategy for this proof is tricky; it involves defining a set \(D\) using a method called diagonalization. For an explanation of the motivation behind this strategy, see HTPI. Here we will use this strategy to prove that 𝒫 (Univ Nat) is uncountable.

lemma set_elt_powerset_univ {U : Type} (A : Set U) :
    A ∈ 𝒫 (Univ U) := by
  fix x : U
  assume h : x ∈ A
  show x ∈ Univ U from elt_Univ x
  done

theorem Cantor's_theorem : ¬ctble (𝒫 (Univ Nat)) := by
  by_contra h1
  rewrite [Theorem_8_1_5_2] at h1
  obtain (R : Rel Nat (Set Nat))
    (h2 : fcnl_onto_from_nat R (𝒫 (Univ Nat))) from h1
  define at h2
  have h3 : unique_val_on_N R := h2.left
  have h4 : nat_rel_onto R (𝒫 (Univ Nat)) := h2.right
  set D : Set Nat := {n : Nat | ∃ (X : Set Nat), R n X ∧ n ∉ X}
  have h5 : D ∈ 𝒫 (Univ Nat) := set_elt_powerset_univ D
  define at h4
  obtain (n : Nat) (h6 : R n D) from h4 h5
  by_cases h7 : n ∈ D
  · -- Case 1. h7 : n ∈ D
    contradict h7
    define at h7
    obtain (X : Set Nat) (h8 : R n X ∧ n ∉ X) from h7
    define at h3
    have h9 : D = X := h3 h6 h8.left
    rewrite [h9]
    show n ∉ X from h8.right
    done
  · -- Case 2. h7 : n ∉ D
    contradict h7
    define
    show ∃ (X : Set Nat), R n X ∧ n ∉ X from
      Exists.intro D (And.intro h6 h7)
    done
  done

As a consequence of Theorem 8.2.5, HTPI shows that \(\mathbb{R}\) is uncountable. The proof is not hard, but it requires facts about the decimal expansions of real numbers. Developing those facts in Lean would take us too far afield, so we will skip the proof.

Exercises

lemma pair_ctble {U : Type} (a b : U) : ctble {a, b} := sorry

--Hint:  Use the previous exercise and Theorem_8_2_2
theorem Theorem_8_2_1_2 {U : Type} {A B : Set U}
    (h1 : ctble A) (h2 : ctble B) : ctble (A ∪ B) := sorry

lemma seq_cons_image {U : Type} (A : Set U) (n : Nat) :
    image (seq_cons U) (A ×ₛ (seq_by_length A n)) =
      seq_by_length A (n + 1) := sorry

--Hint:  Use induction on the size of A
lemma set_to_list {U : Type} {A : Set U} (h : finite A) :
    ∃ (l : List U), ∀ (x : U), x ∈ l ↔ x ∈ A := sorry

--Hint:  Use the previous exercise and Theorem_8_2_4
theorem Like_Exercise_8_2_4 {U : Type} {A : Set U} (h : ctble A) :
    ctble {X : Set U | X ⊆ A ∧ finite X} := sorry

theorem Exercise_8_2_6b (A B C : Type) :
    Univ ((A × B) → C) ∼ Univ (A → (B → C)) := sorry

theorem Like_Exercise_8_2_7 : ∃ (P : Set (Set Nat)),
    partition P ∧ denum P ∧ ∀ X ∈ P, denum X := sorry

theorem unctbly_many_inf_set_nat :
    ¬ctble {X : Set Nat | ¬finite X} := sorry

theorem Exercise_8_2_8 {U : Type} {A B : Set U}
    (h : empty (A ∩ B)) : 𝒫 (A ∪ B) ∼ 𝒫 A ×ₛ 𝒫 B := sorry

8.3. The Cantor–Schröder–Bernstein Theorem

The final section of HTPI proves the Cantor–Schröder–Bernstein theorem. The theorem says that if \(A\) and \(B\) are sets such that each is equinumerous with a subset of the other, then \(A\) and \(B\) are equinumerous. In the notation we are using in this chapter, it can be stated as follows:

theorem Cantor_Schroeder_Bernstein_theorem
    {U V : Type} {A C : Set U} {B D : Set V}
    (h1 : C ⊆ A) (h2 : D ⊆ B) (h3 : A ∼ D) (h4 : C ∼ B) : A ∼ B

The hypotheses h3 and h4 imply that there are matchings R from A to D and S from C to B. To prove the theorem, we must construct a matching T from A to B. Imitating the proof in HTPI, we will do this by defining a set X ⊆ A and then combining R restricted to X with S restricted to A \ X. In other words, T x y will be defined to mean:

(x ∈ X ∧ R x y) ∨ (x ∉ X ∧ S x y)

Which elements of A should be in X? We start with the fact that, since S is a relation within C and B, elements of A \ C are not paired with anything by S, so they must be in X. In other words, if we define X0 to be A \ C, then we must have X0 ⊆ X.

Now suppose x ∈ X0, a ∈ A, y ∈ B, and R x y and S a y are both true. In this situation we will say that x and a have a common image under R and S. If a ∉ X, then we will have T x y and T a y, which means that T will fail to be a matching. Thus, we must have a ∈ X. In other words, if we define X1 to be the set of all a such that for some x ∈ X0, x and a have a common image under R and S, then we’ll need to have X1 ⊆ X. But now the same reasoning applies to X1: if X2 is the set of all a such that for some x ∈ X1, x and a have a common image, then X2 must also be contained in X. Iterating this reasoning motivates the following definition:

def rep_common_image
  {U V : Type} (R S : Rel U V) (X0 : Set U) (n : Nat) : Set U :=
  match n with
    | 0 => X0
    | m + 1 => {a : U | ∃ x ∈ rep_common_image R S X0 m,
                          ∃ (y : V), R x y ∧ S a y}

lemma rep_common_image_step
    {U V : Type} (R S : Rel U V) (X0 : Set U) (m : Nat) (a : U) :
    a ∈ rep_common_image R S X0 (m + 1) ↔
    ∃ x ∈ rep_common_image R S X0 m, ∃ (y : V), R x y ∧ S a y := by rfl

The sets rep_common_image R S X0 n correspond to the sets \(A_n\) in HTPI. As in HTPI, to define X we take the union of these sets.

def cum_rep_image {U V : Type} (R S : Rel U V) (X0 : Set U) : Set U :=
  {a : U | ∃ (n : Nat), a ∈ rep_common_image R S X0 n}

In our proof of the Cantor–Schröder–Bernstein theorem, we will define X to be the set cum_rep_image R S X0, and therefore the matching T will be the relation csb_match R S X0 defined as follows:

def csb_match {U V : Type} (R S : Rel U V) (X0 : Set U)
  (x : U) (y : V) : Prop := x ∈ cum_rep_image R S X0 ∧ R x y ∨
    x ∉ cum_rep_image R S X0 ∧ S x y

It will be convenient to prove a few simple lemmas about these definitions. Our first two lemmas spell out that, for x ∈ X, T x y means R x y, and for x ∉ X, T x y means S x y.

lemma csb_match_cri {U V : Type} {R S : Rel U V} {X0 : Set U}
    {x : U} {y : V} (h1 : csb_match R S X0 x y)
    (h2 : x ∈ cum_rep_image R S X0) : R x y := by
  by_cases on h1
  · -- Case 1. h1 : x ∈ cum_rep_image R S X0 ∧ R x y
    show R x y from h1.right
    done
  · -- Case 2. h1 : x ∉ cum_rep_image R S X0 ∧ S x y
    show R x y from absurd h2 h1.left
    done
  done

lemma csb_match_not_cri {U V : Type} {R S : Rel U V} {X0 : Set U}
    {x : U} {y : V} (h1 : csb_match R S X0 x y)
    (h2 : x ∉ cum_rep_image R S X0) : S x y := sorry

We will also need to know that it cannot happen that T x1 y, T x2 y, x1 ∈ X, and x2 ∉ X:

lemma csb_cri_of_cri
    {U V : Type} {R S : Rel U V} {X0 : Set U} {x1 x2 : U} {y : V}
    (h1 : csb_match R S X0 x1 y) (h2 : csb_match R S X0 x2 y)
    (h3 : x1 ∈ cum_rep_image R S X0) : x2 ∈ cum_rep_image R S X0 := by
  have h4 : R x1 y := csb_match_cri h1 h3
  by_contra h5
  have h6 : S x2 y := csb_match_not_cri h2 h5
  contradict h5       --Goal : x2 ∈ cum_rep_image R S X0
  define at h3
  define
  obtain (n : Nat) (h7 : x1 ∈ rep_common_image R S X0 n) from h3
  apply Exists.intro (n + 1)  --Goal : x2 ∈ rep_common_image R S X0 (n + 1)
  rewrite [rep_common_image_step]
  apply Exists.intro x1
    --Goal : x1 ∈ rep_common_image R S X0 n ∧ ∃ (y : V), R x1 y ∧ S x2 y
  apply And.intro h7
  show ∃ (y : V), R x1 y ∧ S x2 y from Exists.intro y (And.intro h4 h6)
  done

With that preparation, we are ready to prove the theorem.

theorem Cantor_Schroeder_Bernstein_theorem
    {U V : Type} {A C : Set U} {B D : Set V}
    (h1 : C ⊆ A) (h2 : D ⊆ B) (h3 : A ∼ D) (h4 : C ∼ B) : A ∼ B := by
  obtain (R : Rel U V) (R_match_AD : matching R A D) from h3
  obtain (S : Rel U V) (S_match_CB : matching S C B) from h4
  define at R_match_AD; define at S_match_CB
  set X0 : Set U := A \ C
  set X : Set U := cum_rep_image R S X0
  set T : Rel U V := csb_match R S X0
  have Tdef : ∀ (x : U) (y : V),
      T x y ↔ (x ∈ X ∧ R x y) ∨ (x ∉ X ∧ S x y) := by
    fix x : U; fix y : V
    rfl
    done
  have A_not_X_in_C : A \ X ⊆ C := by
    fix a : U
    assume h5 : a ∈ A \ X
    contradict h5.right with h6  --h6 : a ∉ C;  Goal : a ∈ X
    define  --Goal : ∃ (n : Nat), a ∈ rep_common_image R S X0 n
    apply Exists.intro 0 
    define
    show a ∈ A ∧ a ∉ C from And.intro h5.left h6
    done
  define    --Goal : ∃ (R : Rel U V), matching R A B
  apply Exists.intro T
  define    --Goal : rel_within T A B ∧ fcnl_on T A ∧ fcnl_on (invRel T) B
  apply And.intro
  · -- Proof of rel_within T A B
    define
    fix a : U; fix b : V
    assume h5 : T a b
    rewrite [Tdef] at h5   --h5 : a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b
    by_cases on h5
    · -- Case 1. h5 : a ∈ X ∧ R a b
      have h6 : a ∈ A ∧ b ∈ D := R_match_AD.left h5.right
      show a ∈ A ∧ b ∈ B from And.intro h6.left (h2 h6.right)
      done
    · -- Case 2. h5 : a ∉ X ∧ S a b
      have h6 : a ∈ C ∧ b ∈ B := S_match_CB.left h5.right
      show a ∈ A ∧ b ∈ B from And.intro (h1 h6.left) h6.right
      done
    done
  · -- Proof of fcnl_ons
    apply And.intro
    · -- Proof of fcnl_on T A
      define
      fix a : U
      assume aA : a ∈ A   --Goal : ∃! (y : V), T a y
      exists_unique
      · -- Existence
        by_cases h5 : a ∈ X
        · -- Case 1. h5 : a ∈ X
          obtain (b : V) (Rab : R a b) from
            fcnl_exists R_match_AD.right.left aA
          apply Exists.intro b
          rewrite [Tdef]
          show a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b from
            Or.inl (And.intro h5 Rab)
          done
        · -- Case 2. h5 : a ∉ X
          have aC : a ∈ C := A_not_X_in_C (And.intro aA h5)
          obtain (b : V) (Sab : S a b) from
            fcnl_exists S_match_CB.right.left aC
          apply Exists.intro b
          rewrite [Tdef]
          show a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b from
            Or.inr (And.intro h5 Sab)
          done
        done
      · -- Uniqueness
        fix b1 : V; fix b2 : V
        assume Tab1 : T a b1
        assume Tab2 : T a b2
        by_cases h5 : a ∈ X
        · -- Case 1. h5 : a ∈ X
          have Rab1 : R a b1 := csb_match_cri Tab1 h5
          have Rab2 : R a b2 := csb_match_cri Tab2 h5
          show b1 = b2 from
            fcnl_unique R_match_AD.right.left aA Rab1 Rab2
          done
        · -- Case 2. h5 : a ∉ X
          have Sab1 : S a b1 := csb_match_not_cri Tab1 h5
          have Sab2 : S a b2 := csb_match_not_cri Tab2 h5
          have aC : a ∈ C := A_not_X_in_C (And.intro aA h5)
          show b1 = b2 from
            fcnl_unique S_match_CB.right.left aC Sab1 Sab2
          done
        done
      done
    · -- Proof of fcnl_on (invRel T) B
      define
      fix b : V
      assume bB : b ∈ B
      obtain (c : U) (Scb : S c b) from
        fcnl_exists S_match_CB.right.right bB
      have cC : c ∈ C := (S_match_CB.left Scb).left
      exists_unique
      · -- Existence
        by_cases h5 : c ∈ X
        · -- Case 1. h5 : c ∈ X
          define at h5
          obtain (n : Nat) (h6 : c ∈ rep_common_image R S X0 n) from h5
          have h7 : n ≠ 0 := by
            by_contra h7
            rewrite [h7] at h6
            define at h6       --h6 : c ∈ A ∧ c ∉ C
            show False from h6.right cC
            done
          obtain (m : Nat) (h8 : n = m + 1) from
            exists_eq_add_one_of_ne_zero h7
          rewrite [h8] at h6
          rewrite [rep_common_image_step] at h6
          obtain (a : U) (h9 : a ∈ rep_common_image R S X0 m ∧
            ∃ (y : V), R a y ∧ S c y) from h6
          apply Exists.intro a
          rewrite [invRel_def, Tdef]
          apply Or.inl    --Goal : a ∈ X ∧ R a b
          obtain (y : V) (h10 : R a y ∧ S c y) from h9.right
          have h11 : y = b :=
            fcnl_unique S_match_CB.right.left cC h10.right Scb
          rewrite [h11] at h10
          apply And.intro _ h10.left
          define
          show ∃ (n : Nat), a ∈ rep_common_image R S X0 n from
            Exists.intro m h9.left
          done
        · -- Case 2. h5 : c ∉ X
          apply Exists.intro c
          rewrite [invRel_def, Tdef]
          show c ∈ X ∧ R c b ∨ c ∉ X ∧ S c b from
            Or.inr (And.intro h5 Scb)
          done
        done
      · -- Uniqueness
        fix a1 : U; fix a2 : U
        assume Ta1b : T a1 b
        assume Ta2b : T a2 b
        by_cases h5 : a1 ∈ X
        · -- Case 1. h5 : a1 ∈ X
          have h6 : a2 ∈ X := csb_cri_of_cri Ta1b Ta2b h5
          have Ra1b : R a1 b := csb_match_cri Ta1b h5
          have Ra2b : R a2 b := csb_match_cri Ta2b h6
          have h7 : b ∈ D := (R_match_AD.left Ra1b).right
          show a1 = a2 from
            fcnl_unique R_match_AD.right.right h7 Ra1b Ra2b
          done
        · -- Case 2. h5 : a1 ∉ X
          have h6 : a2 ∉ X := by
            by_contra h6
            show False from h5 (csb_cri_of_cri Ta2b Ta1b h6)
            done
          have Sa1b : S a1 b := csb_match_not_cri Ta1b h5
          have Sa2b : S a2 b := csb_match_not_cri Ta2b h6
          show a1 = a2 from
            fcnl_unique S_match_CB.right.right bB Sa1b Sa2b
          done
        done
      done
    done
  done

Exercises

theorem CSB_func {U V : Type} {f : U → V} {g : V → U}
    (h1 : one_to_one f) (h2 : one_to_one g) : Univ U ∼ Univ V := sorry

theorem intervals_equinum :
    {x : Real | 0 < x ∧ x < 1} ∼ {x : Real | 0 < x ∧ x ≤ 1} := sorry

The next six exercises lead up to a proof that the set of all equivalence relations on the natural numbers is equinumerous with the power set of the natural numbers. These exercises use the following definitions:

def EqRel (A : Type) : Set (BinRel A) :=
  {R : BinRel A | equiv_rel R}

def Part (A : Type) : Set (Set (Set A)) :=
  {P : Set (Set A) | partition P}

def EqRelExt (A : Type) : Set (Set (A × A)) :=
  {E : Set (A × A) | ∃ (R : BinRel A), equiv_rel R ∧ extension R = E}

def shift_and_zero (X : Set Nat) : Set Nat :=
  {x + 2 | x ∈ X} ∪ {0}

def saz_pair (X : Set Nat) : Set (Set Nat) :=
  {shift_and_zero X, (Univ Nat) \ (shift_and_zero X)}

theorem EqRel_equinum_Part (A : Type) : EqRel A ∼ Part A := sorry

theorem EqRel_equinum_EqRelExt (A : Type) :
    EqRel A ∼ EqRelExt A := sorry

theorem EqRel_Nat_equinum_sub_PN :
    ∃ (D : Set (Set Nat)), D ⊆ 𝒫 (Univ Nat) ∧ EqRel Nat ∼ D := sorry

theorem saz_pair_part (X : Set Nat) : partition (saz_pair X) := sorry

theorem sub_EqRel_Nat_equinum_PN :
    ∃ (C : Set (BinRel Nat)), C ⊆ EqRel Nat ∧ C ∼ 𝒫 (Univ Nat) := sorry

theorem EqRel_Nat_equinum_PN : EqRel Nat ∼ 𝒫 (Univ Nat) := sorry

---

1. The axiom of choice was first stated by Ernst Zermelo in 1904. You can learn more about it in Gregory H. Moore, Zermelo’s Axiom of Choice: Its Origins, Development, and Influence, Dover Publications, 2013. See also https://en.wikipedia.org/wiki/Axiom_of_choice.