Mathlib 的分析库以 Filter 为核心抽象，在此之上叠加拓扑、度量和赋范结构，统一表达极限、连续、收敛等概念。理解这套分层设计，是读懂 Mathlib 分析证明的前提。本篇梳理 Filter、TopologicalSpace、MetricSpace 和 NormedSpace 四层结构的定义方式和证明惯用法，并通过具体可运行代码展示各层之间的关联。

前置阅读：本系列 09 Mathlib 搜索技巧、10 类型类层次、11 在 Mathlib 上证一个小定理。

Filter：分析库的基础抽象

为什么不直接用 ε-δ

经典分析教材用 ε-δ 定义极限：对每个 ε > 0，存在 δ > 0，使得……这个定义能精确刻画单个极限，但在证明库里它有两个缺陷。第一，同一个"极限"概念在不同情形（趋向实数点、趋向无穷、序列极限、网极限）下需要写出形状不同的 ε-δ 公式，导致同一条定理（如极限的线性性）在每种情形下各需一个版本。第二，组合两个极限结论时，条件匹配需要手动传递 ε/2 技巧，证明文本冗长。

Mathlib 选择用 Filter 把"趋向某处"的结构抽象出来，让极限定理写一次、对所有情形都成立。这是一个典型的"一次抽象、多次复用"的库设计取舍。

Filter 的定义

Filter 是集合的集合，满足三个条件：包含全集、对上集封闭、对有限交封闭。

1
2
3
4
5
6
7
8
9
10
11
12
import Mathlib.Order.Filter.Basic

-- Filter 定义（简化版，对照 Mathlib 源码）
-- structure Filter (α : Type*) where
--   sets        : Set (Set α)
--   univ_sets   : Set.univ ∈ sets
--   sets_of_superset : ∀ {x y}, x ∈ sets → x ⊆ y → y ∈ sets
--   inter_sets  : ∀ {x y}, x ∈ sets → y ∈ sets → x ∩ y ∈ sets

#check Filter          -- Filter : Type u_1 → Type u_1
#check Filter.atTop    -- Filter.atTop : Filter ℕ  (或其他有序类型)
#check Filter.nhds     -- Filter.nhds : α → Filter α

直觉上，Filter 表示"足够靠近某处的集合族"。nhds x 收集 x 的所有邻域；Filter.atTop 收集"从某点之后的所有集合"，即"充分大"的集族；Filter.atBot 是对偶的"充分小"。

Filter.Eventually

Filter.Eventually p f 表示命题 p 在滤子 f 下"最终成立"，即存在 f 中的某个集合 s，使得 p 在 s 上对所有点成立。

1
2
3
4
5
6
7
8
9
10
import Mathlib.Order.Filter.Basic

-- Eventually 的语义
-- def Filter.Eventually (p : α → Prop) (f : Filter α) : Prop :=
--   {x | p x} ∈ f

example : Filter.Eventually (fun n : ℕ => n ≥ 5) Filter.atTop := by
  -- 需要找到某个 N，使得 n ≥ N 蕴含 n ≥ 5
  simp [Filter.Eventually, Filter.atTop]
  exact ⟨5, fun n hn => hn⟩

在 atTop 滤子下，Eventually p atTop 等价于"存在 N，使得对所有 n ≥ N，p n 成立"，即通常意义上的"最终成立"。在 nhds x 下，Eventually p (nhds x) 等价于"存在 x 的邻域 U，使得 p 在 U 上成立"。

这个统一化的"Eventually"是 Mathlib 分析证明的高频词汇，在极限定理的陈述和证明中随处可见。

Filter.Tendsto

Filter.Tendsto f l₁ l₂ 表示函数 f 把滤子 l₁ 映射到 l₂ 之下，即 l₁ 的像包含在 l₂ 中，形式上等价于 ∀ s ∈ l₂, f ⁻¹' s ∈ l₁。

1
2
3
4
5
6
7
8
9
10
11
12
import Mathlib.Topology.Basic

-- Tendsto 的类型签名
#check @Filter.Tendsto
-- Filter.Tendsto : (α → β) → Filter α → Filter β → Prop

-- 序列极限：n → ∞ 时 1/n → 0
-- Filter.Tendsto (fun n : ℕ => 1 / (n : ℝ)) Filter.atTop (nhds 0)

-- 常值函数极限：在任意滤子下趋向常值
#check tendsto_const_nhds
-- tendsto_const_nhds : Filter.Tendsto (fun _ => b) f (nhds b)

常见的极限表达式全都归结为 Tendsto 的不同实例：

分析概念 Tendsto 写法
lim_{x→a} f(x) = L Tendsto f (nhds a) (nhds L)
lim_{n→∞} aₙ = L Tendsto a atTop (nhds L)
f(x) → +∞ 当 x → ∞ Tendsto f atTop atTop
f(x) → L 当 x → a⁻ Tendsto f (nhds[<] a) (nhds L)

这个统一框架使得"极限的复合"（如 Tendsto.comp）只需一条定理，覆盖所有上述情形。

TopologicalSpace：拓扑结构

类型类定义

TopologicalSpace 是 Lean 的类型类（typeclass），定义了开集概念，以及开集对任意并和有限交的封闭性。

1
2
3
4
5
6
7
8
9
10
11
12
import Mathlib.Topology.Basic

-- TopologicalSpace 类型类（简化结构）
-- class TopologicalSpace (α : Type u) where
--   IsOpen       : Set α → Prop
--   isOpen_univ  : IsOpen Set.univ
--   isOpen_inter : ∀ s t, IsOpen s → IsOpen t → IsOpen (s ∩ t)
--   isOpen_sUnion : ∀ s, (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)

#check @IsOpen            -- IsOpen : TopologicalSpace α → Set α → Prop
#check @IsOpen.inter      -- isOpen_inter
#check @ContinuousAt      -- ContinuousAt : (α → β) → α → Prop

Lean 通过 typeclass 机制自动传递 TopologicalSpace 实例，因此在任何已声明拓扑结构的类型上，IsOpen、nhds、ContinuousAt 等都直接可用，无需手动传递结构。

nhds 和邻域滤子

nhds x 返回点 x 的邻域滤子，是 TopologicalSpace 和 Filter 的衔接点。

1
2
3
4
5
6
7
8
9
10
import Mathlib.Topology.Basic

variable {α : Type*} [TopologicalSpace α] (x : α)

#check nhds x           -- nhds x : Filter α
#check mem_nhds_iff     -- 邻域刻画：s ∈ nhds x ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t

-- 连续性用 Tendsto 在 nhds 之间刻画
-- ContinuousAt f x := Tendsto f (nhds x) (nhds (f x))
#check continuousAt_iff_tendsto  -- 连续与 Tendsto 等价

这个等价关系说明，TopologicalSpace 不是独立于 Filter 的另一套语言，而是在 Filter 上增加了"开集"概念后的扩展。连续性、紧致性、Hausdorff 分离公理等所有拓扑概念，最终都可以用 Filter 的语言重新陈述。

连续性 tactic

Mathlib 提供 continuity tactic，自动搜索并组合连续性引理来关闭 Continuous f 或 ContinuousAt f x 形式的目标。

1
2
3
4
5
6
7
8
9
10
import Mathlib.Topology.Algebra.Order.IntermediateValue

example : Continuous (fun x : ℝ => x ^ 2 + 3 * x + 1) := by
  continuity
  -- continuity 通过 Continuous.add, Continuous.mul, continuous_const 等
  -- 引理自动分解并关闭目标

-- 如果 continuity 失败，可以手动展开后用 fun_prop
example : Continuous (fun x : ℝ => Real.exp x + x) := by
  fun_prop

fun_prop 是更广泛的"函数性质"自动化 tactic，覆盖连续、可测、Lipschitz 等性质，在 Mathlib 较新版本中逐步取代部分 continuity 的用例。

MetricSpace：度量结构

类型类层次

MetricSpace 在 TopologicalSpace 之上增加了距离函数 dist : α → α → ℝ，满足非负性、同一性、对称性和三角不等式。Mathlib 用 typeclass 继承把两者联系起来：MetricSpace 实例自动生成对应的 TopologicalSpace 实例，其开集由 ε-球生成。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
import Mathlib.Topology.MetricSpace.Basic

-- MetricSpace 实例自动提供 TopologicalSpace
-- instance MetricSpace.toTopologicalSpace [MetricSpace α] : TopologicalSpace α

variable {α : Type*} [MetricSpace α] (x y : α)

#check dist x y         -- dist x y : ℝ
#check dist_nonneg      -- dist_nonneg : 0 ≤ dist x y
#check dist_comm        -- dist_comm : dist x y = dist y x
#check dist_triangle    -- dist_triangle : dist x z ≤ dist x y + dist y z

-- 在度量空间中，nhds x 等价于以 ε-球为基的滤子
#check Metric.nhds_basis_ball
-- nhds x = ⨅ ε > 0, 𝓟 (Metric.ball x ε)

-- Tendsto 在度量空间中退化为 ε-δ 定义
#check Metric.tendsto_nhds  -- Tendsto f (nhds x) (nhds L) ↔ ε-δ

Metric.tendsto_nhds 定理表明，在 MetricSpace 中，Filter.Tendsto f (nhds x) (nhds L) 与教材中的 ε-δ 定义等价。这说明滤子层次不是用来替代 ε-δ，而是让 ε-δ 成为更通用框架的一个具体实例，从而在抽象层可以复用更多定理。

基本极限证明示例

tendsto_const_nhds 是最简单的收敛证明起点，常值序列在任意滤子下都收敛到该常值：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
import Mathlib.Topology.Basic
import Mathlib.Order.Filter.Basic

-- tendsto_const_nhds：常值函数在任意滤子下趋向该常值
#check @tendsto_const_nhds
-- tendsto_const_nhds : Filter.Tendsto (fun _ => b) f (nhds b)

-- 证明：常值序列收敛
theorem const_seq_tendsto (b : ℝ) :
    Filter.Tendsto (fun _ : ℕ => b) Filter.atTop (nhds b) :=
  tendsto_const_nhds

-- term mode 版本（直接给出证明项）：
theorem const_seq_tendsto' (b : ℝ) :
    Filter.Tendsto (fun _ : ℕ => b) Filter.atTop (nhds b) :=
  tendsto_const_nhds

-- tactic mode 版本（更清晰地展示证明结构）：
theorem const_seq_tendsto_tac (b : ℝ) :
    Filter.Tendsto (fun _ : ℕ => b) Filter.atTop (nhds b) := by
  exact tendsto_const_nhds
  -- InfoView 在 exact 之前显示：
  -- ⊢ Filter.Tendsto (fun _ => b) Filter.atTop (nhds b)

这里 term mode 和 tactic mode 给出完全等价的证明，区别仅在表达形式。term mode 更简洁；tactic mode 在证明较复杂时允许逐步查看 InfoView 状态，便于调试。

更复杂的极限：两个极限的和

1
2
3
4
5
6
7
8
9
10
11
12
13
14
import Mathlib.Topology.Algebra.Order.LiminfLimsup
import Mathlib.Topology.Algebra.InfiniteSum.Basic

-- Filter.Tendsto 关于加法的稳定性
#check Filter.Tendsto.add
-- Tendsto.add : Tendsto f l (nhds a) → Tendsto g l (nhds b)
--             → Tendsto (fun x => f x + g x) l (nhds (a + b))

-- 证明：两个收敛序列的和收敛
theorem sum_tendsto (f g : ℕ → ℝ) (a b : ℝ)
    (hf : Filter.Tendsto f Filter.atTop (nhds a))
    (hg : Filter.Tendsto g Filter.atTop (nhds b)) :
    Filter.Tendsto (fun n => f n + g n) Filter.atTop (nhds (a + b)) :=
  hf.add hg

hf.add hg 使用点记法调用 Filter.Tendsto.add，直接从两个收敛假设得到和的收敛，无需展开任何 ε-δ 细节。这正是滤子框架的设计意图：极限的代数运算在抽象层一次处理，具体空间（ℝ、ℂ、赋范空间）自动继承。

NormedSpace：赋范结构

类型类层次

Mathlib 把赋范结构拆分为多个类型类，形成细粒度的层次：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
import Mathlib.Analysis.Normed.Group.Basic

-- 赋范结构的类型类层次（简化）
-- NormedAddCommGroup α：提供 ‖·‖，满足 ‖x‖ = 0 ↔ x = 0 和三角不等式
-- NormedSpace 𝕜 α：在 𝕜 上的赋范向量空间，‖c • x‖ = ‖c‖ * ‖x‖

variable {α : Type*} [NormedAddCommGroup α] (x y : α)

#check ‖x‖               -- ‖x‖ : ℝ  （范数）
#check norm_nonneg x     -- norm_nonneg : 0 ≤ ‖x‖
#check norm_triangle x y -- norm_triangle : ‖x + y‖ ≤ ‖x‖ + ‖y‖
#check norm_zero         -- norm_zero : ‖(0 : α)‖ = 0

-- NormedAddCommGroup 自动提供 MetricSpace（通过 dist x y = ‖x - y‖）
-- 因此也自动提供 TopologicalSpace
#check NormedAddCommGroup.toMetricSpace

这个层次关系决定了，任何 NormedAddCommGroup 上的证明，都可以直接使用 MetricSpace 和 TopologicalSpace 的全部引理，无需额外声明。

gcongr 和不等式证明

分析证明中大量涉及不等式推导。gcongr tactic 处理单调性和同余不等式，可以在乘积、幂次、绝对值等位置自动传播不等式。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
import Mathlib.Tactic.GCongr

-- gcongr 示例：利用 a ≤ b 和 c ≤ d 推出 a + c ≤ b + d
example (a b c d : ℝ) (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by
  gcongr

-- gcongr 处理乘积
example (a b c : ℝ) (ha : 0 ≤ a) (h : b ≤ c) : a * b ≤ a * c := by
  gcongr

-- 在范数不等式中使用 gcongr
example {α : Type*} [NormedAddCommGroup α] (x y z : α)
    (h : ‖y - z‖ ≤ 1) : ‖x + y - (x + z)‖ ≤ 1 := by
  simp only [add_sub_add_left_eq_sub]
  exact h

gcongr 特别适合处理"把大不等式拆成小不等式"的步骤，在分析证明里可以省去大量手动 linarith 或 nlinarith 调用。

measurability tactic

可测性（Measurable f、AEMeasurable f）是积分论的前提。measurability tactic 类似于 continuity，通过自动组合可测性引理关闭目标。

1
2
3
4
5
6
7
8
9
10
11
12
import Mathlib.MeasureTheory.Measurable.Basic

-- 可测性自动化
example : Measurable (fun x : ℝ => x ^ 2 + 1) := by
  measurability

-- 组合可测函数
example {α : Type*} [MeasurableSpace α]
    (f g : α → ℝ) (hf : Measurable f) (hg : Measurable g) :
    Measurable (fun x => f x + g x) := by
  exact hf.add hg
  -- 或者：measurability（能自动感知 hf 和 hg）

InfoView 的使用

在分析证明中，InfoView 的价值在于实时显示类型类实例和滤子状态。将光标放在某个 #check 或 tactic 上，InfoView 显示当前推断的类型和约束：

1
2
3
4
5
6
7
8
9
10
11
12
13
import Mathlib.Analysis.SpecificLimits.Basic

-- 光标放在 #check 上，InfoView 显示完整类型
#check Real.tendsto_pow_atTop_atTop_of_one_lt
-- Real.tendsto_pow_atTop_atTop_of_one_lt :
--   1 < r → Filter.Tendsto (fun n => r ^ n) Filter.atTop Filter.atTop

-- 光标放在 tactic 之间，InfoView 显示当前 proof state
example : Filter.Tendsto (fun n : ℕ => (2 : ℝ) ^ n) Filter.atTop Filter.atTop := by
  -- InfoView: ⊢ Filter.Tendsto (fun n => 2 ^ n) atTop atTop
  apply Real.tendsto_pow_atTop_atTop_of_one_lt
  -- InfoView: ⊢ 1 < 2
  norm_num

#check 在文件的任意位置都可使用，适合探索 Mathlib 中不熟悉的引理类型；InfoView 在 tactic 序列中提供逐步状态，两者配合是调试分析证明的标准方式。

term mode 与 tactic mode 的分工

分析证明通常在两种模式之间切换：结构清晰、引理直接适用时用 term mode；需要逐步分解目标、检查中间状态时用 tactic mode。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
import Mathlib.Topology.Basic
import Mathlib.Analysis.SpecificLimits.Basic

-- term mode：把证明写成函数应用链
theorem tendsto_example_term :
    Filter.Tendsto (fun n : ℕ => (1 : ℝ) / n) Filter.atTop (nhds 0) :=
  tendsto_const_div_atTop_nhds_0_nat 1

-- tactic mode：逐步分解，InfoView 辅助调试
theorem tendsto_example_tac :
    Filter.Tendsto (fun n : ℕ => (1 : ℝ) / n) Filter.atTop (nhds 0) := by
  have h : Filter.Tendsto (fun n : ℕ => (1 : ℝ) / n) Filter.atTop (nhds 0) :=
    tendsto_const_div_atTop_nhds_0_nat 1
  exact h

两种模式在证明核里完全等价，区别在于书写体验和调试便利性。较长的分析证明通常先在 tactic mode 中探索，再在确认正确后部分改写为 term mode，使文件更紧凑。

类型类继承链小结

Mathlib 分析库的四层结构形成一条清晰的继承链：

1
2
3
4
5
Filter (基础抽象)
  └── TopologicalSpace (开集 / 邻域 / 连续)
        └── MetricSpace  (dist / ε-球 / ε-δ)
              └── NormedAddCommGroup (‖·‖ / 赋范向量空间)
                    └── NormedSpace 𝕜 α (数乘兼容)

每一层都通过 typeclass 实例自动向下提供上层的全部能力。因此，在 NormedSpace 上工作时，Filter.Tendsto、ContinuousAt、Metric.ball 全部可用，无需重复声明。gcongr、continuity、measurability 等 tactic 也在各自适用的层次上自动工作，不要求手动选择对应引理。

练习 1：验证 nhds 和 Metric.ball 的关系

在 MetricSpace ℝ 中，用 Metric.mem_ball 和 mem_nhds_iff 手动证明：

1
2
3
4
5
-- 目标：∀ ε > 0, Metric.ball x ε ∈ nhds x
example {x : ℝ} {ε : ℝ} (hε : 0 < ε) : Metric.ball x ε ∈ nhds x := by
  rw [Metric.mem_nhds_iff]
  exact ⟨ε, hε, Metric.ball_subset_ball le_rfl⟩
  -- 提示：也可以直接用 Metric.ball_mem_nhds

练习 2：用 Filter.Tendsto 证明序列极限

证明序列 aₙ = n / (n + 1) 在 n → ∞ 时趋向 1。提示：可以先搜索 tendsto_div_atTop 或分解为两个 Tendsto 的商。

1
2
3
4
-- 框架
theorem seq_tendsto_one :
    Filter.Tendsto (fun n : ℕ => (n : ℝ) / (n + 1)) Filter.atTop (nhds 1) := by
  sorry  -- 展开后用 Tendsto.congr 和已知极限拼装

练习 3：gcongr 在范数不等式中的应用

给定 ‖f n - L‖ ≤ 1/n（对所有 n ≥ 1），用 gcongr 和 linarith 组合证明 ‖f n - L‖ ≤ 1（当 n ≥ 1 时）：

1
2
3
4
5
example (f : ℕ → ℝ) (L : ℝ) (n : ℕ) (hn : 1 ≤ n)
    (h : ‖f n - L‖ ≤ 1 / n) : ‖f n - L‖ ≤ 1 := by
  calc ‖f n - L‖ ≤ 1 / n := h
    _ ≤ 1 / 1 := by gcongr; exact_mod_cast hn
    _ = 1 := by norm_num

参考资料

  • Mathlib4 文档：Filter、TopologicalSpace、MetricSpace
  • Mathematics in Lean（MIL）第 9–10 章：Topology 和 Metric Spaces
  • Heather Macbeth，The Mechanics of Proof，Chapter 8：Limits and Continuity in Lean
  • 本系列 09 Mathlib 搜索技巧：exact?、apply?、Mathlib.Search 的使用方法
  • 本系列 10 类型类层次：typeclass 继承和实例搜索机制