函数与映射

Introduction

函数是数学最基本的概念之一。这一课我们学习 Lean 中函数性质的描述方法。给定函数 `f : α → β`： - **单射 (injective)**：不同输入给不同输出。`∀ x y, f x = f y → x = y` - **满射 (surjective)**：β 中每个元素都是某个输入的像。`∀ y, ∃ x, f x = y` - **双射 (bijective)**：既是单射又是满射。本关目标：如果 `f` 和 `g` 都是单射，那么它们的复合 `f ∘ g` 也是单射。 `f ∘ g` 的定义：`(f ∘ g) x = f (g x)`。在 Lean 中用 `Function.comp` 或 `.∘` 表示。

本关学到的新东西

策略 (Tactics)

have引入一个中间结论：`have h : P := ...` 给证明分支起个名字

概念 (Concepts)

Injective单射：f x = f y → x = y。不同输入不能有相同输出

Surjective满射：∀ y, ∃ x, f x = y。值域覆盖整个目标类型

f ∘ g (复合)(f ∘ g) x = f (g x)。先应用 g，再应用 f

证明目标

当前目标

f : β → γ

g : α → β

⊢Injective g → Injective f → Injective (f ∘ g)

分步提示

1.先引入两个前提：`intro hg`（g 是单射）和 `intro hf`（f 是单射）。
2.现在要证明 `Injective (f ∘ g)`。Injective 的定义需要展开：`Injective h` 就是 `∀ x y, h x = h y → x = y`。所以继续 `intro x y` 和 `intro h`。
3.`h` 是 `(f ∘ g) x = (f ∘ g) y`。根据 ∘ 的定义，这等于 `f (g x) = f (g y)`。用 `simp [Function.comp] at h` 或直接使用 `h`。
4.现在 `hf : Injective f` 告诉我们：`f a = f b → a = b`。h 给了 `f (g x) = f (g y)`，所以 `apply hf at h` 得到 `g x = g y`。
5.再 `apply hg at h`，得到 `x = y`。这就是目标！用 `exact h`。

怎么玩：编辑器里有预写代码。直接点 运行 ▶ 看效果，或修改代码后运行。卡住了看左侧的提示。

Lean 代码编辑器