我的博客

Ch4 集合与函数 - 深度伴读

9分钟阅读

第4章 集合与函数 - 深度伴读

本章定位

本章进入集合论领域，核心概念：

  1. 类型 vs 集合的区别
  2. 集合操作（交、并、差、子集）
  3. ext 扩展性原理
  4. 像与原像
  5. Schroeder-Bernstein 定理（可选）

4.1 Sets

核心洞见

Lean 中，集合是类型的子集。Set α 是类型 α 的子集的类型。 与 ZF 集合论不同，sin ∈ cos 在 Lean 中无意义（类型错误）。

类型 vs 集合

ZF 集合论Lean 类型论
一切皆集合一切皆有类型
a ∈ b 对任意 a, b 有意义x ∈ s 要求 x : α, s : Set α
集合是基础类型是基础，集合是 α → Prop

Set α 的本质

-- Set α 实际上是 α → Prop
-- x ∈ s 实际上是 s x（s 对 x 的应用）
-- 这意味着"集合就是谓词"
 
-- 集合构建记号
{ y | P y }  =  fun y ↦ P y

基本集合操作

s ⊆ t    -- 子集：∀ {x}, x ∈ s → x ∈ t
s ∩ t    -- 交集：{x | x ∈ s ∧ x ∈ t}
s ∪ t    -- 并集：{x | x ∈ s ∨ x ∈ t}
s \ t    -- 差集：{x | x ∈ s ∧ x ∉ t}
∅        -- 空集：{x | False}
univ     -- 全集：{x | True}

证明集合等式：ext 战术

variable {α : Type*} (s t u : Set α)
 
-- mem_inter_iff : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t（交集的成员定义）
example : s ∩ t = t ∩ s := by
  ext x                      -- 扩展性：要证 s = t，证 ∀ x, x ∈ s ↔ x ∈ t
  simp only [mem_inter_iff]  -- 展开交集定义：目标变成 (x ∈ s ∧ x ∈ t) ↔ (x ∈ t ∧ x ∈ s)
  constructor
  · rintro ⟨xs, xt⟩; exact ⟨xt, xs⟩  -- ∧ 的交换
  · rintro ⟨xt, xs⟩; exact ⟨xs, xt⟩

ext 的直觉

扩展性原理：两个集合相等当且仅当它们有相同的元素。 ext x 把 s = t 变成 x ∈ s ↔ x ∈ t。

定义归约

-- 假设 s, t, u 是某类型 α 上的集合
example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  intro x xsu          -- 任取 x ∈ s ∩ u
  exact ⟨h xsu.1, xsu.2⟩  -- xsu.1 : x ∈ s, 用 h 得 x ∈ t; xsu.2 : x ∈ u
-- Lean 自动展开 ⊆ 和 ∩ 的定义

交集证明模式

-- 证明 x ∈ s ∩ t
constructor
· exact xs    -- 证明 x ∈ s
· exact xt    -- 证明 x ∈ t
 
-- 或用匿名构造器
⟨xs, xt⟩
 
-- 使用 x ∈ s ∩ t
hx.1    -- x ∈ s
hx.2    -- x ∈ t
rcases hx with ⟨xs, xt⟩

并集证明模式

-- 证明 x ∈ s ∪ t
left; exact xs    -- 证明 x ∈ s
right; exact xt   -- 证明 x ∈ t
 
-- 使用 x ∈ s ∪ t
rcases hx with xs | xt
· ...  -- 情况 x ∈ s
· ...  -- 情况 x ∈ t

差集证明模式

-- 证明 x ∈ s \ t
constructor
· exact xs    -- x ∈ s
· intro xt    -- 假设 x ∈ t
  contradiction
 
-- 使用 x ∈ s \ t
hx.1    -- x ∈ s
hx.2    -- x ∉ t

有界量词

-- ∀ x ∈ s, P x 是 ∀ x, x ∈ s → P x 的缩写
-- ∃ x ∈ s, P x 是 ∃ x, x ∈ s ∧ P x 的缩写
 
example (h₀ : ∀ x ∈ s, ¬Even x) (h₁ : ∀ x ∈ s, Prime x) : ∀ x ∈ s, ¬Even x ∧ Prime x := by
  intro x xs
  constructor
  · apply h₀ x xs
  · apply h₁ x xs

索引并集与交集

variable (A : ℕ → Set α)
 
⋃ i, A i    -- 索引并集：{x | ∃ i, x ∈ A i}
⋂ i, A i    -- 索引交集：{x | ∀ i, x ∈ A i}
 
-- 证明 x ∈ ⋃ i, A i
use i, xAi    -- 提供索引 i 和 x ∈ A i
 
-- 使用 x ∈ ⋃ i, A i
rcases hx with ⟨i, xAi⟩
 
-- 证明 x ∈ ⋂ i, A i
intro i       -- 对任意 i
exact xAi     -- 证明 x ∈ A i
 
-- 使用 x ∈ ⋂ i, A i
hx i          -- 对特定的 i

4.2 Functions

核心洞见

  • 原像 f ⁻¹' p：{x | f x ∈ p}（总是定义良好）
  • 像 f '' s：{y | ∃ x, x ∈ s ∧ f x = y}（涉及存在量词）

原像

variable {α β : Type*} (f : α → β) (p u v : Set β)
 
-- 原像的定义
f ⁻¹' p = {x | f x ∈ p}
 
-- 原像保持所有集合操作
example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by ext; rfl
example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v := by ext; rfl

为什么原像更好用

x ∈ f ⁻¹' t 直接展开为 f x ∈ t，不需要解包存在量词。

像

variable (s : Set α) (y : β)
 
-- 像的定义
f '' s = {y | ∃ x, x ∈ s ∧ f x = y}
 
-- 使用 y ∈ f '' s
rcases hy with ⟨x, xs, rfl⟩   -- x : α, xs : x ∈ s, rfl : f x = y（自动重写）
 
-- 证明 y ∈ f '' s
use x, xs                       -- 提供 x 和 x ∈ s

像与原像的 Galois 连接

variable (v : Set β)
 
example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v
-- 这是最重要的等价关系之一！
-- 右边通常更有用（不需要解包存在量词）

InjOn：局部单射

def InjOn f s := ∀ x₁ ∈ s, ∀ x₂ ∈ s, f x₁ = f x₂ → x₁ = x₂
-- f 在集合 s 上是单射的
 
-- Injective f ↔ InjOn f univ

range：值域

def range f := {x | ∃ y, f y = x}
-- range f = f '' univ
 
-- exp_pos : ∀ x, exp x > 0（指数函数的值恒正）
-- exp_log : y > 0 → exp (log y) = y（指数和对数互为反函数）
example : range exp = { y | y > 0 } := by
  ext y; constructor
  · rintro ⟨x, rfl⟩; apply exp_pos    -- exp x > 0，所以 y ∈ range exp ⇒ y > 0
  · intro ypos; use log y; rw [exp_log ypos]  -- 对 y > 0，取 x = log y，则 exp x = y

逆函数（经典逻辑）

noncomputable def inverse (f : α → β) : β → α := fun y ↦
  if h : ∃ x, f x = y then Classical.choose h else default
 
-- inverse_spec: f (inverse f y) = y（当存在 x 使 f x = y）

4.3 Schröder-Bernstein 定理（选读）

定理陈述

如果 f : α → β 和 g : β → α 都是单射，那么存在 h : α → β 是双射。

这个定理的证明比较复杂，但展示了 Lean 证明真实数学定理的能力。 如果你时间有限，可以跳过这一节。

本章核心 Tactic 总结

Tactic用途场景
ext扩展性证明集合等式
constructor分解 ∧, ↔交集、双蕴含
left/right选择析取分支并集
rcases解包 ∃, ∧像、交集
rintrointro + rcases复合模式
use提供见证像、存在
simp自动简化集合操作
rfl定义相等原像

本章练习策略

必做练习

  1. 集合等式：用 ext 证明 s ∩ t = t ∩ s
  2. 像与原像：证明 f '' s ⊆ v ↔ s ⊆ f ⁻¹' v
  3. Cantor 定理：理解对角线论证

练习技巧

遇到卡住的练习

  1. 先明确要证的是 ⊆ 还是 =
  2. ⊆ 用 intro x xs
  3. = 用 ext x
  4. 用 simp 或 dsimp 展开定义

预告：第5章会学到什么

第5章进入数论：

  • 整除 ∣
  • 素数 Prime
  • 归纳法 induction
  • omega 战术

自测问题

  1. Set α 的底层表示是什么？
  2. ext 做了什么？
  3. 像和原像哪个更好用？为什么？
  4. f '' s 的定义涉及什么逻辑联结词？

伴读文档 - 第4章完

关系图谱

反向链接