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

5  Functions

5.1. Functions

The first definition in Chapter 5 of HTPI says that if \(F \subseteq A \times B\), then \(F\) is called a function from \(A\) to \(B\) if for every \(a \in A\) there is exactly one \(b \in B\) such that \((a, b) \in F\). The notation \(F : A \to B\) means that \(F\) is a function from \(A\) to \(B\). If \(F\) is a function from \(A\) to \(B\) and \(a \in A\), then HTPI introduces the notation \(F(a)\) for the unique \(b \in B\) such that \((a, b) \in F\). Thus, if \(F : A \to B\), \(a \in A\), and \(b \in B\), then \(F(a) = b\) means the same thing as \((a, b) \in F\). We sometimes think of \(F\) as representing an operation that can be applied to an element \(a\) of \(A\) to produce a corresponding element \(F(a)\) of \(B\), and we call \(F(a)\) the value of \(F\) at \(a\), or the result of applying \(F\) to \(a\).

This might remind you of the situation we faced in Chapter 4. If \(R \subseteq A \times B\), \(a \in A\), and \(b \in B\), then Chapter 4 of HTPI uses the notation \(aRb\) to mean the same thing as \((a, b) \in R\). But in Lean, we found it necessary to change this notation. Instead of using HTPI’s notation \(aRb\), we introduced the notation R a b, which we use when R has type Rel A B, a has type A, and b has type B. (The notation (a, b) ∈ R, in contrast, can be used only when R has type Set (A × B).) If R has type Rel A B, then we think of R as representing some relationship that might hold between a and b, and R a b as the proposition saying that this relationship holds. And although R is not a set of ordered pairs, there is a corresponding set, extension R, of type Set (A × B), with the property that (a, b) ∈ extension R if and only if R a b.

We will take a similar approach to functions in this chapter. For any types A and B, we introduce a new type A → B. If f has type A → B, then we think of f as representing some operation that can be applied to an object of type A to produce a corresponding object of type B. We will say that f is a function from A to B, and A is the domain of f. If a has type A, then we write f a (with a space but no parentheses) for the result of applying the operation represented by f to the object a. Thus, if we have f : A → B and a : A, then f a has type B. As with relations, if f has type A → B, then f is not a set of ordered pairs. But there is a corresponding set of ordered pairs, which we will call the graph of f, whose elements are the ordered pairs (a, b) for which f a = b:

def graph {A B : Type} (f : A → B) : Set (A × B) :=
  {(a, b) : A × B | f a = b}

theorem graph_def {A B : Type} (f : A → B) (a : A) (b : B) :
    (a, b) ∈ graph f ↔ f a = b := by rfl

Every set of type Set (A × B) is the extension of some relation from A to B, but not every such set is the graph of a function from A to B. To be the graph of a function, it must have the property that was used to define functions in HTPI: each object of type A must be paired in the set with exactly one object of type B. Let’s give this property a name:

def is_func_graph {A B : Type} (F : Set (A × B)) : Prop :=
  ∀ (x : A), ∃! (y : B), (x, y) ∈ F

And now we can say that the sets of type Set (A × B) that are graphs of functions from A to B are precisely the ones that have the property is_func_graph:

theorem func_from_graph {A B : Type} (F : Set (A × B)) :
    (∃ (f : A → B), graph f = F) ↔ is_func_graph F

We will ask you to prove the left-to-right direction of this theorem in the exercises. The proof of the right-to-left direction in Lean is tricky; it requires an idea that we won’t introduce until Section 8.2. We’ll give the proof then, but we’ll go ahead and use the theorem in this chapter when we find it useful.

Section 5.1 of HTPI proves two theorems about functions. The first gives a convenient way of proving that two functions are equal (HTPI p. 232):

Suppose \(f\) and \(g\) are functions from \(A\) to \(B\). If \(\forall a \in A(f(a) = g(a))\), then \(f = g\).

The proof of this theorem in HTPI is based on the axiom of extensionality for sets. But in Lean, functions aren’t sets of ordered pairs, so this method of proof won’t work. Fortunately, Lean has a similar axiom of extensionality for functions. The axiom is called funext, and it proves Theorem 5.1.4.

theorem Theorem_5_1_4 {A B : Type} (f g : A → B) :
    (∀ (a : A), f a = g a) → f = g := funext

We saw previously that if we are trying to prove X = Y, where X and Y both have type Set U, then often the best first step is the tactic apply Set.ext, which converts the goal to ∀ (x : U), x ∈ X ↔︎ x ∈ Y. Similarly, if we are trying to prove f = g, where f and g both have type A → B, then we will usually start with the tactic apply funext, which will convert the goal to ∀ (x : A), f x = g x. By Theorem_5_1_4, this implies the original goal f = g. For example, here is a proof that if two functions have the same graph, then they are equal:

example {A B : Type} (f g : A → B) :
    graph f = graph g → f = g := by
  assume h1 : graph f = graph g  --Goal : f = g
  apply funext                   --Goal : ∀ (x : A), f x = g x
  fix x : A
  have h2 : (x, f x) ∈ graph f := by
    define                       --Goal : f x = f x
    rfl
    done
  rewrite [h1] at h2             --h2 : (x, f x) ∈ graph g
  define at h2                   --h2 : g x = f x
  show f x = g x from h2.symm
  done

The axiom of extensionality for sets says that a set is completely determined by its elements. This is what justifies our usual method of defining a set: we specify what its elements are, using notation like {0, 1, 2} or {x : Nat | x < 3}. Similarly, the axiom of extensionality for functions says that a function is completely determined by its values, and therefore we can define a function by specifying its values. For instance, we can define a function from Nat to Nat by specifying, for any n : Nat, the result of applying the function to n. As an example of this, we could define the “squaring function” from Nat to Nat to be the function that, when applied to any n : Nat, produces the result n ^ 2. Here are two ways to define this function in Lean:

def square1 (n : Nat) : Nat := n ^ 2

def square2 : Nat → Nat := fun (n : Nat) => n ^ 2

The first of these definitions uses notation we have used before; it says that if n has type Nat, then the expression square1 n also has type Nat, and it is definitionally equal to n ^ 2. The second definition introduces new Lean notation. It says that square2 has type Nat → Nat, and it defines it to be the function that, when applied to any n of type Nat, yields the result n ^ 2. Of course, this also means that square2 n is definitionally equal to n ^ 2. In general, the notation fun (x : A) => ... means “the function which, when applied to any x of type A, yields the result …” The two definitions above are equivalent. You can ask Lean to confirm this, and try out the squaring function, as follows (the #eval command asks Lean to evaluate an expression):

example : square1 = square2 := by rfl

++#eval:: square1 7     --Answer: 49

There is one more theorem in Section 5.1 of HTPI. Theorem 5.1.5 says that if \(f\) is a function from \(A\) to \(B\) and \(g\) is a function from \(B\) to \(C\), then the composition of \(g\) and \(f\) is a function from \(A\) to \(C\). To state this theorem in Lean, we will have to make adjustments for the differences between the treatment of functions in HTPI and Lean. In Chapter 4, we defined comp S R to be the composition of S and R, where R has type Set (A × B) and S had type Set (B × C). But functions in Lean are not sets of ordered pairs, so we cannot apply the operation comp to them. We can, however, apply it to their graphs. So the theorem corresponding to Theorem 5.1.5 in HTPI is this:

theorem Theorem_5_1_5 {A B C : Type} (f : A → B) (g : B → C) :
    ∃ (h : A → C), graph h = comp (graph g) (graph f) := by
  set h : A → C := fun (x : A) => g (f x)
  apply Exists.intro h
  apply Set.ext
  fix (a, c) : A × C
  apply Iff.intro
  · -- Proof that (a, c) ∈ graph h → (a, c) ∈ comp (graph g) (graph f)
    assume h1 : (a, c) ∈ graph h
    define at h1  --h1 : h a = c
    define        --Goal : ∃ (x : B), (a, x) ∈ graph f ∧ (x, c) ∈ graph g
    apply Exists.intro (f a)
    apply And.intro
    · -- Proof that (a, f a) ∈ graph f
      define
      rfl
      done
    · -- Proof that (f a, c) ∈ graph g
      define
      show g (f a) = c from h1
      done
    done
  · -- Proof that (a, c) ∈ comp (graph g) (graph f) → (a, c) ∈ graph h
    assume h1 : (a, c) ∈ comp (graph g) (graph f)
    define        --Goal : h a = c
    define at h1  --h1 : ∃ (x : B), (a, x) ∈ graph f ∧ (x, c) ∈ graph g
    obtain (b : B) (h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g) from h1
    have h3 : (a, b) ∈ graph f := h2.left
    have h4 : (b, c) ∈ graph g := h2.right
    define at h3          --h3 : f a = b
    define at h4          --h4 : g b = c
    rewrite [←h3] at h4   --h4 : g (f a) = c
    show h a = c from h4
    done
  done

Notice that the proof of Theorem_5_1_5 begins by defining the function h for which graph h = comp (graph g) (graph f). The definition says that for all x of type A, h x = g (f x). This function h is called the composition of g and f, and it is denoted g ∘ f. (To type ∘ in VS Code, type \comp or \circ.) In other words, g ∘ f has type A → C, and for all x of type A, (g ∘ f) x is definitionally equal to g (f x). In HTPI, functions are sets of ordered pairs, and the operation of composition of functions is literally the same as the operation comp that we used in Chapter 4. But in Lean, we distinguish among functions, relations, and sets of ordered pairs, so all we can say is that the operation of composition of functions corresponds to the operation comp from Chapter 4. The correspondence is that, as shown in the proof of Theorem_5_1_5, if h = g ∘ f, then graph h = comp (graph g) (graph f).

We saw in part 4 of Theorem 4.2.5 that composition of relations is associative. Composition of functions is also associative. In fact, if f : A → B, g : B → C, and h : C → D, then h ∘ (g ∘ f) and (h ∘ g) ∘ f are definitionally equal, since they both mean the same thing as fun (x : A) => h (g (f a)). As a result, the tactic rfl proves the associativity of composition of functions:

example {A B C D : Type} (f : A → B) (g : B → C) (h : C → D) :
    h ∘ (g ∘ f) = (h ∘ g) ∘ f := by rfl

HTPI defines the identity function on a set \(A\) to be the function \(i_A\) from \(A\) to \(A\) such that \(\forall x \in A(i_A(x) = x)\), and Exercise 9 from Section 4.3 of HTPI implies that if \(f : A \to B\), then \(f \circ i_A = f\) and \(i_B \circ f = f\). We say, therefore, that the identity functions are identity elements for composition of functions. Similarly, in Lean, for each type A there is an identity function from A to A. This identity function is denoted id; there is no need to specify A in the notation, because A is an implicit argument to id. Thus, when you use id to denote an identity function, Lean will figure out what type A to use as the domain of the function. (If, for some reason, you want to specify that the domain is some type A, you can write @id A instead of id.) For any x, of any type, id x is definitionally equal to x, and as a result the proof that id is an identity element for composition of functions can also be done with the rfl tactic:

example {A B : Type} (f : A → B) : f ∘ id = f := by rfl

example {A B : Type} (f : A → B) : id ∘ f = f := by rfl

Exercises

theorem func_from_graph_ltr {A B : Type} (F : Set (A × B)) :
    (∃ (f : A → B), graph f = F) → is_func_graph F := sorry

theorem Exercise_5_1_13a
    {A B C : Type} (R : Set (A × B)) (S : Set (B × C)) (f : A → C)
    (h1 : ∀ (b : B), b ∈ Ran R ∧ b ∈ Dom S) (h2 : graph f = comp S R) :
    is_func_graph S := sorry

theorem Exercise_5_1_14a
    {A B : Type} (f : A → B) (R : BinRel A) (S : BinRel B)
    (h : ∀ (x y : A), R x y ↔ S (f x) (f y)) :
    reflexive S → reflexive R := sorry

4. Here is a putative theorem:

Suppose \(f : A \to B\), \(R\) is a binary relation on \(A\), and \(S\) is the binary relation on \(B\) defined as follows: \[ \forall x \in B \forall y \in B(xSy \leftrightarrow \exists u \in A\exists v \in A(f(u) = x \wedge f(v) = y \wedge uRv)). \] If \(R\) is reflexive then \(S\) is reflexive.

Is the theorem correct? Try to prove it in Lean. If you can’t prove it, see if you can find a counterexample.

--You might not be able to complete this proof
theorem Exercise_5_1_15a
    {A B : Type} (f : A → B) (R : BinRel A) (S : BinRel B)
    (h : ∀ (x y : B), S x y ↔ ∃ (u v : A), f u = x ∧ f v = y ∧ R u v) :
    reflexive R → reflexive S := sorry

5. Here is a putative theorem with an incorrect proof:

Suppose \(f : A \to B\), \(R\) is a binary relation on \(A\), and \(S\) is the binary relation on \(B\) defined as follows: \[ \forall x \in B \forall y \in B(xSy \leftrightarrow \exists u \in A\exists v \in A(f(u) = x \wedge f(v) = y \wedge uRv)). \] If \(R\) is transitive then \(S\) is transitive.

Suppose \(R\) is transitive. Let \(x\), \(y\), and \(z\) be arbitrary elements of \(B\). Assume that \(xSy\) and \(ySz\). By the definition of \(S\), this means that there are \(u\), \(v\), and \(w\) in \(A\) such that \(f(u) = x\), \(f(v) = y\), \(f(w) = z\), \(uRv\), and \(vRw\). Since \(R\) is transitive, it follows that \(uRw\). Since \(f(u) = x\), \(f(w) = z\), and \(uRw\), \(xSz\). Therefore \(S\) is transitive.  □

Find the mistake in the proof by attempting to write the proof in Lean. Is the theorem correct?

--You might not be able to complete this proof
theorem Exercise_5_1_15c
    {A B : Type} (f : A → B) (R : BinRel A) (S : BinRel B)
    (h : ∀ (x y : B), S x y ↔ ∃ (u v : A), f u = x ∧ f v = y ∧ R u v) :
    transitive R → transitive S := sorry

theorem Exercise_5_1_16b
    {A B : Type} (R : BinRel B) (S : BinRel (A → B))
    (h : ∀ (f g : A → B), S f g ↔ ∀ (x : A), R (f x) (g x)) :
    symmetric R → symmetric S := sorry

theorem Exercise_5_1_17a {A : Type} (f : A → A) (a : A)
    (h : ∀ (x : A), f x = a) : ∀ (g : A → A), f ∘ g = f := sorry

theorem Exercise_5_1_17b {A : Type} (f : A → A) (a : A)
    (h : ∀ (g : A → A), f ∘ g = f) :
    ∃ (y : A), ∀ (x : A), f x = y := sorry

5.2. One-to-One and Onto

Section 5.2 of HTPI introduces two important properties that a function might have. A function f : A → B is called onto if for every b of type B there is at least one a of type A such that f a = b:

def onto {A B : Type} (f : A → B) : Prop :=
  ∀ (y : B), ∃ (x : A), f x = y

It is called one-to-one if there do not exist distinct a1 and a2 of type A such that f a1 = f a2. This phrasing of the definition makes it clear what is at issue: Are there distinct objects in the domain to which the function assigns the same value? But it is a negative statement, and that would make it difficult to work with it in proofs. Fortunately, it is not hard to rephrase the definition as an equivalent positive statement, using quantifier negation, De Morgan, and conditional laws. The resulting equivalent positive statement is given in Theorem 5.2.3 of HTPI, and we take it as our official definition of one_to_one in Lean:

def one_to_one {A B : Type} (f : A → B) : Prop :=
  ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2

There is only one more theorem about these properties in Section 5.2 of HTPI. It says that a composition of one-to-one functions is one-to-one, and a composition of onto functions is onto. It is straightforward to carry out these proofs in Lean by simply applying the definitions of the relevant concepts.

theorem Theorem_5_2_5_1 {A B C : Type} (f : A → B) (g : B → C) :
    one_to_one f → one_to_one g → one_to_one (g ∘ f) := by
  assume h1 : one_to_one f
  assume h2 : one_to_one g
  define at h1  --h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
  define at h2  --h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
  define        --Goal : ∀ (x1 x2 : A), (g ∘ f) x1 = (g ∘ f) x2 → x1 = x2
  fix a1 : A
  fix a2 : A    --Goal : (g ∘ f) a1 = (g ∘ f) a2 → a1 = a2
  define : (g ∘ f) a1; define : (g ∘ f) a2
                --Goal : g (f a1) = g (f a2) → a1 = a2
  assume h3 : g (f a1) = g (f a2)
  have h4 : f a1 = f a2 := h2 (f a1) (f a2) h3
  show a1 = a2 from h1 a1 a2 h4
  done

Notice that the tactic define : (g ∘ f) a1 replaces (g ∘ f) a1 with its definition, g (f a1). As usual, this step isn’t really needed—Lean will apply the definition on its own when necessary, without being told. But using this tactic makes the proof easier to read. Also, notice that define : g ∘ f produces a result that is much less useful. As we have observed before, the define tactic works best when applied to a complete expression, rather than just a part of an expression.

An alternative way to apply the definition of composition of functions is to prove a lemma that can be used in the rewrite tactic. We try out this approach for the second part of the theorem.

lemma comp_def {A B C : Type} (f : A → B) (g : B → C) (x : A) :
    (g ∘ f) x = g (f x) := by rfl

theorem Theorem_5_2_5_2 {A B C : Type} (f : A → B) (g : B → C) :
    onto f → onto g → onto (g ∘ f) := by
  assume h1 : onto f
  assume h2 : onto g
  define at h1           --h1 : ∀ (y : B), ∃ (x : A), f x = y
  define at h2           --h2 : ∀ (y : C), ∃ (x : B), g x = y
  define                 --Goal : ∀ (y : C), ∃ (x : A), (g ∘ f) x = y
  fix c : C
  obtain (b : B) (h3 : g b = c) from h2 c
  obtain (a : A) (h4 : f a = b) from h1 b
  apply Exists.intro a   --Goal : (g ∘ f) a = c
  rewrite [comp_def]     --Goal : g (f a) = c
  rewrite [←h4] at h3
  show g (f a) = c from h3
  done

Exercises

theorem Exercise_5_2_10a {A B C : Type} (f: A → B) (g : B → C) :
    onto (g ∘ f) → onto g := sorry

theorem Exercise_5_2_10b {A B C : Type} (f: A → B) (g : B → C) :
    one_to_one (g ∘ f) → one_to_one f := sorry

theorem Exercise_5_2_11a {A B C : Type} (f: A → B) (g : B → C) :
    onto f → ¬(one_to_one g) → ¬(one_to_one (g ∘ f)) := sorry

theorem Exercise_5_2_11b {A B C : Type} (f: A → B) (g : B → C) :
    ¬(onto f) → one_to_one g → ¬(onto (g ∘ f)) := sorry

theorem Exercise_5_2_12 {A B : Type} (f : A → B) (g : B → Set A)
    (h : ∀ (b : B), g b = {a : A | f a = b}) :
    onto f → one_to_one g := sorry

theorem Exercise_5_2_16 {A B C : Type}
    (R : Set (A × B)) (S : Set (B × C)) (f : A → C) (g : B → C)
    (h1 : graph f = comp S R) (h2 : graph g = S) (h3 : one_to_one g) :
    is_func_graph R := sorry

theorem Exercise_5_2_17a
    {A B : Type} (f : A → B) (R : BinRel A) (S : BinRel B)
    (h1 : ∀ (x y : B), S x y ↔ ∃ (u v : A), f u = x ∧ f v = y ∧ R u v)
    (h2 : onto f) : reflexive R → reflexive S := sorry

theorem Exercise_5_2_17b
    {A B : Type} (f : A → B) (R : BinRel A) (S : BinRel B)
    (h1 : ∀ (x y : B), S x y ↔ ∃ (u v : A), f u = x ∧ f v = y ∧ R u v)
    (h2 : one_to_one f) : transitive R → transitive S := sorry

theorem Exercise_5_2_21a {A B C : Type} (f : B → C) (g h : A → B)
    (h1 : one_to_one f) (h2 : f ∘ g = f ∘ h) : g = h := sorry

theorem Exercise_5_2_21b {A B C : Type} (f : B → C) (a : A)
    (h1 : ∀ (g h : A → B), f ∘ g = f ∘ h → g = h) :
    one_to_one f := sorry

5.3. Inverses of Functions

Section 5.3 of HTPI is motivated by the following question: If \(f\) is a function from \(A\) to \(B\), is \(f^{-1}\) a function from \(B\) to \(A\)? Here is the first theorem in that section (HTPI p. 250):

Suppose \(f : A \to B\). If \(f\) is one-to-one and onto, then \(f^{-1} : B \to A\).

Of course, we will have to rephrase this theorem slightly to prove it in Lean. If f has type A → B, then the inverse operation inv cannot be applied to f, but it can be applied to graph f. So we must rephrase the theorem like this:

theorem Theorem_5_3_1 {A B : Type}
    (f : A → B) (h1 : one_to_one f) (h2 : onto f) :
    ∃ (g : B → A), graph g = inv (graph f)

To prove this theorem, we will use the theorem func_from_graph that was stated in Section 5.1. We can remind ourselves of what that theorem says by using the command #check @func_from_graph, which gives the result:

@func_from_graph : ∀ {A B : Type} (F : Set (A × B)),
                    (∃ (f : A → B), graph f = F) ↔ is_func_graph F

This means that, in the context of the proof of Theorem_5_3_1, func_from_graph (inv (graph f)) is a proof of the statement

∃ (g : B → A), graph g = inv (graph f) ↔ is_func_graph (inv (graph f)).

Therefore the tactic rewrite [func_from_graph (inv (graph f))] will change the goal to is_func_graph (inv (func f)). In fact, we can just use rewrite [func_from_graph], and Lean will figure out how to apply the theorem to rewrite the goal. The rest of the proof is straightforward.

theorem Theorem_5_3_1 {A B : Type}
    (f : A → B) (h1 : one_to_one f) (h2 : onto f) :
    ∃ (g : B → A), graph g = inv (graph f) := by
  rewrite [func_from_graph]   --Goal : is_func_graph (inv (graph f))
  define        --Goal : ∀ (x : B), ∃! (y : A), (x, y) ∈ inv (graph f)
  fix b : B
  exists_unique
  · -- Existence
    define at h2          --h2 : ∀ (y : B), ∃ (x : A), f x = y
    obtain (a : A) (h4 : f a = b) from h2 b
    apply Exists.intro a  --Goal : (b, a) ∈ inv (graph f)
    define                --Goal : f a = b
    show f a = b from h4
    done
  · -- Uniqueness
    fix a1 : A; fix a2 : A
    assume h3 : (b, a1) ∈ inv (graph f)
    assume h4 : (b, a2) ∈ inv (graph f) --Goal : a1 = a2
    define at h3          --h3 : f a1 = b
    define at h4          --h4 : f a2 = b
    rewrite [←h4] at h3   --h3 : f a1 = f a2
    define at h1          --h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
    show a1 = a2 from h1 a1 a2 h3
    done
  done

Suppose, now, that we have f : A → B, g : B → A, and graph g = inv (graph f), as in Theorem_5_3_1. What can we say about the relationship between f and g? One answer is that g ∘ f = id and f ∘ g = id, as shown in Theorem 5.3.2 of HTPI. We’ll prove one of these facts, and leave the other as an exercise for you.

theorem Theorem_5_3_2_1 {A B : Type} (f : A → B) (g : B → A)
    (h1 : graph g = inv (graph f)) : g ∘ f = id := by
  apply funext           --Goal : ∀ (x : A), (g ∘ f) x = id x
  fix a : A              --Goal : (g ∘ f) a = id a
  have h2 : (f a, a) ∈ graph g := by
    rewrite [h1]         --Goal : (f a, a) ∈ inv (graph f)
    define               --Goal : f a = f a
    rfl
    done
  define at h2           --h2 : g (f a) = a
  show (g ∘ f) a = id a from h2
  done

theorem Theorem_5_3_2_2 {A B : Type} (f : A → B) (g : B → A)
    (h1 : graph g = inv (graph f)) : f ∘ g = id := sorry

Combining the theorems above, we have shown that if f is one-to-one and onto, then there is a function g such that g ∘ f = id and f ∘ g = id. In fact, the converse is true as well: if such a function g exists, then f must be one-to-one and onto. Again, we’ll prove one statement and leave the second as an exercise.

theorem Theorem_5_3_3_1 {A B : Type} (f : A → B) (g : B → A)
    (h1 : g ∘ f = id) : one_to_one f := by
  define              --Goal : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
  fix a1 : A; fix a2 : A
  assume h2 : f a1 = f a2
  show a1 = a2 from
    calc a1
      _ = id a1 := by rfl
      _ = (g ∘ f) a1 := by rw [h1]
      _ = g (f a1) := by rfl
      _ = g (f a2) := by rw [h2]
      _ = (g ∘ f) a2 := by rfl
      _ = id a2 := by rw [h1]
      _ = a2 := by rfl
  done

theorem Theorem_5_3_3_2 {A B : Type} (f : A → B) (g : B → A)
    (h1 : f ∘ g = id) : onto f := sorry

We can combine the theorems above to show that if we have f : A → B, g : B → A, g ∘ f = id, and f ∘ g = id, then graph g must be the inverse of graph f. Compare the proof below to the proof of Theorem 5.3.5 in HTPI.

theorem Theorem_5_3_5 {A B : Type} (f : A → B) (g : B → A)
    (h1 : g ∘ f = id) (h2 : f ∘ g = id) : graph g = inv (graph f) := by
  have h3 : one_to_one f := Theorem_5_3_3_1 f g h1
  have h4 : onto f := Theorem_5_3_3_2 f g h2
  obtain (g' : B → A) (h5 : graph g' = inv (graph f))
    from Theorem_5_3_1 f h3 h4
  have h6 : g' ∘ f = id := Theorem_5_3_2_1 f g' h5
  have h7 : g = g' :=
    calc g
      _ = id ∘ g := by rfl
      _ = (g' ∘ f) ∘ g := by rw [h6]
      _ = g' ∘ (f ∘ g) := by rfl
      _ = g' ∘ id := by rw [h2]
      _ = g' := by rfl
  rewrite [←h7] at h5
  show graph g = inv (graph f) from h5
  done

Exercises

theorem Theorem_5_3_2_2 {A B : Type} (f : A → B) (g : B → A)
    (h1 : graph g = inv (graph f)) : f ∘ g = id := sorry

theorem Theorem_5_3_3_2 {A B : Type} (f : A → B) (g : B → A)
    (h1 : f ∘ g = id) : onto f := sorry

theorem Exercise_5_3_11a {A B : Type} (f : A → B) (g : B → A) :
    one_to_one f → f ∘ g = id → graph g = inv (graph f) := sorry

theorem Exercise_5_3_11b {A B : Type} (f : A → B) (g : B → A) :
    onto f → g ∘ f = id → graph g = inv (graph f) := sorry

theorem Exercise_5_3_14a {A B : Type} (f : A → B) (g : B → A)
    (h : f ∘ g = id) : ∀ x ∈ Ran (graph g), g (f x) = x := sorry

theorem Exercise_5_3_18 {A B C : Type} (f : A → C) (g : B → C)
    (h1 : one_to_one g) (h2 : onto g) :
    ∃ (h : A → B), g ∘ h = f := sorry

The next two exercises will use the following definition:

def conjugate (A : Type) (f1 f2 : A → A) : Prop :=
  ∃ (g g' : A → A), (f1 = g' ∘ f2 ∘ g) ∧ (g ∘ g' = id) ∧ (g' ∘ g = id)

theorem Exercise_5_3_17a {A : Type} : symmetric (conjugate A) := sorry

theorem Exercise_5_3_17b {A : Type} (f1 f2 : A → A)
    (h1 : conjugate A f1 f2) (h2 : ∃ (a : A), f1 a = a) :
    ∃ (a : A), f2 a = a := sorry

5.4. Closures

Suppose we have f : A → A and C : Set A. We say that C is closed under f if the value of f at any element of C is again an element of C:

def closed {A : Type} (f : A → A) (C : Set A) : Prop := ∀ x ∈ C, f x ∈ C

According to this definition, closed f C means that C is closed under f. Sometimes, if we have a set B of type Set A that is not closed under f, we are interested in adding more elements to the set to make it closed. The closure of B under f is the smallest set containing B that is closed under f. That is, it is the smallest element of {D : Set A | B ⊆ D ∧ closed f D}, where we use the subset partial ordering on Set A to determine which element is smallest. We will write closure f B C to mean that the closure of B under f is C. We can define this as follows:

def closure {A : Type} (f : A → A) (B C : Set A) : Prop :=
  smallestElt (sub A) C {D : Set A | B ⊆ D ∧ closed f D}

We know that smallest elements, when they exist, are unique, so it makes sense to talk about the closure of B under f. But not every set has a smallest element. Does every set have a closure? Theorem 5.4.5 in HTPI says that the answer is yes. The idea behind the proof is that, for any family of sets F, if F has a smallest element under the subset partial order, then that smallest element is equal to ⋂₀ F. (We’ll ask you to prove this in the exercises.)

theorem Theorem_5_4_5 {A : Type} (f : A → A) (B : Set A) :
    ∃ (C : Set A), closure f B C := by
  set F : Set (Set A) := {D : Set A | B ⊆ D ∧ closed f D}
  set C : Set A := ⋂₀ F
  apply Exists.intro C    --Goal : closure f B C
  define                  --Goal : C ∈ F ∧ ∀ x ∈ F, C ⊆ x
  apply And.intro
  · -- Proof that C ∈ F
    define                  --Goal : B ⊆ C ∧ closed f C
    apply And.intro
    · -- Proof that B ⊆ C
      fix a : A
      assume h1 : a ∈ B       --Goal : a ∈ C
      define                  --Goal : ∀ t ∈ F, a ∈ t
      fix D : Set A
      assume h2 : D ∈ F
      define at h2            --h2 : B ⊆ D ∧ closed f D
      show a ∈ D from h2.left h1
      done
    · -- Proof that C is closed under f
      define                  --Goal : ∀ x ∈ C, f x ∈ C
      fix a : A
      assume h1 : a ∈ C       --Goal : f a ∈ C
      define                  --Goal : ∀ t ∈ F, f a ∈ t
      fix D : Set A
      assume h2 : D ∈ F       --Goal : f a ∈ D
      define at h1            --h1 : ∀ t ∈ F, a ∈ t
      have h3 : a ∈ D := h1 D h2
      define at h2            --h2 : B ⊆ D ∧ closed f D
      have h4 : closed f D := h2.right
      define at h4            --h4 : ∀ x ∈ D, f x ∈ D
      show f a ∈ D from h4 a h3
      done
    done
  · -- Proof that C is smallest
    fix D : Set A
    assume h1 : D ∈ F      --Goal : sub A C D
    define
    fix a : A
    assume h2 : a ∈ C       --Goal : a ∈ D
    define at h2            --h2 : ∀ t ∈ F, a ∈ t
    show a ∈ D from h2 D h1
    done
  done

The idea of the closure of a set under a function can also be applied to functions of two variables. One way to represent a function of two variables on a type A would be to use a function g of type (A × A) → A. If a and b have type A, then (a, b) has type A × A, and the result of applying the function g to the pair of values a and b would be written g (a, b).

However, there is another way to represent a function of two variables that turns out to be more convenient in Lean. Suppose f has type A → A → A. As with the arrow used in conditional propositions, the arrow for function types groups to the right, so A → A → A means A → (A → A). Thus, if a has type A, then f a has type A → A. In other words, f a is a function from A to A, and therefore if b has type A then f a b has type A. The upshot is that if f is followed by two objects of type A, then the resulting expression has type A, so f can be thought of as a function that applies to a pair of objects of type A and gives a value of type A.

For example, we can think of addition of integers as a function of two variables. Here are three ways to define this function in Lean.

def plus (m n : Int) : Int := m + n

def plus' : Int → Int → Int := fun (m n : Int) => m + n

def plus'' : Int → Int → Int := fun (m : Int) => (fun (n : Int) => m + n)

The third definition matches the description above most closely: plus'' is a function that, when applied to an integer m, produces a new function plus'' m : Int → Int. The function plus'' m is defined to be the function that, when applied to an integer n, produces the value m + n. In other words, plus'' m n = m + n. The first two definitions are more convenient ways of defining exactly the same function. Let’s have Lean confirm this, and try out the function:

example : plus = plus'' := by rfl

example : plus' = plus'' := by rfl

++#eval:: plus 3 2     --Answer: 5

There are two reasons why this way of representing functions of two variables in Lean is more convenient. First, it saves us the trouble of grouping the arguments of the function together into an ordered pair before applying the function. If we have f : A → A → A and a b : A, then to apply the function f to the arguments a and b we can just write f a b. Second, it allows for the possibility of “partially applying” the function f. The expression f a is meaningful, and denotes the function that, when applied to any b : A, produces the result f a b. For example, if m is an integer, then plus m denotes the function that, when applied to an integer n, produces the result m + n. We might call plus m the “add to m” function.

We have actually been using these ideas for a long time. In Chapter 3, we introduced the type Pred U of predicates applying to objects of type U, but we did not explain how such predicates are represented internally in Lean. In fact, Pred U is defined to be the type U → Prop, so if P has type Pred U, then P is a function from U to Prop, and if x has type U, then the proposition P x is the result of applying the function P to x. Similarly, Rel A B stands for A → B → Prop, so if R has type Rel A B, then R is a function of two variables, one of type A and one of type B. Earlier in this section, we defined closed f C to be the proposition asserting that C is closed under f. This means that closed is a function of two variables, the first a function f of type A → A and the second a set C of type Set A (where the type A is an implicit argument of closed). But that means that the partial application closed f denotes a function from Set A to Prop. In other words, closed f is a predicate applying to sets of type Set A; we could think of it as the “is closed under f” predicate. Similarly, in Section 4.4 we defined sub to be a function of three variables: if A is a type and X and Y have type Set A, then sub A X Y is the proposition X ⊆ Y. Since then, we have used the partial application sub A, which is the subset relation on Set A. For example, we used it earlier in this section in the definition of closure.

Returning to the subject of closures, here’s how we can extend the idea of closures to functions of two variables:

def closed2 {A : Type} (f : A → A → A) (C : Set A) : Prop :=
  ∀ x ∈ C, ∀ y ∈ C, f x y ∈ C

def closure2 {A : Type} (f : A → A → A) (B C : Set A) : Prop := 
  smallestElt (sub A) C {D : Set A | B ⊆ D ∧ closed2 f D}

We will leave it as an exercise for you to prove that closures under functions of two variables also exist.

theorem Theorem_5_4_9 {A : Type} (f : A → A → A) (B : Set A) :
    ∃ (C : Set A), closure2 f B C := sorry

Exercises

example {A : Type} (F : Set (Set A)) (B : Set A) :
    smallestElt (sub A) B F → B = ⋂₀ F := sorry

2. If B has type Set A, then complement B is the set {a : A | a ∉ B}. Thus, for any a of type A, a ∈ complement B if and only if a ∉ B:

def complement {A : Type} (B : Set A) : Set A := {a : A | a ∉ B}

Use this definition to prove the following theorem:

theorem Exercise_5_4_7 {A : Type} (f g : A → A) (C : Set A)
    (h1 : f ∘ g = id) (h2 : closed f C) : closed g (complement C) := sorry

theorem Exercise_5_4_9a {A : Type} (f : A → A) (C1 C2 : Set A)
    (h1 : closed f C1) (h2 : closed f C2) : closed f (C1 ∪ C2) := sorry

theorem Exercise_5_4_10a {A : Type} (f : A → A) (B1 B2 C1 C2 : Set A)
    (h1 : closure f B1 C1) (h2 : closure f B2 C2) :
    B1 ⊆ B2 → C1 ⊆ C2 := sorry

theorem Exercise_5_4_10b {A : Type} (f : A → A) (B1 B2 C1 C2 : Set A)
    (h1 : closure f B1 C1) (h2 : closure f B2 C2) :
    closure f (B1 ∪ B2) (C1 ∪ C2) := sorry

theorem Theorem_5_4_9 {A : Type} (f : A → A → A) (B : Set A) :
    ∃ (C : Set A), closure2 f B C := sorry

7. Suppose we define a set to be closed under a family of functions if it is closed under all of the functions in the family. Of course, the closure of a set B under a family of functions is the smallest set containing B that is closed under the family.

def closed_family {A : Type} (F : Set (A → A)) (C : Set A) : Prop :=
  ∀ f ∈ F, closed f C

def closure_family {A : Type} (F : Set (A → A)) (B C : Set A) : Prop :=
  smallestElt (sub A) C {D : Set A | B ⊆ D ∧ closed_family F D}

Prove that the closure of a set under a family of functions always exists:

theorem Exercise_5_4_13a {A : Type} (F : Set (A → A)) (B : Set A) :
    ∃ (C : Set A), closure_family F B C := sorry

5.5. Images and Inverse Images: A Research Project

Section 5.5 of HTPI introduces two new definitions (HTPI p. 268). Suppose \(f : A \to B\). If \(X \subseteq A\), then the image of \(X\) under \(f\) is the set \(f(X)\) defined as follows: \[ f(X) = \{f(x) \mid x \in X\} = \{b \in B \mid \exists x \in X(f(x) = b)\}. \] If \(Y \subseteq B\), then the inverse image of \(Y\) under \(f\) is the set \(f^{-1}(Y)\) defined as follows: \[ f^{-1}(Y) = \{a \in A \mid f(a) \in Y\}. \]

Here are definitions of these concepts in Lean:

def image {A B : Type} (f : A → B) (X : Set A) : Set B :=
  {f x | x ∈ X}

def inverse_image {A B : Type} (f : A → B) (Y : Set B) : Set A :=
  {a : A | f a ∈ Y}

--The following theorems illustrate the meaning of these definitions:
theorem image_def {A B : Type} (f : A → B) (X : Set A) (b : B) :
    b ∈ image f X ↔ ∃ x ∈ X, f x = b := by rfl

theorem inverse_image_def {A B : Type} (f : A → B) (Y : Set B) (a : A) :
    a ∈ inverse_image f Y ↔ f a ∈ Y := by rfl

It is natural to wonder how these concepts interact with familiar operations on sets. HTPI gives an example of such an interaction in Theorem 5.5.2. The theorem makes two assertions. Here are proofs of the two parts of the theorem in Lean.

theorem Theorem_5_5_2_1 {A B : Type} (f : A → B) (W X : Set A) :
    image f (W ∩ X) ⊆ image f W ∩ image f X := by
  fix y : B
  assume h1 : y ∈ image f (W ∩ X)  --Goal : y ∈ image f W ∩ image f X
  define at h1                     --h1 : ∃ x ∈ W ∩ X, f x = y
  obtain (x : A) (h2 : x ∈ W ∩ X ∧ f x = y) from h1
  define : x ∈ W ∩ X at h2         --h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
  apply And.intro
  · -- Proof that y ∈ image f W
    define                         --Goal : ∃ x ∈ W, f x = y
    show ∃ (x : A), x ∈ W ∧ f x = y from
      Exists.intro x (And.intro h2.left.left h2.right)
    done
  · -- Proof that y ∈ image f X
    show y ∈ image f X from
      Exists.intro x (And.intro h2.left.right h2.right)
    done
  done

theorem Theorem_5_5_2_2 {A B : Type} (f : A → B) (W X : Set A)
    (h1 : one_to_one f) : image f (W ∩ X) = image f W ∩ image f X := by
  apply Set.ext
  fix y : B      --Goal : y ∈ image f (W ∩ X) ↔ y ∈ image f W ∩ image f X
  apply Iff.intro
  · -- (→)
    assume h2 : y ∈ image f (W ∩ X)
    show y ∈ image f W ∩ image f X from Theorem_5_5_2_1 f W X h2
    done
  · -- (←)
    assume h2 : y ∈ image f W ∩ image f X  --Goal : y ∈ image f (W ∩ X)
    define at h2                  --h2 : y ∈ image f W ∧ y ∈ image f X
    rewrite [image_def, image_def] at h2
          --h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
    obtain (x1 : A) (h3 : x1 ∈ W ∧ f x1 = y) from h2.left
    obtain (x2 : A) (h4 : x2 ∈ X ∧ f x2 = y) from h2.right
    have h5 : f x2 = y := h4.right
    rewrite [←h3.right] at h5  --h5 : f x2 = f x1
    define at h1               --h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
    have h6 : x2 = x1 := h1 x2 x1 h5
    rewrite [h6] at h4           --h4 : x1 ∈ X ∧ f x1 = y
    show y ∈ image f (W ∩ X) from
      Exists.intro x1 (And.intro (And.intro h3.left h4.left) h3.right)
    done
  done

The rest of Section 5.5 of HTPI consists of statements for you to try to prove. Here are the statements, written as examples in Lean. Some are correct and some are not; some can be made correct by adding additional hypotheses or weakening the conclusion. Prove as much as you can.

--Warning!  Not all of these examples are correct!

example {A B : Type} (f : A → B) (W X : Set A) :
    image f (W ∪ X) = image f W ∪ image f X := sorry

example {A B : Type} (f : A → B) (W X : Set A) :
    image f (W \ X) = image f W \ image f X := sorry

example {A B : Type} (f : A → B) (W X : Set A) :
    W ⊆ X ↔ image f W ⊆ image f X := sorry

example {A B : Type} (f : A → B) (Y Z : Set B) :
    inverse_image f  (Y ∩ Z) =
        inverse_image f Y ∩ inverse_image f Z := sorry

example {A B : Type} (f : A → B) (Y Z : Set B) :
    inverse_image f  (Y ∪ Z) =
        inverse_image f Y ∪ inverse_image f Z := sorry

example {A B : Type} (f : A → B) (Y Z : Set B) :
    inverse_image f  (Y \ Z) =
        inverse_image f Y \ inverse_image f Z := sorry

example {A B : Type} (f : A → B) (Y Z : Set B) :
    Y ⊆ Z ↔ inverse_image f Y ⊆ inverse_image f Z := sorry

example {A B : Type} (f : A → B) (X : Set A) :
    inverse_image f (image f X) = X := sorry

example {A B : Type} (f : A → B) (Y : Set B) :
    image f (inverse_image f Y) = Y := sorry

example {A : Type} (f : A → A) (C : Set A) :
    closed f C → image f C ⊆ C := sorry

example {A : Type} (f : A → A) (C : Set A) :
    image f C ⊆ C → C ⊆ inverse_image f C := sorry

example {A : Type} (f : A → A) (C : Set A) :
    C ⊆ inverse_image f C → closed f C := sorry

example {A B : Type} (f : A → B) (g : B → A) (Y : Set B)
    (h1 : f ∘ g = id) (h2 : g ∘ f = id) :
    inverse_image f Y = image g Y := sorry