8. 函数

到目前为止，本书研究的是数的性质（一个数是否为奇数、正数、素数；一个数是否能被另一个数整除）以及数上的运算（加法、最大公因子）。

在本章中，我们上升到更高的抽象层次，研究函数的性质以及函数上的运算。这些新性质包括：一个函数是否为单射、满射、双射；一个函数是否为另一个函数的逆；以及复合运算。

我们还把视野扩展到数值类型（\(\mathbb{N}\)、\(\mathbb{Z}\)、\(\mathbb{Q}\)、\(\mathbb{R}\)）之外；这些数值类型构成了本书前半部分的语境。现在我们开始处理更广泛的类型，包括函数类型、有限归纳类型和积类型。

8.1. 单射性与满射性

8.1.1. 例

我们以前已经研究过具体函数。例如，例 6.3.3 中的 Fibonacci 数列是从 \(\mathbb{N}\) 到 \(\mathbb{Z}\) 的函数：它输入一个自然数，例如 5，并输出一个整数，在这个例子中为 8（该数列第 5 项）。

def F : ℕ → ℤ
  | 0 => 1
  | 1 => 1
  | n + 2 => F (n + 1) + F n

#eval F 5 -- infoview displays `8`

函数的定义域是它取输入值所在的类型，陪域是它取输出值所在的类型。例如，Fibonacci 数列的定义域是 \(\mathbb{N}\)，陪域是 \(\mathbb{Z}\)。定义域为 \(\mathbb{N}\)、陪域为 \(\mathbb{Z}\) 的函数类型记为 \(\mathbb{N}\to \mathbb{Z}\)。Lean 会为我们确认 Fibonacci 数列 F 具有这个类型：

#check @F -- infoview displays `F : ℕ → ℤ`

定义函数的另一种方式是用闭公式。例如，“设 \(q:\mathbb{R}\to \mathbb{R}\) 为函数，定义为 \(q(x)=x+3\)。”在 Lean 中可以写成

def q (x : ℝ) : ℝ := x + 3

这个函数的定义域和陪域都是 \(\mathbb{R}\)；我在定义它时甚至明确说了要让 \(q\) 具有类型 \(\mathbb{R}\to \mathbb{R}\)。我们检查一下这确实是 Lean 对象的类型：

#check @q -- infoview displays `q : ℝ → ℝ`

第三种定义函数的方式是使用记号 \(\mapsto\)，适用于我们预计只用一次、而不想浪费一个名称的函数：例如可以说“从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x \mapsto x ^ 2\)”。下面是在 Lean 中的同一记号：

#check fun (x : ℝ) ↦ x ^ 2 -- infoview displays `fun x ↦ x ^ 2 : ℝ → ℝ`

8.1.2. 定义

既然我们已经有了表示“从 \(X\) 到 \(Y\) 的函数类型”的记号 \(X\to Y\)，就可以像以前给数引入性质（如“奇”“素”）一样，给函数引入性质。下面是第一个性质。

定义

函数 \(f : X \to Y\) 称为单射，如果对类型 \(X\) 的所有 \(x_1\) 和 \(x_2\)，若 \(f(x_1)=f(x_2)\)，则 \(x_1=x_2\)。

def Injective (f : X → Y) : Prop := ∀ {x1 x2 : X}, f x1 = f x2 → x1 = x2

8.1.3. 例

问题

证明例 8.1.1 中的函数 \(q:\mathbb{R}\to\mathbb{R}\) 是单射。

解答

设 \(x_1\) 和 \(x_2\) 为实数，并假设 \(q(x_1)=q(x_2)\)。那么 \(x_1+1=x_2+1\)，所以 \(x_1=x_2\)。

下面是在 Lean 中的这个解答。注意，在用命令 dsimp [Injective] 展开“单射”的定义之后，目标状态显示

⊢ ∀ ⦃x1 x2 : ℝ⦄, q x1 = q x2 → x1 = x2

这正是“单射”定义特化到当前问题后的形式。

example : Injective q := by
  dsimp [Injective]
  intro x1 x2 h
  dsimp [q] at h
  addarith [h]

8.1.4. 例

问题

证明从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x \mapsto x ^ 2\) 不是单射。

解答

我们必须证明存在实数 \(x_1\) 和 \(x_2\)，使得 \(x_1{}^2=x_2{}^2\) 且 \(x_1\ne x_2\)。确实，-1 和 1 具有这些性质。

该证明的第一句话是一次否定规范化：我展开“单射”的定义，并把它的否定重述为一个逻辑等价但更方便的形式。回忆在 Lean 中我们用策略 push_neg 做这件事。下面是使用策略 push_neg 后的目标状态：

⊢ ∃ x1 x2, x1 ^ 2 = x2 ^ 2 ∧ x1 ≠ x2

下面是完整的 Lean 证明。

example : ¬ Injective (fun x : ℝ ↦ x ^ 2) := by
  dsimp [Injective]
  push_neg
  use -1, 1
  constructor
  · numbers
  · numbers

8.1.5. 定义

定义

函数 \(f : X \to Y\) 称为满射，如果对类型 \(Y\) 的每个 \(y\)，存在类型 \(X\) 的 \(x\)，使得 \(f(x)=y\)。

def Surjective (f : X → Y) : Prop := ∀ y : Y, ∃ x : X, f x = y

8.1.6. 例

问题

考虑函数 \(s:\mathbb{Q}\to\mathbb{Q}\)，定义为 \(s(a)=3a+2\)。证明 \(s\) 是满射。

解答

设 \(y\) 为有理数。那么

\[\begin{split}s\left(\frac{y-2}{3}\right)&=3\left(\frac{y-2}{3}\right)+2\\ &=y.\end{split}\]

下面是在 Lean 中的解答。展开“满射”的定义之后，目标状态是

⊢ ∀ (y : ℚ), ∃ x, s x = y

这确认了我们需要证明什么，也解释了为什么上面的文字证明足够。

def s (a : ℚ) : ℚ := 3 * a + 2

example : Surjective s := by
  dsimp [Surjective]
  intro y
  use (y - 2) / 3
  calc s ((y - 2) / 3) = 3 * ((y - 2) / 3) + 2 := by rw [s]
    _ = y := by ring

8.1.7. 例

问题

证明从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x \mapsto x ^ 2\) 不是满射。

解答

我们将证明存在实数 \(y\)，使得对所有实数 \(x\)，都有 \(x^2\ne y\)。

确实，我们证明 -1 具有这个性质。设 \(x\) 为实数。那么

\[\begin{split}-1&<0\\ &\le x^2,\end{split}\]

所以 \(x^2\ne -1\)。

和例 8.1.4 中一样，第一句话构成了在当前语境中对“满射”定义的否定规范化。实际上，我们是在陈述 Lean 证明中使用 push_neg 之后将出现的目标状态。

⊢ ∃ y, ∀ (x : ℝ), x ^ 2 ≠ y

下面是完整的 Lean 证明。

example : ¬ Surjective (fun x : ℝ ↦ x ^ 2) := by
  dsimp [Surjective]
  push_neg
  use -1
  intro x
  apply ne_of_gt
  calc -1 < 0 := by numbers
    _ ≤ x ^ 2 := by extra

8.1.8. 例

到目前为止，我们已经见过数值类型，例如整数 \(\mathbb{Z}\) 和实数 \(\mathbb{R}\)，以及函数类型，例如 \(\mathbb{Z}\to \mathbb{R}\)（从 \(\mathbb{Z}\) 到 \(\mathbb{R}\) 的函数）。

构造类型的另一种方式是把类型看作有限个选项的集合。有限类型对概念性例子很有用，因为一切都是显式且可检查的。

inductive Musketeer
  | athos
  | porthos
  | aramis
  deriving DecidableEq

下面说明如何定义一个定义域为给定有限归纳类型的函数。

def f : Musketeer → Musketeer
  | athos => aramis
  | porthos => aramis
  | aramis => athos

问题

证明函数 \(f\) 不是单射。

example : ¬ Injective f := by
  dsimp [Injective]
  push_neg
  use athos, porthos
  dsimp [f] -- optional
  exhaust

这里的新策略是 exhaust。在使用它的位置，目标状态是

aramis = aramis ∧ athos ≠ porthos

也就是

True ∧ ¬ False

这与 True 逻辑等价。策略 exhaust 可以完成这种命题逻辑推理，复杂度不限。

特别地，exhaust 可以证明归纳类型中任何（为真的）无变量陈述；这就是本章中我们使用它的方式。我们会在第 9 章开始更认真地使用 exhaust。

8.1.9. 例

问题

证明例 8.1.8 中定义的函数 \(f\) 不是满射。

对于有限归纳类型中的变量 a，我们可以使用策略 cases 作分类检查。

example : ¬ Surjective f := by
  dsimp [Surjective]
  push_neg
  use porthos
  intro a
  cases a
  · exhaust
  · exhaust
  · exhaust

这样的证明可能变得重复；你也许想使用我们以前见过的技巧（例如例 4.4.4、例 4.5.9、例 6.6.2、例 6.7.2）：当某个策略（如 cases）生成许多都能由同一个策略证明的目标时，可以写 <;> 把该策略应用到所有这些目标上。

-- better (more automated) version of the previous proof
example : ¬ Surjective f := by
  dsimp [Surjective]
  push_neg
  use porthos
  intro a
  cases a <;> exhaust

你也可以检查 cases a <;> exhaust 这一行是必要的；exhaust 无法独自关闭目标。正如例 8.1.8 中所讨论的，exhaust 可以证明归纳类型中任何（为真的）无变量陈述，但在 cases a <;> exhaust 这一行之前，目标状态是

a : Musketeer
⊢ f a ≠ porthos

其中含有一个变量 a。

8.1.10. 例

设 \(g\) 为如下从 Musketeer 类型到自身的函数：

def g : Musketeer → Musketeer
  | athos => porthos
  | porthos => aramis
  | aramis => athos

问题

证明函数 \(g\) 是单射。

这个证明中有很多情形，准确地说有 \(3 \times 3 = 9\) 个。幸运的是，exhaust 可以证明全部情形！

example : Injective g := by
  dsimp [Injective]
  intro x1 x2 hx
  cases x1 <;> cases x2 <;> exhaust

8.1.11. 例

问题

证明例 8.1.10 中定义的函数 \(g\) 是满射。

example : Surjective g := by
  dsimp [Surjective]
  intro y
  cases y
  · use aramis
    exhaust
  · use athos
    exhaust
  · use porthos
    exhaust

8.1.12. 例

我们以一个相对较难的例子结束。本证明高效且自洽，但动机并不特别明显。若想要另一种（也许更直观的）做法，请把本节最后一道练习（关于严格单调函数的那道）与例 2.1.8 的思想结合起来。

问题

证明从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x \mapsto x ^ 3\) 是单射。

解答

设 \(x_1\) 和 \(x_2\) 为实数，并假设 \(x_1{}^3=x_2{}^3\)。那么

\[\begin{split}(x_1-x_2)(x_1{}^2+x_1x_2+x_2{}^2)&=x_1{}^3-x_2{}^3\\ &=x_1{}^3-x_1{}^3\\ &=0,\end{split}\]

所以要么 \(x_1-x_2=0\)，此时证明完成；要么 \(x_1{}^2+x_1x_2+x_2{}^2=0\)，以下假设后一种情形。

现在我们进一步按照 \(x_1=0\) 是否成立分类讨论。

情形 1（\(x_1=0\)）：那么

\[\begin{split}x_2{}^3&=x_1{}^3\\ &=0^3\\&=0,\end{split}\]

所以 \(x_2=0\)。于是 \(x_1=0=x_2\)，如所需。

情形 2（\(x_1\ne 0\)）：那么

\[\begin{split}0&< x_1{}^2+\left((x_1+x_2)^2+x_2{}^2\right)\\ &=2(x_1{}^2+x_1x_2+x_2{}^2)\\ &=2\cdot 0\\ &=0,\end{split}\]

矛盾。

example : Injective (fun (x:ℝ) ↦ x ^ 3) := by
  intro x1 x2 hx
  dsimp at hx
  have H : (x1 - x2) * (x1 ^ 2 + x1 * x2 + x2 ^ 2) = 0
  · calc (x1 - x2) * (x1 ^ 2 + x1 * x2 + x2 ^ 2) = x1 ^ 3 - x2 ^ 3 := by ring
      _ = x1 ^ 3 - x1 ^ 3 := by rw [hx]
      _ = 0 := by ring
  rw [mul_eq_zero] at H
  obtain H1 | H2 := H
  · -- case 1: x1 - x2 = 0
    addarith [H1]
  · -- case 2: x1 ^2 + x1 * x2 + x2 ^ 2  = 0
    by_cases hx1 : x1 = 0
    · -- case 2a: x1 = 0
      have hx2 :=
      calc x2 ^ 3 = x1 ^ 3 := by rw [hx]
        _ = 0 ^ 3 := by rw [hx1]
        _ = 0 := by numbers
      cancel 3 at hx2
      calc x1 = 0 := by rw [hx1]
        _ = x2 := by rw [hx2]
    · -- case 2b: x1 ≠ 0
      have :=
      calc 0 < x1 ^ 2 + ((x1 + x2) ^ 2 + x2 ^ 2) := by extra
          _ = 2 * (x1 ^ 2 + x1 * x2 + x2 ^ 2) := by ring
          _ = 2 * 0 := by rw [H2]
          _ = 0 := by ring
      numbers at this -- contradiction!

8.1.13. 练习

证明或反驳：从 \(\mathbb{Q}\) 到 \(\mathbb{Q}\) 的函数 \(x \mapsto x-12\) 是单射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Injective (fun (x : ℚ) ↦ x - 12) := by
  sorry

example : ¬ Injective (fun (x : ℚ) ↦ x - 12) := by
  sorry
```
证明或反驳：从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x \mapsto 3\) 是单射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Injective (fun (x : ℝ) ↦ 3) := by
  sorry

example : ¬ Injective (fun (x : ℝ) ↦ 3) := by
  sorry
```
证明或反驳：从 \(\mathbb{Q}\) 到 \(\mathbb{Q}\) 的函数 \(x \mapsto 3x-1\) 是单射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Injective (fun (x : ℚ) ↦ 3 * x - 1) := by
  sorry

example : ¬ Injective (fun (x : ℚ) ↦ 3 * x - 1) := by
  sorry
```
证明或反驳：从 \(\mathbb{Z}\) 到 \(\mathbb{Z}\) 的函数 \(x \mapsto 3x-1\) 是单射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Injective (fun (x : ℤ) ↦ 3 * x - 1) := by
  sorry

example : ¬ Injective (fun (x : ℤ) ↦ 3 * x - 1) := by
  sorry
```
证明或反驳：从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x \mapsto 2x\) 是满射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Surjective (fun (x : ℝ) ↦ 2 * x) := by
  sorry

example : ¬ Surjective (fun (x : ℝ) ↦ 2 * x) := by
  sorry
```
证明或反驳：从 \(\mathbb{Z}\) 到 \(\mathbb{Z}\) 的函数 \(x \mapsto 2x\) 是满射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Surjective (fun (x : ℤ) ↦ 2 * x) := by
  sorry

example : ¬ Surjective (fun (x : ℤ) ↦ 2 * x) := by
  sorry
```
证明或反驳：从 \(\mathbb{N}\) 到 \(\mathbb{N}\) 的函数 \(n \mapsto n^2\) 是满射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Surjective (fun (n : ℕ) ↦ n ^ 2) := by
  sorry

example : ¬ Surjective (fun (n : ℕ) ↦ n ^ 2) := by
  sorry
```

考虑如下有限归纳类型 White，以及如下从 Musketeer 类型（见例 8.1.8）到 White 类型的函数 \(h\)。证明或反驳：函数 \(h\) 是单射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）

inductive White
  | meg
  | jack
  deriving DecidableEq

open White

def h : Musketeer → White
  | athos => jack
  | porthos => meg
  | aramis => jack

example : Injective h := by
  sorry

example : ¬ Injective h := by
  sorry

证明或反驳：前一例中的函数 \(h\) 是满射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Surjective h := by
  sorry

example : ¬ Surjective h := by
  sorry
```
考虑如下从 White 类型（见前两题）到 Musketeer 类型（见例 8.1.8）的函数 \(l\)。证明或反驳：函数 \(l\) 是单射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
def l : White → Musketeer
  | meg => aramis
  | jack => porthos

example : Injective l := by
  sorry

example : ¬ Injective l := by
  sorry
```
证明或反驳：前一例中的函数 \(l\) 是满射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Surjective l := by
  sorry

example : ¬ Surjective l := by
  sorry
```
设 \(f : X \to Y\) 为函数。证明：\(f\) 为单射，当且仅当对类型 \(X\) 的所有 \(x_1\) 和 \(x_2\)，若 \(x_1\ne x_2\)，则 \(f(x_1)\ne f(x_2)\)。你需要使用能够处理较微妙否定的策略，例如 push_neg 或 by_cases。
```
example (f : X → Y) : Injective f ↔ ∀ x1 x2 : X, x1 ≠ x2 → f x1 ≠ f x2 := by
  sorry
```

证明或反驳：对所有函数 \(f:\mathbb{Q}\to \mathbb{Q}\)，若 \(f\) 为单射，则从 \(\mathbb{Q}\) 到 \(\mathbb{Q}\) 的函数 \(x \mapsto f(x)+1\) 也为单射。

example : ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + 1) := by
  sorry

example : ¬ ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + 1) := by
  sorry

证明或反驳：对所有函数 \(f:\mathbb{Q}\to \mathbb{Q}\)，若 \(f\) 为单射，则从 \(\mathbb{Q}\) 到 \(\mathbb{Q}\) 的函数 \(x \mapsto f(x)+x\) 也为单射。

example : ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + x) := by
  sorry

example : ¬ ∀ (f : ℚ → ℚ), Injective f → Injective (fun x ↦ f x + x) := by
  sorry

证明或反驳：对所有函数 \(f:\mathbb{Z}\to \mathbb{Z}\)，若 \(f\) 为满射，则从 \(\mathbb{Z}\) 到 \(\mathbb{Z}\) 的函数 \(x \mapsto 2f(x)\) 也为满射。

example : ∀ (f : ℤ → ℤ), Surjective f → Surjective (fun x ↦ 2 * f x) := by
  sorry

example : ¬ ∀ (f : ℤ → ℤ), Surjective f → Surjective (fun x ↦ 2 * f x) := by
  sorry

证明或反驳：对所有实数 \(c\)，从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x\mapsto cx\) 都是满射。

example : ∀ c : ℝ, Surjective (fun x ↦ c * x) := by
  sorry

example : ¬ ∀ c : ℝ, Surjective (fun x ↦ c * x) := by
  sorry

设 \(f:\mathbb{Q}\to\mathbb{Q}\) 为严格单调函数；也就是说，对所有满足 \(xlt_trichotomy；它按两个有理数大小关系作分类讨论。

lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ x < y :=

example {f : ℚ → ℚ} (hf : ∀ x y, x < y → f x < f y) : Injective f := by
  sorry

设 \(f:X\to\mathbb{N}\) 为函数，设 \(x_0\) 为类型 \(X\) 的元素且满足 \(f(x_0)=0\)，并设 \(i:X\to X\) 为函数，满足对所有 \(x\)，都有 \(f(i(x))=f(x)+1\)。证明 \(f\) 是满射。我建议使用归纳法。我们把这个定理记为 surjective_of_intertwining，供以后使用。
```
example {f : X → ℕ} {x0 : X} (h0 : f x0 = 0) {i : X → X}
    (hi : ∀ x, f (i x) = f x + 1) : Surjective f := by
  sorry
```

8.2. 双射性

8.2.1. 定义

定义

一个函数称为双射，如果它既是单射又是满射。

def Bijective (f : X → Y) : Prop := Injective f ∧ Surjective f

8.2.2. 例

问题

设 \(p:\mathbb{R}\to\mathbb{R}\) 为函数，定义为 \(p(x)=2x-5\)。证明 \(p\) 是双射。

解答

我们必须证明 \(p\) 是单射且是满射。

对于单射性，设 \(x_1\) 和 \(x_2\) 为实数，并假设 \(p(x_1)=p(x_2)\)。这意味着 \(2x_1-5=2x_2-5\)。所以

\[\begin{split}x_1&= \frac{(2x_1-5)+5}{2}\\ &= \frac{(2x_2-5)+5}{2}\\ &=x_2.\end{split}\]

对于满射性，设 \(y\) 为实数。那么

\[\begin{split}p \left(\frac{y+5}{2}\right)&=2\left(\frac{y+5}{2}\right)-5\\ &=y.\end{split}\]

def p (x : ℝ) : ℝ := 2 * x - 5

example : Bijective p := by
  dsimp [Bijective]
  constructor
  · dsimp [Injective]
    intro x1 x2 hx
    dsimp [p] at hx
    calc x1 = ((2 * x1 - 5) + 5) / 2 := by ring
      _ = ((2 * x2 - 5) + 5) / 2 := by rw [hx]
      _ = x2 := by ring
  · dsimp [Surjective]
    intro y
    use (y + 5) / 2
    calc p ((y + 5) / 2) = 2 * ((y + 5) / 2) - 5 := by rfl
      _ = y := by ring

8.2.3. 例

问题

设 \(a:\mathbb{R}\to\mathbb{R}\) 为函数，定义为 \(a(t)=t^3-t\)。证明 \(a\) 不是双射。

解答

我们将证明 \(a\) 不是单射。确实，注意 \(0\ne 1\)，但

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

def a (t : ℝ) : ℝ := t ^ 3 - t

example : ¬ Bijective a := by
  dsimp [Bijective]
  push_neg
  left
  dsimp [Injective]
  push_neg
  use 0, 1
  constructor
  · calc a 0 = 0 ^ 3 - 0 := by rfl
      _ = 1 ^ 3 - 1 := by numbers
      _ = a 1 := by rfl
  · numbers

8.2.4. 例

考虑如下有限归纳类型 Celestial 和 Subatomic：

inductive Celestial
  | sun
  | moon
  deriving DecidableEq

inductive Subatomic
  | proton
  | neutron
  | electron
  deriving DecidableEq

考虑如下从 Celestial 类型到 Subatomic 类型的函数 \(f\)。

def f : Celestial → Subatomic
  | sun => proton
  | moon => electron

问题

证明函数 \(f\) 不是双射。

example : ¬ Bijective f := by
  dsimp [Bijective]
  push_neg
  right
  dsimp [Surjective]
  push_neg
  use neutron
  intro x
  cases x <;> exhaust

8.2.5. 例

定理

函数 \(f:X\to Y\) 是双射，当且仅当对类型 \(Y\) 的每个 \(y\)，存在唯一一个类型 \(X\) 的 \(x\)，使得 \(f(x)=y\)。

证明

首先，假设 \(f\) 是双射。设 \(y\) 为类型 \(Y\) 的元素。由于 \(f\) 是满射，存在类型 \(X\) 的 \(x\)，使得 \(f(x)=y\)。我们将证明这个 \(x\) 是唯一的。确实，对任意另一个满足 \(f(x')=y\) 的 \(x'\)，有

\[\begin{split}f(x')&=y\\ &=f(x),\end{split}\]

于是由 \(f\) 的单射性，\(x'=x\)。

反过来，假设对类型 \(Y\) 的每个 \(y\)，存在唯一一个类型 \(X\) 的 \(x\)，使得 \(f(x)=y\)。（\(\star\)）我们必须证明 \(f\) 是单射且是满射。

对于单射性，设 \(x_1\) 和 \(x_2\) 为类型 \(X\) 的元素，并假设 \(f(x_1)=f(x_2)\)。将（\(\star\)）应用于 \(y=f(x_1)\)，存在唯一一个类型 \(X\) 的 \(x\)，使得 \(f(x)=f(x_1)\)。所以由唯一性，\(x_1=x\)；并且由于 \(f(x_2)=f(x_1)=f(x)\)，也有 \(x_2=x\)。合并可得 \(x_1=x_2\)。

对于满射性，设 \(y\) 为类型 \(Y\) 的元素。由（\(\star\)），存在（唯一）类型 \(X\) 的 \(x\)，使得 \(f(x)=y\)。

example {f : X → Y} : Bijective f ↔ ∀ y, ∃! x, f x = y := by
  constructor
  · -- if `f` is bijective then `∀ y, ∃! x, f x = y`
    intro h y
    obtain ⟨h_inj, h_surj⟩ := h
    obtain ⟨x, hx⟩ := h_surj y
    use x
    dsimp
    constructor
    · apply hx
    · intro x' hx'
      apply h_inj
      calc f x' = y := by rw [hx']
        _ = f x := by rw [hx]
  · -- if `∀ y, ∃! x, f x = y` then `f` is bijective
    intro h
    constructor
    · -- `f` is injective
      intro x1 x2 hx1x2
      obtain ⟨x, hx, hx'⟩ := h (f x1)
      have hxx1 : x1 = x
      · apply hx'
        rfl
      have hxx2 : x2 = x
      · apply hx'
        rw [hx1x2]
      calc x1 = x := by rw [hxx1]
        _ = x2 := by rw [hxx2]
    · -- `f` is surjective
      intro y
      obtain ⟨x, hx, hx'⟩ := h y
      use x
      apply hx

8.2.6. 例

问题

证明：对从 Celestial 类型（例 8.2.4）到自身的所有函数 \(f\)，若 \(f\) 是单射，则它是双射。

我们通过穷尽分析从 Celestial 类型到自身的所有函数 \(f\) 来证明。这样的函数共有四个。下面我处理了前两种情形；请你自行补全后两种。

example : ∀ f : Celestial → Celestial, Injective f → Bijective f := by
  intro f hf
  constructor
  · -- `f` is injective by assumption
    apply hf
  -- show that `f` is surjective
  match h_sun : f sun, h_moon : f moon with
  | sun, sun =>
    have : sun = moon
    · apply hf
      rw [h_sun, h_moon]
    contradiction
  | sun, moon =>
    intro y
    cases y
    · use sun
      apply h_sun
    · use moon
      apply h_moon
  | moon, sun => sorry
  | moon, moon => sorry

8.2.7. 例

问题

证明：并非对所有函数 \(f:\mathbb{N}\to \mathbb{N}\)，若 \(f\) 是单射，则它是双射。

解答

我们必须证明存在一个函数 \(f:\mathbb{N}\to \mathbb{N}\)，它是单射但不是双射。

确实，考虑函数 \(f(n)=n+1\)。这个函数是单射，因为对所有自然数 \(n_1\) 和 \(n_2\)，若 \(n_1+1=n_2+1\)，则 \(n_1=n_2\)。

然而，这个函数不是满射，因此不是双射。要看出这一点，注意对所有自然数 \(n\)，都有 \(f(n)=n+1>0\)，因此 \(f(n)\ne 0\)。

example : ¬ ∀ f : ℕ → ℕ, Injective f → Bijective f := by
  push_neg
  use fun n ↦ n + 1
  constructor
  · -- the function is injective
    intro n1 n2 hn
    addarith [hn]
  · -- the function is not bijective
    dsimp [Bijective]
    push_neg
    right
    -- specifically, it's not surjective
    dsimp [Surjective]
    push_neg
    use 0
    intro n
    apply ne_of_gt
    extra

8.2.8. 练习

证明或反驳：从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x \mapsto 4-3x\) 是双射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Bijective (fun (x : ℝ) ↦ 4 - 3 * x) := by
  sorry

example : ¬ Bijective (fun (x : ℝ) ↦ 4 - 3 * x) := by
  sorry
```
证明或反驳：从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(x \mapsto x^2+2x\) 是双射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）
```
example : Bijective (fun (x : ℝ) ↦ x ^ 2 + 2 * x) := by
  sorry

example : ¬ Bijective (fun (x : ℝ) ↦ x ^ 2 + 2 * x) := by
  sorry
```

考虑如下有限归纳类型 Element，以及如下从 Element 类型到自身的函数 \(e\)。证明或反驳：函数 \(e\) 是双射。（若你认为它为真，请完成下面第一个版本；若你认为它为假，请完成第二个版本。）

inductive Element
  | fire
  | water
  | earth
  | air
  deriving DecidableEq

open Element

def e : Element → Element
  | fire => earth
  | water => air
  | earth => fire
  | air => water

example : Bijective e := by
  sorry

example : ¬ Bijective e := by
  sorry

证明：对从 Subatomic 类型（例 8.2.4）到自身的所有函数 \(f\)，若 \(f\) 是单射，则它是双射。这类似于例 8.2.6，但需要检查更多情形。
```
example : ∀ f : Subatomic → Subatomic, Injective f → Bijective f := by
  sorry
```
考虑前一道练习中的有限归纳类型 Element。证明：对从 Element 类型到自身的所有函数 \(f\)，若 \(f\) 是单射，则它是双射。这类似于例 8.2.6 和前一道练习，但需要检查更多情形，多到坦率地说有点过多。
```
example : ∀ f : Element → Element, Injective f → Bijective f := by
  sorry
```

8.3. 函数复合

8.3.1. 定义

定义

函数 \(g : Y \to Z\) 与函数 \(f : X \to Y\) 的复合，是从 \(X\) 到 \(Z\) 的函数，它把 \(x\) 送到 \(g(f(x))\)。

def comp (f : X → Y) (g : Y → Z) (x : X) : Z := g (f x)

\(g : Y \to Z\) 与 \(f : X \to Y\) 的复合记为 \(g \circ f\)（在 Lean 中为 g ∘ f）。

8.3.2. 例

问题

设 \(f:\mathbb{R}\to\mathbb{R}\) 为函数，定义为 \(f(a)=a+3\)。设 \(g:\mathbb{R}\to\mathbb{R}\) 为函数，定义为 \(g(b)=2b\)。设 \(h:\mathbb{R}\to\mathbb{R}\) 为函数，定义为 \(h(c)=2c+6\)。

证明 \(g \circ f = h\)。

解答

设 \(x\) 为实数。那么

\[\begin{split}(g \circ f) (x)&=g(f(x))\\ &=2(x+3)\\ &=2x+6\\ &=h(x).\end{split}\]

在 Lean 证明中，注意新策略 ext。要证明两个函数相等，我们必须证明它们在每个输入上都相等。这正是策略 ext 所做的事。（这个名称代表“外延性”。）在使用它之前，目标状态是

⊢ g ∘ f = h

使用它之后，目标状态是

x : ℝ
⊢ (g ∘ f) x = h x

下面是完整的 Lean 证明。

def f (a : ℝ) : ℝ := a + 3
def g (b : ℝ) : ℝ := 2 * b
def h (c : ℝ) : ℝ := 2 * c + 6

example : g ∘ f = h := by
  ext x
  calc (g ∘ f) x = g (f x) := by rfl
    _ = 2 * (x + 3) := by rfl
    _ = 2 * x + 6 := by ring
    _ = h x := by rfl

8.3.3. 定义

定义

恒等函数 \(\operatorname{Id}_X:X\to X\) 是把类型 \(X\) 的每个 \(x\) 送到其自身的函数。

def id (x : X) : X := x

8.3.4. 例

问题

设 \(s:\mathbb{R}\to\mathbb{R}\) 为函数，定义为 \(s(x)=5-x\)。

证明 \(s \circ s = \operatorname{Id}_\mathbb{R}\)。

解答

设 \(x\) 为实数。我们必须证明 \(5 - (5 - x) = x\)，这是真的。

def s (x : ℝ) : ℝ := 5 - x

example : s ∘ s = id := by
  ext x
  dsimp [s]
  ring

8.3.5. 定义

定义

函数 \(g : Y \to X\) 称为 \(f : X \to Y\) 的逆，如果 \(g \circ f=\operatorname{Id}_X\) 且 \(f \circ g=\operatorname{Id}_Y\)。

def Inverse (f : X → Y) (g : Y → X) : Prop := g ∘ f = id ∧ f ∘ g = id

8.3.6. 例

考虑如下有限归纳类型 Humour：

inductive Humour
  | melancholic
  | choleric
  | phlegmatic
  | sanguine
  deriving DecidableEq

考虑如下从 Humour 类型到自身的函数 \(p\)。

def p : Humour → Humour
  | melancholic => choleric
  | choleric => sanguine
  | phlegmatic => phlegmatic
  | sanguine => melancholic

问题

定义一个从 Humour 类型到自身、作为 \(p\) 的逆的函数 \(q\)，并证明这一点。

def q : Humour → Humour
  | melancholic => sanguine
  | choleric => melancholic
  | phlegmatic => phlegmatic
  | sanguine => choleric

example : Inverse p q := by
  constructor
  · ext x
    cases x <;> exhaust
  · ext x
    cases x <;> exhaust

8.3.7. 例

命题

设 \(f : X \to Y\) 为双射函数。则存在函数 \(g : Y \to X\)，它是 \(f\) 的逆。

证明

如下定义函数 \(g : Y \to X\)：给定类型 \(Y\) 的 \(y\)，由 \(f\) 的满射性，存在类型 \(X\) 的 \(x\) 使得 \(f(x)=y\)，于是把 \(g(y)\) 定义为这个 \(x\)。这样，对所有 \(y\)，都有 \(f(g(y))=y\)。（\(\star\)）

这立即给出 \(f \circ g = \operatorname{Id}_Y\)。为了证明 \(g \circ f = \operatorname{Id}_X\)，设 \(x\) 为类型 \(X\) 的元素。由（\(\star\)）可知

\[\begin{split}f((g \circ f)(x))&=f(g(f(x)))\\ &=f(x)\\ &=f(\operatorname{Id}_X(x)),\end{split}\]

因此由 \(f\) 的单射性，推出 \((g \circ f)(x) = \operatorname{Id}_X(x)\)。

要在 Lean 中写出这个证明，我们需要一个本书其他地方不会用到的策略 choose。这个策略会构造文字证明第一段中描述的函数 \(g : Y \to X\)。更准确地说，给定假设

h_surj: ∀ (b : Y), ∃ a, f a = b

策略调用 choose g hg using h_surj 会创建一个函数：它为每个 \(b\) 选择一个相应的 \(a\)：

g : Y → X
hg : ∀ (b : Y), f (g b) = b

下面是在 Lean 中的完整证明。

theorem exists_inverse_of_bijective {f : X → Y} (hf : Bijective f) :
    ∃ g : Y → X, Inverse f g := by
  dsimp [Bijective] at hf
  obtain ⟨h_inj, h_surj⟩ := hf
  dsimp [Surjective] at h_surj
  choose g hg using h_surj
  use g
  dsimp [Inverse]
  constructor
  · -- prove `g ∘ f = id`
    ext x
    dsimp [Injective] at h_inj
    apply h_inj
    calc f ((g ∘ f) x) = f (g (f x)) := by rfl
      _ = f x := by apply hg
      _ = f (id x) := by rfl
  · -- prove `f ∘ g = id`
    ext y
    apply hg

8.3.8. 例

命题

设 \(f : X \to Y\) 与 \(g : Y \to X\) 为函数，并且 \(g : Y \to X\) 是 \(f : X \to Y\) 的逆。则 \(f : X \to Y\) 是双射。

证明

我们先证明 \(f\) 是单射。确实，设 \(x_1\) 与 \(x_2\) 为类型 \(X\) 的元素，并假设 \(f(x_1)=f(x_2)\)。则

\[\begin{split}x_1&=\operatorname{Id}_X(x_1)\\ &=(g\circ f)(x_1)\\ &=g(f(x_1))\\ &=g(f(x_2))\\ &=(g\circ f)(x_2)\\ &=\operatorname{Id}_X(x_2)\\ &=x_2.\end{split}\]

现在证明 \(f\) 是满射。确实，设 \(y\) 为类型 \(Y\) 的元素。则

\[\begin{split}f(g(y))&=(f\circ g)(y)\\ &=\operatorname{Id}_Y(y)\\ &=y.\end{split}\]

theorem bijective_of_inverse {f : X → Y} {g : Y → X} (h : Inverse f g) :
    Bijective f := by
  dsimp [Inverse] at h
  obtain ⟨hgf, hfg⟩ := h
  constructor
  · -- `f` is injective
    intro x1 x2 hx
    calc x1 = id x1 := by rfl
      _ = (g ∘ f) x1 := by rw [hgf]
      _ = g (f x1) := by rfl
      _ = g (f x2) := by rw [hx]
      _ = (g ∘ f) x2 := by rfl
      _ = id x2 := by rw [hgf]
      _ = x2 := by rfl
  · -- `f` is surjective
    intro y
    use g y
    calc f (g y) = (f ∘ g) y := by rfl
      _ = id y := by rw [hfg]
      _ = y := by rfl

8.3.9. 例

定理

设 \(f : X \to Y\) 为函数。则 \(f\) 是双射，当且仅当存在函数 \(g : Y \to X\)，它是 \(f\) 的逆。

证明

第一个方向由例 8.3.7 给出，第二个方向由例 8.3.8 给出。

theorem bijective_iff_exists_inverse (f : X → Y) :
    Bijective f ↔ ∃ g : Y → X, Inverse f g := by
  constructor
  · apply exists_inverse_of_bijective
  · intro h
    obtain ⟨g, H⟩ := h
    apply bijective_of_inverse H

8.3.10. 练习

考虑如下从 Humour 类型（见例 8.3.6）到自身的函数 \(a\) 和 \(b\)。写出一个从 Humour 类型到自身的函数 \(c\)，使得 \(b \circ a=c\)。当你写出的函数正确时，附带的证明会通过。

def a : Humour → Humour
  | melancholic => sanguine
  | choleric => choleric
  | phlegmatic => phlegmatic
  | sanguine => melancholic

def b : Humour → Humour
  | melancholic => phlegmatic
  | choleric => phlegmatic
  | phlegmatic => melancholic
  | sanguine => sanguine

def c : Humour → Humour
  | melancholic => sorry
  | choleric => sorry
  | phlegmatic => sorry
  | sanguine => sorry

example : b ∘ a = c := by
  ext x
  cases x <;> exhaust

考虑函数 \(u:\mathbb{R}\to\mathbb{R}\)，定义为 \(u(x)=5x+1\)。写出一个从 \(\mathbb{R}\) 到 \(\mathbb{R}\) 的函数 \(v\)，它是 \(u\) 的逆，并证明这一点。
```
def u (x : ℝ) : ℝ := 5 * x + 1

noncomputable def v (x : ℝ) : ℝ := sorry

example : Inverse u v := by
  sorry
```

设 \(f : X \to Y\) 与 \(g : Y \to Z\) 为单射函数。证明 \(g \circ f\) 也是单射。

example {f : X → Y} (hf : Injective f) {g : Y → Z} (hg : Injective g) :
    Injective (g ∘ f) := by
  sorry

设 \(f : X \to Y\) 与 \(g : Y \to Z\) 为满射函数。证明 \(g \circ f\) 也是满射。

example {f : X → Y} (hf : Surjective f) {g : Y → Z} (hg : Surjective g) :
    Surjective (g ∘ f) := by
  sorry

设 \(f : X \to Y\) 为满射函数。证明存在函数 \(g : Y \to X\)，使得 \(f \circ g=\operatorname{Id}_Y\)。
```
example {f : X → Y} (hf : Surjective f) : ∃ g : Y → X, f ∘ g = id := by
  sorry
```
设 \(f : X \to Y\) 与 \(g : Y \to X\) 为函数，并且 \(g\) 是 \(f\) 的逆。证明 \(f\) 是 \(g\) 的逆。
```
example {f : X → Y} {g : Y → X} (h : Inverse f g) : Inverse g f := by
  sorry
```
设 \(f : X \to Y\) 与 \(g_1,g_2 : Y \to X\) 为函数，并且 \(g_1\) 和 \(g_2\) 都是 \(f\) 的逆。证明 \(g_1=g_2\)。本题说明：若函数 \(f\) 有逆，则其逆唯一。
```
example {f : X → Y} {g1 g2 : Y → X} (h1 : Inverse f g1) (h2 : Inverse f g2) :
    g1 = g2 := by
  sorry
```

脚注

1: 熟悉相关内容的读者会认出，这就是选择公理。

8.4. 积类型

8.4.1. 例

问题

考虑函数 \(q:\mathbb{Z}\to\mathbb{Z}^2\)，定义为 \(q(m)=(m + 1, 2 - m)\)。证明 \(q\) 是

单射；
非满射。

解答

设 \(m_1\) 和 \(m_2\) 为整数，并假设 \(q(m_1)=q(m_2)\)。于是按定义有 \[(m_1+1,2-m_1)=(m_2+1,2-m_2),\] 所以 \(m_1+1=m_2+1\) 且 \(2-m_1=2-m_2\)，从而 \(m_1=m_2\)。
我们将证明存在 \(\mathbb{Z}^2\) 中的 \((a,b)\)，使得对所有整数 \(m\)，都有 \(q(m)\ne(a,b)\)。确实，我们证明 \((0,1)\) 具有这个性质。假设存在整数 \(m\) 满足 \(q(m)=(0,1)\)。则按定义有 \[(m+1,2-m)=(0,1),\] 所以 \(m+1=0\) 且 \(2-m=1\)，于是 \[\begin{split}1&=(m+1)+(2-m)-2\\ &=0+1-2\\ &=-1,\end{split}\] 矛盾。

要在 Lean 中写出这些证明，请注意在单射性问题中使用策略 obtain：它把积类型等式的假设

hm : (m1 + 1, 2 - m1) = (m2 + 1, 2 - m2)

转化为关于两个分量分别相等的两个假设：

hm' : m1 + 1 = m2 + 1
hm'' : 2 - m1 = 2 - m2

这与你应当如何理解积类型中的相等是一致的：两个有序对相等，当且仅当它们的左分量相等且右分量相等。因此我们使用与逻辑联结词“且”相同的策略和语法。

def q (m : ℤ) : ℤ × ℤ := (m + 1, 2 - m)

example : Injective q := by
  dsimp [Injective]
  intro m1 m2 hm
  dsimp [q] at hm
  obtain ⟨hm', hm''⟩ := hm
  addarith [hm']

在非满射性问题中，策略 obtain 也类似地用来分解一个积类型等式的假设，

hm : (m + 1, 2 - m) = (0, 1)

这个假设正是在该问题中出现的。

example : ¬ Surjective q := by
  dsimp [Surjective]
  push_neg
  use (0, 1)
  intro m hm
  dsimp [q] at hm
  obtain ⟨hm1, hm2⟩ := hm
  have H : 1 = -1 := by addarith [hm1, hm2]
  numbers at H

8.4.2. 例

问题

考虑从 \(\mathbb{Z}^2\) 到 \(\mathbb{Z}^2\) 的函数 \((m,n)\mapsto (m+n,m+2n)\)。证明这个函数是双射。

通常，证明一个函数为双射的最高效方法，是给出它的一个逆。根据例 8.3.9 中证明的定理，这已经足够。找出这个逆应当作为草稿工作来做，通常在纸上做，而不是在 Lean 中做。例如，在本题中，你可以写出逆函数必须满足的关于 \((a,b)\) 的方程：

\[(a,b)=(m+n, m+2n)\]

并把它化简为一个整数方程组，然后解出 \(m\) 和 \(n\)：

\[\begin{split}a&=m+n\\ b&=m+2n\\ b-a&=(m+2n)-(m+n)\\ &=n\\ n&=b-a\\ a&=m+n\\ &=m+(b-a)\\ a-(b-a)&=m\\ 2a-b&=m\\ m&=2a-b\end{split}\]

由此可知，逆函数的一个好候选是从 \(\mathbb{Z}^2\) 到 \(\mathbb{Z}^2\) 的函数 \((a,b)\mapsto (2a-b,b-a)\)。但这些草稿工作不写进正式解答，无论纸笔解答还是 Lean 证明都不写。正式写作中，只要直接给出这个逆并检查它确实成立即可。

解答

由例 8.3.9，只需证明该函数有逆。我们将证明函数 \((a,b)\mapsto (2a-b,b-a)\) 是它的逆。

首先，对 \(\mathbb{Z}^2\) 中任意 \((m,n)\)，有

\[\left(2 (m + n) - (m + 2 n), (m + 2 n) - (m + n)\right) = (m, n).\]

其次，对 \(\mathbb{Z}^2\) 中任意 \((a,b)\)，有

\[\left((2 a - b) + (b - a), (2 a - b) + 2 (b - a)\right) = (a, b).\]

在 Lean 中，请注意：

引理 bijective_iff_exists_inverse，这是例 8.3.9 中定理在 Lean 中的名称；
使用策略 ext（回忆例 8.3.2），通过证明两个函数在任意输入处相等来证明它们相等。

example : Bijective (fun ((m, n) : ℤ × ℤ) ↦ (m + n, m + 2 * n)) := by
  rw [bijective_iff_exists_inverse]
  use fun (a, b) ↦ (2 * a - b, b - a)
  constructor
  · ext ⟨m, n⟩
    dsimp
    ring
  · ext ⟨a, b⟩
    dsimp
    ring

8.4.3. 例

例 8.4.2 的思想可以相当灵活地改造，特别是在有理数和实数上。请自己尝试下面这题。

问题

考虑从 \(\mathbb{R}^2\) 到 \(\mathbb{R}^2\) 的函数 \((m,n)\mapsto (m+n,m-n)\)。证明这个函数是双射。

example : Bijective (fun ((m, n) : ℝ × ℝ) ↦ (m + n, m - n)) := by
  sorry

但在整数上会出现麻烦。你会发现，前一个例子中想到的逆函数涉及除法；这在 \(\mathbb{R}\) 上没有问题，却不能在 \(\mathbb{Z}\) 上使用。事实上，在这种情况下，该函数作为从 \(\mathbb{Z}^2\) 到 \(\mathbb{Z}^2\) 的映射并不是双射。

问题

考虑从 \(\mathbb{Z}^2\) 到 \(\mathbb{Z}^2\) 的函数 \((m,n)\mapsto (m+n,m-n)\)。证明这个函数不是双射。

解答

我们将证明这个函数不是满射。事实上，我们将证明对 \(\mathbb{Z}^2\) 中所有 \((m,n)\)，命题 \((m+n,m-n)=(0,1)\) 都不成立。于是设 \((m,n)\in\mathbb{Z}^2\)，并假设 \((m+n,m-n)=(0,1)\)。则 \(m+n=0\) 且 \(m-n=1\)，所以

\[\begin{split}0&\equiv 2m\mod 2\\ &=(m-n)+(m+n)\\ &=1+0\\ &=1,\end{split}\]

矛盾。

本题最后一步可以用几种不同方式完成。假设 \(m+n=0\) 与 \(m-n=1\)（在整数中）显然矛盾，因此除了我这里给出的数值矛盾 \(0\equiv 1\mod 2\) 之外，你还可以用其他方式推出矛盾。

example : ¬ Bijective (fun ((m, n) : ℤ × ℤ) ↦ (m + n, m - n)) := by
  dsimp [Bijective, Injective, Surjective]
  push_neg
  right
  use (0, 1)
  intro (m, n) h
  dsimp at h
  obtain ⟨h1, h2⟩ := h
  have :=
  calc 0 ≡ 2 * m [ZMOD 2] := by extra
    _ = (m - n) + (m + n) := by ring
    _ = 1 + 0 := by rw [h1, h2]
    _ = 1 := by numbers
  numbers at this

8.4.4. 例

问题

考虑从 \(\mathbb{R}^2\) 到 \(\mathbb{R}^3\) 的函数 \((x,y)\mapsto (x+y,x-y,y)\)。证明这个函数是单射。

解答

设 \((x_1,y_1)\) 和 \((x_2,y_2)\) 为 \(\mathbb{R}^2\) 中的点，并假设

\[(x_1+y_1,x_1-y_1, y_1)=(x_2+y_2,x_2-y_2, y_2).\]

于是逐坐标观察可得

\[\begin{split}x_1+y_1&=x_2+y_2\\ x_1-y_1&=x_2-y_2\\ y_1&=y_2\end{split}\]

把第三个方程从第一个方程中减去，还可得 \(x_1=x_2\)。因此 \((x_1,y_1)=(x_2,y_2)\)。

在 Lean 中，请注意使用策略 constructor，把积类型等式的目标

⊢ (x1, y1) = (x2, y2)

化为两个较简单的目标，每个坐标一个：

⊢ x1 = x2
⊢ y1 = y2

这和用 obtain 处理积类型等式假设的情形一样（回忆例 8.4.1）：要点在于，积类型中的相等本质上就是关于第一坐标相等和第二坐标相等的“且”陈述。

example : Injective (fun ((x, y) : ℝ × ℝ) ↦ (x + y, x - y, y)) := by
  intro (x1, y1) (x2, y2) h
  dsimp at h
  obtain ⟨h, h', hy⟩ := h
  constructor
  · addarith [h, hy]
  · apply hy

8.4.5. 例

问题

考虑从 \(\mathbb{R}^2\) 到 \(\mathbb{R}\) 的函数 \((x,y)\mapsto x+y\)。证明这个函数是

非单射；
满射。

解答

1. 我们将证明存在 \(\mathbb{R}^2\) 中的点 \((x_1,y_1)\) 和 \((x_2,y_2)\)，使得 \(x_1+y_1=x_2+y_2\) 且 \((x_1,y_1)\ne (x_2,y_2)\)。确实，考虑点 \((0,0)\) 与 \((1,-1)\)。有 \(0+0=1+(-1)\)，并且 \((0,0)\ne (1,-1)\)。

2. 设 \(a\) 为实数。我们必须证明存在 \(\mathbb{R}^2\) 中的点 \((x,y)\)，使得 \(x+y=a\)。确实，\(a+0=a\)，所以 \((a,0)\) 具有这个性质。

example : ¬ Injective (fun ((x, y) : ℝ × ℝ) ↦ x + y) := by
  dsimp [Injective]
  push_neg
  use (0, 0), (1, -1)
  dsimp
  constructor
  · numbers
  · numbers

example : Surjective (fun ((x, y) : ℝ × ℝ) ↦ x + y) := by
  intro a
  use (a, 0)
  dsimp
  ring

8.4.6. 例

问题

考虑从 \(\mathbb{Z}^2\) 到 \(\mathbb{Z}\) 的函数 \((m,n)\mapsto 5m+8n\)。证明这个函数是

非单射；
满射。

解答

1. 我们将证明存在 \(\mathbb{Z}^2\) 中的数对 \((m_1,n_1)\) 和 \((m_2,n_2)\)，使得 \(5m_1+8n_1=5m_2+8n_2\) 且 \((m_1,n_1)\ne (m_2,n_2)\)。确实，考虑数对 \((0,0)\) 与 \((8,-5)\)。有 \(5\cdot 0+8\cdot 0=5\cdot 8+8\cdot (-5)\)，并且 \((0,0)\ne (8,-5)\)。

2. 设 \(a\) 为整数。我们必须证明存在 \(\mathbb{Z}^2\) 中的数对 \((m,n)\)，使得 \(5m+8n=a\)。确实，\(5(-3a)+8(2a)=a\)，所以 \((-3a,2a)\) 具有这个性质。

在这个证明的第二部分中，-3 和 2 是从哪里来的？请与例 3.5.1 和例 3.5.3 比较。

example : ¬ Injective (fun ((m, n) : ℤ × ℤ) ↦ 5 * m + 8 * n) := by
  dsimp [Injective]
  push_neg
  use (0, 0), (8, -5)
  constructor
  · numbers
  · numbers

example : Surjective (fun ((m, n) : ℤ × ℤ) ↦ 5 * m + 8 * n) := by
  intro a
  use (-3 * a, 2 * a)
  dsimp
  ring

8.4.7. 例

问题

考虑从 \(\mathbb{Z}^2\) 到 \(\mathbb{Z}\) 的函数 \((m,n)\mapsto 5m+10n\)。证明这个函数是

非单射；
非满射。

非单射性的证明留作练习；它与前两个问题中的证明类似。

解答

（非满射性）我们将证明存在整数 \(x\)，使得对所有整数数对 \((m,n)\)，都有 \(5m+10n\ne x\)。确实，我们证明 1 具有这个性质。设 \((m,n)\) 为一对整数，并假设 \(5m+10n=1\)。则

\[\begin{split}0 &\equiv 5(m+2n)\mod 5\\ &=5m+10n\\ &=1,\end{split}\]

矛盾。

example : ¬ Injective (fun ((m, n) : ℤ × ℤ) ↦ 5 * m + 10 * n) := by
  sorry

example : ¬ Surjective (fun ((m, n) : ℤ × ℤ) ↦ 5 * m + 10 * n) := by
  dsimp [Surjective]
  push_neg
  use 1
  intro (m, n) h
  dsimp at h
  have :=
  calc 0 ≡ 5 * (m + 2 * n) [ZMOD 5] := by extra
    _ = 5 * m + 10 * n := by ring
    _ = 1 := h
  numbers at this

8.4.8. 例

问题

考虑函数 \(g:\mathbb{R}^2\to \mathbb{R}^2\)，定义为 \(g(x,y)=(y,x)\)。证明 \(g\circ g=\operatorname{Id}_\mathbb{R}\)。

解答

设 \((x,y)\) 为 \(\mathbb{R}^2\) 中的点。则

\[\begin{split}g(g(x,y))&=g(y,x)\\ &=(x,y).\end{split}\]

def g : ℝ × ℝ → ℝ × ℝ
  | (x, y) => (y, x)

example : g ∘ g = id := by
  ext ⟨x, y⟩
  dsimp [g]

8.4.9. 例

定理

存在一个从 \(\mathbb{N}^2\) 到 \(\mathbb{N}\) 的双射。

先回忆例 6.2.4 中的数列 \(A_n\)；我们证明关于它的一个引理。

def A : ℕ → ℕ
  | 0 => 0
  | n + 1 => A n + n + 1

theorem A_mono {n m : ℕ} (h : n ≤ m) : A n ≤ A m := by
  induction_from_starting_point m, h with k hk IH
  · extra
  · calc A n ≤ A k := IH
      _ ≤ A k + (k + 1) := by extra
      _ = A k + k + 1 := by ring
      _ = A (k + 1) := by rw [A]

还有一个更困难的推论。

theorem of_A_add_mono {a1 a2 b1 b2 : ℕ} (h : A (a1 + b1) + b1 ≤ A (a2 + b2) + b2) :
    a1 + b1 ≤ a2 + b2 := by
  obtain h' | h' : _ ∨ a2 + b2 + 1 ≤ a1 + b1 := le_or_lt (a1 + b1) (a2 + b2)
  · apply h'
  rw [← not_lt] at h
  have :=
  calc A (a2 + b2) + b2
     < A (a2 + b2) + b2 + (a2 + 1) := by extra
    _ = A (a2 + b2) + (a2 + b2) + 1 := by ring
    _ = A ((a2 + b2) + 1) := by rw [A]
    _ = A (a2 + b2 + 1) := by ring
    _ ≤ A (a1 + b1) := A_mono h'
    _ ≤ A (a1 + b1) + b1 := by extra
  contradiction

我们用数列 \(A_n\) 定义函数 \(p:\mathbb{N}^2\to \mathbb{N}\)，它将是我们要找的双射：\(p(a,b)=A_{a+b}+b\)。

def p : ℕ × ℕ → ℕ
  | (a, b) => A (a + b) + b

最后证明这个函数 \(p\) 确实是双射。我们为 \(p\) 设置一个“交织”映射 \(i\)，并调用第 8.1 节练习中证明的引理 surjective_of_intertwining。

def i : ℕ × ℕ → ℕ × ℕ
  | (0, b) => (b + 1, 0)
  | (a + 1, b) => (a, b + 1)

theorem p_comp_i (x : ℕ × ℕ) : p (i x) = p x + 1 := by
  match x with
  | (0, b) =>
    calc p (i (0, b)) = p (b + 1, 0) := by rw [i]
      _ = A ((b + 1) + 0) + 0 := by dsimp [p]
      _ = A (b + 1) := by ring
      _ = A b + b + 1 := by rw [A]
      _ = (A (0 + b) + b) + 1 := by ring
      _ = p (0, b) + 1 := by dsimp [p]
  | (a + 1, b) =>
    calc p (i (a + 1, b)) = p (a, b + 1) := by rw [i] ; rfl -- FIXME
      _ = A (a + (b + 1)) + (b + 1) := by dsimp [p]
      _ = (A ((a + 1) + b) + b) + 1 := by ring
      _ = p (a + 1, b) + 1 := by rw [p]

example : Bijective p := by
  constructor
  · intro (a1, b1) (a2, b2) hab
    dsimp [p] at hab
    have H : a1 + b1 = a2 + b2
    · apply le_antisymm
      · apply of_A_add_mono
        rw [hab]
      · apply of_A_add_mono
        rw [hab]
    have hb : b1 = b2
    · zify at hab ⊢
      calc (b1:ℤ) = A (a2 + b2) + b2 - A (a1 + b1) := by addarith [hab]
        _ = A (a2 + b2) + b2 - A (a2 + b2) := by rw [H]
        _ = b2 := by ring
    constructor
    · zify at hb H ⊢
      addarith [H, hb]
    · apply hb
  · apply surjective_of_intertwining (x0 := (0, 0)) (i := i)
    · calc p (0, 0) = A (0 + 0) + 0 := by dsimp [p]
        _ = A 0 := by ring
        _ = 0 := by rw [A]
    · intro x
      apply p_comp_i

8.4.10. 练习

考虑从 \(\mathbb{Q}^2\) 到 \(\mathbb{Q}^2\) 的函数 \((r,s)\mapsto (s,r-s)\)。证明这个函数是双射。

example : Bijective (fun ((r, s) : ℚ × ℚ) ↦ (s, r - s)) := by
  rw [bijective_iff_exists_inverse]
  sorry

考虑从 \(\mathbb{Z}^2\) 到 \(\mathbb{Z}\) 的函数 \((x,y)\mapsto x-2y-1\)。证明这个函数非单射且满射。

非单射；
满射。

example : ¬ Injective (fun ((x, y) : ℤ × ℤ) ↦ x - 2 * y - 1) := by
  sorry

example : Surjective (fun ((x, y) : ℤ × ℤ) ↦ x - 2 * y - 1) := by
  sorry

考虑从 \(\mathbb{Q}^2\) 到 \(\mathbb{Q}\) 的函数 \((x,y)\mapsto x^2+y^2\)。证明这个函数不是满射。
```
example : ¬ Surjective (fun ((x, y) : ℚ × ℚ) ↦ x ^ 2 + y ^ 2) := by
  sorry
```
考虑从 \(\mathbb{Q}^2\) 到 \(\mathbb{Q}\) 的函数 \((x,y)\mapsto x^2-y^2\)。证明这个函数是满射。
```
example : Surjective (fun ((x, y) : ℚ × ℚ) ↦ x ^ 2 - y ^ 2) := by
  sorry
```
考虑从 \(\mathbb{Q}\times \mathbb{N}\) 到 \(\mathbb{Q}\) 的函数 \((a,b)\mapsto a^b\)。证明这个函数是满射。
```
example : Surjective (fun ((a, b) : ℚ × ℕ) ↦ a ^ b) := by
  sorry
```

考虑从 \(\mathbb{R}^3\) 到 \(\mathbb{R}^2\) 的函数 \((x,y,z)\mapsto (x+y+z,x+2y+3z)\)。证明这个函数不是单射。

example : ¬ Injective
    (fun ((x, y, z) : ℝ × ℝ × ℝ) ↦ (x + y + z, x + 2 * y + 3 * z)) := by
  sorry

考虑从 \(\mathbb{R}^2\) 到 \(\mathbb{R}^3\) 的函数 \((x,y)\mapsto (x+y,x+2y,x+3y)\)。证明这个函数是单射。

example : Injective (fun ((x, y) : ℝ × ℝ) ↦ (x + y, x + 2 * y, x + 3 * y)) := by
  sorry

考虑函数 \(h:\mathbb{R}^3\to \mathbb{R}^3\)，定义为 \(h(x,y,z)=(y,z,x)\)。证明 \(h\circ h\circ h=\operatorname{Id}_\mathbb{R}\)。

def h : ℝ × ℝ × ℝ → ℝ × ℝ × ℝ
  | (x, y, z) => (y, z, x)

example : h ∘ h ∘ h = id := by
  sorry