Chap5.qmd

# 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`:

```lean
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:

```lean
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`:

```lean
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):

::: {.nthm arguments="Theorem 5.1.4"}
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.

```lean
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:

```lean
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:

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

```lean
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:

```lean
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:

```lean
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:

```lean
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

::: {.numex arguments="1"}
```lean
theorem func_from_graph_ltr {A B : Type} (F : Set (A × B)) :
    (∃ (f : A → B), graph f = F) → is_func_graph F := sorry
```
:::

::: {.numex arguments="2"}
```lean
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
```
:::

::: {.numex arguments="3"}
```lean
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:

::: {.nthm arguments="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.

```lean
--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:

::: {.nthm arguments="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 transitive then $S$ is transitive.
:::

::: {.npf arguments="Incorrect Proof"}
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. [&nbsp;□]{.excl}\qedhere
:::

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

```lean
--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
```

::: {.numex arguments="6"}
```lean
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
```
:::

::: {.numex arguments="7"}
```lean
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
```
:::

::: {.numex arguments="8"}
```lean
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`:

```lean
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:

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

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

```lean
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

::: {.numex arguments="1"}
```lean
theorem Exercise_5_2_10a {A B C : Type} (f: A → B) (g : B → C) :
    onto (g ∘ f) → onto g := sorry
```
:::

::: {.numex arguments="2"}
```lean
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
```
:::

::: {.numex arguments="3"}
```lean
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
```
:::

::: {.numex arguments="4"}
```lean
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
```
:::

::: {.numex arguments="5"}
```lean
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
```
:::

::: {.numex arguments="6"}
```lean
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
```
:::

::: {.numex arguments="7"}
```lean
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
```
:::

::: {.numex arguments="8"}
```lean
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
```
:::

::: {.numex arguments="9"}
```lean
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
```
:::

::: {.numex arguments="10"}
```lean
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):

::: {.nthm arguments="Theorem 5.3.1"}
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:

```lean
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:

:::{.ind}
```
@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

::: {.ind}
```
∃ (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.

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

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

```lean
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*.

```lean
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

::: {.numex arguments="1"}
```lean
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
```
:::

::: {.numex arguments="2"}
```lean
theorem Theorem_5_3_3_2 {A B : Type} (f : A → B) (g : B → A)
    (h1 : f ∘ g = id) : onto f := sorry
```
:::

::: {.numex arguments="3"}
```lean
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
```
:::

::: {.numex arguments="4"}
```lean
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
```
:::

::: {.numex arguments="5"}
```lean
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
```
:::

::: {.numex arguments="6"}
```lean
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
```
:::

::: {.mdsk}
:::

The next two exercises will use the following definition:

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

::: {.numex arguments="7"}
```lean
theorem Exercise_5_3_17a {A : Type} : symmetric (conjugate A) := sorry
```
:::

::: {.numex arguments="8"}
```lean
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`:

```lean
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:

```lean
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.)

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

```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:

```lean
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:

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

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

### Exercises

::: {.numex arguments="1"}
```lean
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`:

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

Use this definition to prove the following theorem:

```lean
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
```

::: {.numex arguments="3"}
```lean
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
```
:::

::: {.numex arguments="4"}
```lean
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
```
:::

::: {.numex arguments="5"}
```lean
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
```
:::

::: {.numex arguments="6"}
```lean
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.

```lean
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:

```lean
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:

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

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

```lean
--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
```