Analysis Trinity / 数学分析三位一体

Formal verification of three fundamental theorems of real analysis in Lean 4

实数完备性的三座丰碑 — Lean 4 形式化证明

Powered by Mathlib.

Nested Intervals · Bolzano-Weierstrass · Heine-Borel

区间套定理 · 聚点定理 · 有限覆盖定理

---

Overview / 概述

These three theorems are equivalent characterizations of the completeness of the real numbers — the property that distinguishes ℝ from ℚ. Each reveals a different facet of the same deep truth.

这三个定理是实数完备性的三种等价刻画——正是完备性将实数 ℝ 与有理数 ℚ 本质区分开来。每个定理都从不同角度揭示了同一个深刻事实。

Theorem / 定理	Statement / 陈述	Perspective / 视角
Nested Intervals	Shrinking nested closed intervals meet in exactly one point	Sequences & Limits
区间套定理	收缩的嵌套闭区间交于唯一一点	序列与极限
Bolzano-Weierstrass	Every bounded sequence has a convergent subsequence	Accumulation & Convergence
聚点定理	有界数列必有收敛子列	聚集与收敛
Heine-Borel	Every open cover of [a, b] has a finite subcover	Compactness & Covering
有限覆盖定理	闭区间的任意开覆盖都有有限子覆盖	紧性与覆盖

They form a logical cycle, each implying the next:

三者构成逻辑闭环，彼此等价：

    Completeness of ℝ / 实数完备性 (LUB)
                 │
                 ▼
      Monotone Convergence / 单调收敛定理
                 │
     ┌───────────┴───────────┐
     ▼                       ▼
 ① Nested              Cauchy
   Intervals           Completeness
   区间套定理          柯西收敛原理
     │
     ▼
 ② Bolzano-Weierstrass / 聚点定理
     │
     ▼
 ③ Heine-Borel / 有限覆盖定理
     │
     └──────── ▶ ① ───┘  (cycle / 循环)

Proof Architecture / 证明架构

① Nested Intervals Theorem / 区间套定理 (NestedIntervals.lean)

The most detailed proof, built from first principles on ℝ.

从实数第一性原理出发，展开最详细的证明：

1. Cross Inequality / 交叉不等式 — ∀ m n, aₘ ≤ bₙ（对 m ≤ n 分类讨论）
2. Monotone Convergence / 单调收敛 — aₙ → ⨆ aₙ, bₙ → ⨅ bₙ via tendsto_atTop_ciSup/ciInf
3. Limit Uniqueness / 极限唯一性 — bₙ - aₙ → 0 迫使 ⨆ aₙ = ⨅ bₙ（tendsto_nhds_unique）
4. Existence & Uniqueness / 存在与唯一 — le_antisymm + ciSup_le + le_ciInf

② Bolzano-Weierstrass Theorem / 聚点定理 (BolzanoWeierstrass.lean)

Two formulations / 两种形式：

• Interval form / 区间形式: bounded sequence in [a, b] → convergent subsequence in [a, b]
• General form / 一般形式: sequence with bounded range → convergent subsequence

Key path / 关键路径: ProperSpace ℝ → IsCompact.isBounded → tendsto_subseq_of_bounded

Also includes the Infinite Pigeonhole Principle / 无穷鸽巢原理, foundation of the classical bisection argument (经典二分法的基础).

③ Heine-Borel Theorem / 有限覆盖定理 (HeineBorel.lean)

The logical chain connecting all three / 串联三大定理的逻辑链：

Bolzano-Weierstrass → IsSeqCompact [a,b] → IsCompact [a,b] → finite subcover
聚点定理            → 序列紧           → 紧             → 有限子覆盖

Plus the full Heine-Borel characterization / Heine-Borel 特征定理 for ℝ:

IsCompact s ↔ IsClosed s ∧ IsBounded s

紧致 ⟺ 闭且有界

And three classical applications / 三个经典应用：

• Heine-Cantor / 一致连续性定理: continuous on [a,b] → uniformly continuous（连续 → 一致连续）
• Boundedness / 有界性定理: continuous on [a,b] → bounded（连续 → 有界）
• Extreme Value Theorem / 最值定理: continuous on [a,b] → attains maximum（连续 → 取最大值）

Building / 构建

Prerequisites / 前置要求

• elan (Lean version manager / Lean 版本管理器)

Build / 编译

git clone https://github.com/L0stInFades/AnalysisTrinity.git
cd AnalysisTrinity
lake exe cache get    # download prebuilt Mathlib / 下载 Mathlib 预编译缓存 (~8000 files)
lake build            # verify all proofs / 验证所有证明

Project Structure / 项目结构

AnalysisTrinity/
├── lakefile.toml                          # build configuration / 构建配置
├── lean-toolchain                         # Lean version / Lean 版本
├── AnalysisTrinity.lean                   # root import / 根导入
└── AnalysisTrinity/
    ├── NestedIntervals.lean               # 区间套定理 / Nested Intervals
    ├── BolzanoWeierstrass.lean            # 聚点定理 / Bolzano-Weierstrass
    └── HeineBorel.lean                    # 有限覆盖定理 / Heine-Borel

Mathlib Dependency / Mathlib 依赖

This project builds on Mathlib4, using:

本项目基于 Mathlib4 构建，使用了以下模块：

• Mathlib.Topology.Order.MonotoneConvergence — monotone convergence in ordered spaces / 序空间中的单调收敛
• Mathlib.Topology.MetricSpace.Sequences — Bolzano-Weierstrass for proper metric spaces / ProperSpace 上的聚点定理
• Mathlib.Topology.Compactness.Compact — compactness and finite subcovers / 紧性与有限子覆盖
• Mathlib.Topology.MetricSpace.Bounded — Heine-Borel characterization / Heine-Borel 特征定理
• Mathlib.Order.ConditionallyCompleteLattice.Indexed — iSup/iInf properties / 上确界与下确界性质

License / 许可证

Apache 2.0