10. 拓扑学

微积分建立在函数的概念之上，旨在对相互依赖的量进行建模。例如，研究随时间变化的量是一个常见的应用场景。 极限（limit） 这一概念同样基础。我们可以说，当 \(x\) 趋近于某个值 \(a\) 时，函数 \(f(x)\) 的极限是一个值 \(b\) ，或者说 \(f(x)\) 当 \(x\) 趋近于 \(a\) 时 收敛于（converges to） \(b\) 。 等价地，我们可以说当 \(x\) 趋近于某个值 \(a\) 时，\(f(x)\) 趋近于 \(b\) ，或者说它当 \(x\) 趋向于 \(a\) 时 趋向于（tends to） \(b\) 。我们在 Section 3.6 中已开始考虑此类概念。

拓扑学 是对极限和连续性的抽象研究。 在第 2 章到第 6 章中，我们已经介绍了形式化的基础知识，在本章中，我们将解释在 Mathlib 中如何形式化拓扑概念。 拓扑抽象不仅适用范围更广，而且有些矛盾的是，这也使得在具体实例中推理极限和连续性变得更加容易。

拓扑概念建立在多层数学结构之上。 第一层是朴素集合论，如第 Chapter 4 所述。 接下来的一层是 滤子 理论，我们将在 Section 10.1 中进行描述。 在此之上，我们再叠加 拓扑空间 、 度量空间 以及一种稍显奇特的中间概念—— 一致空间 的理论。

虽然前面的章节所依赖的数学概念您可能已经熟悉，但“滤子”这一概念对您来说可能不太熟悉，甚至对许多从事数学工作的人员来说也是如此。 然而，这一概念对于有效地形式化数学来说是必不可少的。让我们解释一下原因。 设 f : ℝ → ℝ 为任意函数。我们可以考虑当 x 趋近于某个值 x₀ 时 f x 的极限，但也可以考虑当 x 趋近于正无穷或负无穷时 f x 的极限。此外，我们还可以考虑当 x 从右趋近于 x₀ （通常记为 x₀⁺）或从左趋近于 x₀ （记为 x₀⁻）时 f x 的极限。还有些变化情况是 x 趋近于 x₀ 或 x₀⁺ 或 x₀⁻，但不允许取值为 x₀ 本身。 这导致了至少八种 x 趋近于某个值的方式。我们还可以限制 x 为有理数，或者对定义域施加其他约束，但让我们先只考虑这八种情况。

在值域方面，我们也有类似的多种选择： 我们可以指定 f x 从左侧或右侧趋近某个值，或者趋近正无穷或负无穷等等。 例如，我们可能希望说当 x 从右侧趋近 x₀ 但不等于 x₀ 时，f x 趋近于 +∞ 。 这会产生 64 种不同的极限表述，而且我们甚至还没有开始处理序列的极限，就像我们在 Section 3.6 中所做的那样。

当涉及到辅助引理时，问题变得更加复杂。 例如，极限的复合：如果当 x 趋近于 x₀ 时， f x 趋近于 y₀，且当 y 趋近于 y₀ 时， g y 趋近于 z₀，那么当 x 趋近于 x₀ 时， g ∘ f x 趋近于 z₀。 这里涉及三种“趋近于”的概念，每种概念都可以按照上一段描述的八种方式中的任何一种来实例化。 而这会产生 512 个引理，要添加到库中实在太多了！ 非正式地说，数学家通常只证明其中两三个，然后简单地指出其余的可以“以相同方式”进行证明。 形式化数学需要明确相关“相同”的概念，而这正是布尔巴基（Bourbaki）的滤子理论所做到的。

10.1. 滤子

类型 X 上的 滤子 是 X 的集合的集合，满足以下三个条件（我们将在下面详细说明）。该概念支持两个相关的想法：

  • 极限 ，包括上述讨论过的各种极限：数列的有限极限和无穷极限、函数在某点或无穷远处的有限极限和无穷极限等等。

  • 最终发生的事情 ，包括对于足够大的自然数 n : ℕ 发生的事情，或者在某一点 x 足够近的地方发生的事情，或者对于足够接近的点对发生的事情，或者在测度论意义上几乎处处发生的事情。对偶地，滤子也可以表达 经常发生的事情 的概念：对于任意大的 n ，在给定点的任意邻域内存在某点发生，等等。

与这些描述相对应的滤子将在本节稍后定义，但我们现在就可以给它们命名：

  • (atTop : Filter ℕ) ，由包含 {n | n ≥ N} 的 ℕ 的集合构成，其中 N 为某个自然数

  • 𝓝 x ，由拓扑空间中 x 的邻域构成

  • 𝓤 X ，由一致空间的邻域基构成（一致空间推广了度量空间和拓扑群）

  • μ.ae ，由相对于测度 μ 其补集测度为零的集合构成

一般的定义如下：一个滤子 F : Filter X 是集合 F.sets : Set (Set X) 的一个集合，满足以下条件：

  • F.univ_sets : univ ∈ F.sets

  • F.sets_of_superset : ∀ {U V}, U ∈ F.sets → U ⊆ V → V ∈ F.sets

  • F.inter_sets : ∀ {U V}, U ∈ F.sets → V ∈ F.sets → U ∩ V ∈ F.sets

第一个条件表明，集合 X 的所有元素都属于 F.sets 。 第二个条件表明，如果 U 属于 F.sets ，那么包含 U 的任何集合也属于 F.sets 。 第三个条件表明， F.sets 对有限交集是封闭的。 在 Mathlib 中，滤子 F 被定义为捆绑 F.sets 及其三个属性的结构，但这些属性不携带额外的数据，并且将 F 和 F.sets 之间的区别模糊化是方便的。我们 因此，将 U ∈ F 定义为 U ∈ F.sets 。 这就解释了为什么在一些提及 U ∈ F 的引理名称中会出现 sets 这个词。

可以将滤子视为定义“足够大”集合的概念。第一个条件表明 univ 是足够大的集合，第二个条件表明包含足够大集合的集合也是足够大的集合，第三个条件表明两个足够大集合的交集也是足够大的集合。

将类型 X 上的一个滤子视为 Set X 的广义元素，可能更有用。例如， atTop 是“极大数的集合”，而 𝓝 x₀ 是“非常接近 x₀ 的点的集合”。这种观点的一种体现是，我们可以将任何 s : Set X 与所谓的“主滤子”相关联，该主滤子由包含 s 的所有集合组成。 此定义已在 Mathlib 中，并有一个记号 𝓟 （在 Filter 命名空间中本地化）。为了演示的目的，我们请您借此机会在此处推导出该定义。

def principal {α : Type*} (s : Set α) : Filter α
    where
  sets := { t | s ⊆ t }
  univ_sets := sorry
  sets_of_superset := sorry
  inter_sets := sorry

对于我们的第二个示例，我们请您定义滤子 atTop : Filter ℕ （我们也可以使用任何具有预序关系的类型来代替 ℕ ）

example : Filter ℕ :=
  { sets := { s | ∃ a, ∀ b, a ≤ b → b ∈ s }
    univ_sets := sorry
    sets_of_superset := sorry
    inter_sets := sorry }

我们还可以直接定义任意实数 x : ℝ 的邻域滤子 𝓝 x 。在实数中， x 的邻域是一个包含开区间 \((x_0 - \varepsilon, x_0 + \varepsilon)\) 的集合，在 Mathlib 中定义为 Ioo (x₀ - ε) (x₀ + ε) 。（Mathlib 中的这种邻域概念只是更一般构造的一个特例。）

有了这些例子，我们就可以定义函数 f : X → Y 沿着某个 F : Filter X 收敛到某个 G : Filter Y 的含义，如下所述：

def Tendsto₁ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :=
  ∀ V ∈ G, f ⁻¹' V ∈ F

当 X 为 ℕ 且 Y 为 ℝ 时， Tendsto₁ u atTop (𝓝 x) 等价于说序列 u : ℕ → ℝ 收敛于实数 x 。当 X 和 Y 均为 ℝ 时， Tendsto f (𝓝 x₀) (𝓝 y₀) 等价于熟悉的概念 \(\lim_{x \to x₀} f(x) = y₀\) 。介绍中提到的所有其他类型的极限也等价于对源和目标上适当选择的滤子的 Tendsto₁ 的实例。

上述的 Tendsto₁ 概念在定义上等同于在 Mathlib 中定义的 Tendsto 概念，但后者定义得更为抽象。 Tendsto₁ 的定义存在的问题是它暴露了量词和 G 的元素，并且掩盖了通过将滤子视为广义集合所获得的直观理解。我们可以通过使用更多的代数和集合论工具来隐藏量词 ∀ V ，并使这种直观理解更加突出。第一个要素是与任何映射 f : X → Y 相关的 前推 操作 \(f_*\)，在 Mathlib 中记为 Filter.map f 。给定 X 上的滤子 F ， Filter.map f F : Filter Y 被定义为使得 V ∈ Filter.map f F ↔ f ⁻¹' V ∈ F 成立。在这个示例文件中，我们已经打开了 Filter 命名空间，因此 Filter.map 可以写成 map 。这意味着我们可以使用 Filter Y 上的序关系来重写 Tendsto 的定义，该序关系是成员集合的反向包含关系。换句话说，给定 G H : Filter Y ，我们有 G ≤ H ↔ ∀ V : Set Y， V ∈ H → V ∈ G 。

def Tendsto₂ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :=
  map f F ≤ G

example {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :
    Tendsto₂ f F G ↔ Tendsto₁ f F G :=
  Iff.rfl

可能看起来滤子上的序关系是反向的。但请回想一下，我们可以通过将任何集合 s 映射到相应的主滤子的 𝓟 : Set X → Filter X 的包含关系，将 X 上的滤子视为 Set X 的广义元素。这种包含关系是保序的，因此 Filter 上的序关系确实可以被视为广义集合之间的自然包含关系。在这个类比中，前推类似于直接像（direct image）。而且，确实有 map f (𝓟 s) = 𝓟 (f '' s) 。

现在我们可以直观地理解为什么一个序列 u : ℕ → ℝ 收敛于点 x₀ 当且仅当 map u atTop ≤ 𝓝 x₀ 成立。这个不等式意味着在 “ u 作用下”的“非常大的自然数集合”的“直接像”包含在“非常接近 x₀ 的点的集合”中。

正如所承诺的那样， Tendsto₂ 的定义中没有任何量词或集合。 它还利用了前推操作的代数性质。 首先，每个 Filter.map f 都是单调的。其次， Filter.map 与复合运算兼容。

#check (@Filter.map_mono : ∀ {α β} {m : α → β}, Monotone (map m))

#check
  (@Filter.map_map :
    ∀ {α β γ} {f : Filter α} {m : α → β} {m' : β → γ}, map m' (map m f) = map (m' ∘ m) f)

这两个性质结合起来使我们能够证明极限的复合性，从而一次性得出引言中描述的 256 种组合引理变体，以及更多。 您可以使用 Tendsto₁ 的全称量词定义或代数定义，连同上述两个引理，来练习证明以下陈述。

example {X Y Z : Type*} {F : Filter X} {G : Filter Y} {H : Filter Z} {f : X → Y} {g : Y → Z}
    (hf : Tendsto₁ f F G) (hg : Tendsto₁ g G H) : Tendsto₁ (g ∘ f) F H :=
  sorry

前推构造使用一个映射将滤子从映射源推送到映射目标。 还有一个“拉回”操作，即 Filter.comap ，其方向相反。 这推广了集合上的原像操作。对于任何映射 f ，

Filter.map f 和 Filter.comap f 构成了所谓的 伽罗瓦连接 ，也就是说，它们满足

filter.map_le_iff_le_comap : f 映射下的 F 小于等于 G 当且仅当 F 小于等于 G 在 f 下的逆像。

对于每一个 F 和 G 。 此操作可用于提供“Tendsto”的另一种表述形式，该形式可证明（但不是定义上）等同于 Mathlib 中的那个。

comap 操作可用于将滤子限制在子类型上。例如，假设我们有 f : ℝ → ℝ 、 x₀ : ℝ 和 y₀ : ℝ ，并且假设我们想要说明当 x 在有理数范围内趋近于 x₀ 时， f x 趋近于 y₀ 。我们可以使用强制转换映射 (↑) : ℚ → ℝ 将滤子 𝓝 x₀ 拉回到 ℚ ，并声明 Tendsto (f ∘ (↑) : ℚ → ℝ) (comap (↑) (𝓝 x₀)) (𝓝 y₀) 。

variable (f : ℝ → ℝ) (x₀ y₀ : ℝ)

#check comap ((↑) : ℚ → ℝ) (𝓝 x₀)

#check Tendsto (f ∘ (↑)) (comap ((↑) : ℚ → ℝ) (𝓝 x₀)) (𝓝 y₀)

拉回操作也与复合运算兼容，但它具有 逆变性 ，也就是说，它会颠倒参数的顺序。

section
variable {α β γ : Type*} (F : Filter α) {m : γ → β} {n : β → α}

#check (comap_comap : comap m (comap n F) = comap (n ∘ m) F)

end

现在让我们将注意力转向平面 ℝ × ℝ ，并尝试理解点 (x₀， y₀) 的邻域与 𝓝 x₀ 和 𝓝 y₀ 之间的关系。 存在一个乘积运算 Filter.prod : Filter X → Filter Y → Filter (X × Y) ，记作 ×ˢ ，它回答了这个问题：

example : 𝓝 (x₀, y₀) = 𝓝 x₀ ×ˢ 𝓝 y₀ :=
  nhds_prod_eq

该乘积运算通过拉回运算和 inf 运算来定义：

F ×ˢ G = (comap Prod.fst F) ⊓ (comap Prod.snd G)

这里的 inf 操作指的是对于任何类型 X 的 Filter X 上的格结构，其中 F ⊓ G 是小于 F 和 G 的最大滤子。 因此， inf 操作推广了集合交集的概念。

在 Mathlib 中的许多证明都使用了上述所有结构（ map 、 comap 、 inf 、 sup 和 prod ），从而给出关于收敛性的代数证明，而无需提及滤子的成员。您可以在以下引理的证明中练习这样做，如果需要，可以展开 Tendsto 和 Filter.prod 的定义。

#check le_inf_iff

example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) :
    Tendsto f atTop (𝓝 (x₀, y₀)) ↔
      Tendsto (Prod.fst ∘ f) atTop (𝓝 x₀) ∧ Tendsto (Prod.snd ∘ f) atTop (𝓝 y₀) :=
  sorry

有序类型 Filter X 实际上是一个 完备 格，也就是说，存在一个最小元素，存在一个最大元素，并且 X 上的每个滤子集都有一个 Inf 和一个 Sup 。

请注意，根据滤子定义中的第二个性质（如果 U 属于 F ，那么任何包含 U 的集合也属于 F ），第一个性质（ X 的所有元素组成的集合属于 F ）等价于 F 不是空集合这一性质。这不应与更微妙的问题相混淆，即空集是否为 F 的一个 元素 。滤子的定义并不禁止 ∅ ∈ F ，但如果空集在 F 中，那么每个集合都在 F 中，也就是说， ∀ U : Set X, U ∈ F 。在这种情况下， F 是一个相当平凡的滤子，恰好是完备格 Filter X 的最小元素。这与布尔巴基对滤子的定义形成对比，布尔巴基的定义不允许滤子包含空集。

由于我们在定义中包含了平凡滤子，所以在某些引理中有时需要明确假设非平凡性。不过作为回报，该理论具有更优的整体性质。我们已经看到，包含平凡滤子为我们提供了一个最小元素。它还允许我们定义 principal : Set X → Filter X ，将 ∅ 映射到 ⊥ ，而无需添加预条件来排除空集。而且它还允许我们定义拉回操作时无需预条件。实际上，有可能 comap f F = ⊥ 尽管 F ≠ ⊥ 。例如，给定 x₀ : ℝ 和 s : Set ℝ ， 𝓝 x₀ 在从与 s 对应的子类型强制转换下的拉回非平凡当且仅当 x₀ 属于 s 的闭包。

为了管理确实需要假设某些滤子非平凡的引理，Mathlib 设有类型类 Filter.NeBot ，并且库中存在假设 （F : Filter X）[F.NeBot] 的引理。实例数据库知道，例如， (atTop : Filter ℕ).NeBot ，并且知道将非平凡滤子向前推进会得到一个非平凡滤子。因此，假设 [F.NeBot] 的引理将自动应用于任何序列 u 的 map u atTop 。

我们对滤子的代数性质及其与极限的关系的探讨基本上已经完成，但我们尚未证明我们所提出的重新捕捉通常极限概念的主张是合理的。 表面上看， Tendsto u atTop (𝓝 x₀) 似乎比在 :numref: sequences_and_convergence 中定义的收敛概念更强，因为我们要求 x₀ 的 每个 邻域都有一个属于 atTop 的原像，而通常的定义仅要求对于标准邻域 Ioo (x₀ - ε) (x₀ + ε) 满足这一条件。关键在于，根据定义，每个邻域都包含这样的标准邻域。这一观察引出了 滤子基（filter basis） 的概念。

给定 F : Filter X ，如果对于每个集合 U ，我们有 U ∈ F 当且仅当它包含某个 s i ，那么集合族 s : ι → Set X 就是 F 的基。 换句话说，严格说来， s 是基当且仅当它满足 ∀ U : Set X, U ∈ F ↔ ∃ i, s i ⊆ U 。考虑在索引类型中仅选择某些值 i 的 ι 上的谓词会更加灵活。 对于 𝓝 x₀ ，我们希望 ι 为 ℝ ，用 ε 表示 i ，并且谓词应选择 ε 的正值。因此，集合 Ioo (x₀ - ε) (x₀ + ε) 构成 ℝ 上邻域拓扑的基这一事实可表述如下：

example (x₀ : ℝ) : HasBasis (𝓝 x₀) (fun ε : ℝ ↦ 0 < ε) fun ε ↦ Ioo (x₀ - ε) (x₀ + ε) :=
  nhds_basis_Ioo_pos x₀

还有一个很好的 atTop 滤子的基础。引理 Filter.HasBasis.tendsto_iff 允许我们在给定 F 和 G 的基础的情况下，重新表述形式为 Tendsto f F G 的陈述。将这些部分组合在一起，就基本上得到了我们在 :numref: sequences_and_convergence 中使用的收敛概念。

example (u : ℕ → ℝ) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ∈ Ioo (x₀ - ε) (x₀ + ε) := by
  have : atTop.HasBasis (fun _ : ℕ ↦ True) Ici := atTop_basis
  rw [this.tendsto_iff (nhds_basis_Ioo_pos x₀)]
  simp

现在我们展示一下滤子如何有助于处理对于足够大的数字或对于给定点足够近的点成立的性质。在 Section 3.6 中，我们经常遇到这样的情况：我们知道某个性质 P n 对于足够大的 n 成立，而另一个性质 Q n 对于足够大的 n 也成立。使用两次 cases 得到了满足 ∀ n ≥ N_P， P n 和 ∀ n ≥ N_Q， Q n 的 N_P 和 N_Q 。通过 set N := max N_P N_Q ，我们最终能够证明 ∀ n ≥ N， P n ∧ Q n 。反复这样做会让人感到厌烦。

我们可以通过注意到“对于足够大的 n， P n 和 Q n 成立”这一表述意味着我们有 {n | P n} ∈ atTop 和 {n | Q n} ∈ atTop 来做得更好。由于 atTop 是一个滤子，所以 atTop 中两个元素的交集仍在 atTop 中，因此我们有 {n | P n ∧ Q n} ∈ atTop 。书写 {n | P n} ∈ atTop 不太美观，但我们可以用更具提示性的记号 ∀ᶠ n in atTop， P n 。这里的上标 f 表示“滤子”。你可以将这个记号理解为对于“非常大的数集”中的所有 n ， P n 成立。 ∀ᶠ 记号代表 Filter.Eventually ，而引理 Filter.Eventually.and 利用滤子的交集性质来实现我们刚才所描述的操作：

example (P Q : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n) :
    ∀ᶠ n in atTop, P n ∧ Q n :=
  hP.and hQ

这种表示法如此方便且直观，以至于当 P 是一个等式或不等式陈述时，我们也有专门的表示形式。例如，设 u 和 v 是两个实数序列，让我们证明如果对于足够大的 n ， u n 和 v n 相等，那么 u 趋向于 x₀ 当且仅当 v 趋向于 x₀ 。首先我们将使用通用的 Eventually ，然后使用专门针对等式谓词的 EventuallyEq 。这两个陈述在定义上是等价的，因此在两种情况下相同的证明都适用。

example (u v : ℕ → ℝ) (h : ∀ᶠ n in atTop, u n = v n) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) :=
  tendsto_congr' h

example (u v : ℕ → ℝ) (h : u =ᶠ[atTop] v) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) :=
  tendsto_congr' h

从 Eventually 这一概念的角度来审视滤子的定义是很有启发性的。 给定滤子 F : Filter X ，对于 X 上的任意谓词 P 和 Q ，

条件 univ ∈ F 确保了 (∀ x, P x) → ∀ᶠ x in F, P x ， 条件 U ∈ F → U ⊆ V → V ∈ F 确保了 (∀ᶠ x in F, P x) → (∀ x, P x → Q x) → ∀ᶠ x in F, Q x ，并且 条件 U ∈ F → V ∈ F → U ∩ V ∈ F 确保了 (∀ᶠ x in F, P x) → (∀ᶠ x in F, Q x) → ∀ᶠ x in F, P x ∧ Q x 。

#check Eventually.of_forall
#check Eventually.mono
#check Eventually.and

第二个项目，对应于 Eventually.mono ，支持使用滤子的优雅方式，尤其是与 Eventually.and 结合使用时。 filter_upwards 策略使我们能够将它们组合起来。比较：

example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n)
    (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by
  apply (hP.and (hQ.and hR)).mono
  rintro n ⟨h, h', h''⟩
  exact h'' ⟨h, h'⟩

example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n)
    (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by
  filter_upwards [hP, hQ, hR] with n h h' h''
  exact h'' ⟨h, h'⟩

熟悉测度论的读者会注意到，补集测度为零的集合构成的滤子 μ.ae （即“几乎每个点构成的集合”）作为 Tendsto 的源或目标并不是很有用，但它可以方便地与 Eventually 一起使用，以表明某个性质对几乎每个点都成立。

存在 ∀ᶠ x in F, P x 的对偶版本，有时会很有用： 用 ∃ᶠ x in F, P x 表示

{x | ¬P x} ∉ F 。例如， ∃ᶠ n in atTop, P n 意味着存在任意大的 n 使得 P n 成立。 ∃ᶠ 符号代表 Filter.Frequently 。

对于一个更复杂的示例，请考虑以下关于序列 u 、集合 M 和值 x 的陈述：

如果序列 u 收敛于 x ，且对于足够大的 n ， u n 属于集合 M ，那么 x 就在集合 M 的闭包内。

这可以形式化表述如下：

Tendsto u atTop (𝓝 x) → (∀ᶠ n in atTop, u n ∈ M) → x ∈ closure M .

这是拓扑库中定理 mem_closure_of_tendsto 的一个特殊情况。 试着利用所引用的引理来证明它，利用 ClusterPt x F 意味着 (𝓝 x ⊓ F).NeBot 这一事实，以及根据定义， ∀ᶠ n in atTop， u n ∈ M 这一假设意味着 M ∈ map u atTop 。

#check mem_closure_iff_clusterPt
#check le_principal_iff
#check neBot_of_le

example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x))
    (huM : ∀ᶠ n in atTop, u n ∈ M) : x ∈ closure M :=
  sorry

10.2. 度量空间

在上一节中的示例主要关注实数序列。在本节中，我们将提高一点一般性，关注度量空间。 度量空间是一种类型 X ，它配备了一个距离函数 dist : X → X → ℝ ，这是在 X = ℝ 情形下函数 fun x y ↦ |x - y| 的一种推广。

引入这样一个空间很简单，我们将检验距离函数所需的所有性质。

variable {X : Type*} [MetricSpace X] (a b c : X)

#check (dist a b : ℝ)
#check (dist_nonneg : 0 ≤ dist a b)
#check (dist_eq_zero : dist a b = 0 ↔ a = b)
#check (dist_comm a b : dist a b = dist b a)
#check (dist_triangle a b c : dist a c ≤ dist a b + dist b c)

请注意，我们还有其他变体，其中距离可以是无穷大，或者 dist a b 可以为零而不需要 a = b 或者两者皆是。 它们分别被称为 EMetricSpace 、 PseudoMetricSpace 和 PseudoEMetricSpace （这里“e”代表“扩展”）。

请注意，我们从实数集 ℝ 到度量空间的旅程跳过了需要线性代数知识的赋范空间这一特殊情况，这部分内容将在微积分章节中进行解释。

10.2.1. 收敛与连续性

利用距离函数，我们已经能够在度量空间之间定义收敛序列和连续函数。 实际上，它们是在下一节所涵盖的更一般的情形中定义的， 但我们有一些引理将定义重新表述为距离的形式。

example {u : ℕ → X} {a : X} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε :=
  Metric.tendsto_atTop

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} :
    Continuous f ↔
      ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε :=
  Metric.continuous_iff

很多 引理都有一些连续性假设，所以我们最终要证明很多连续性结果，并且有一个专门用于此任务的 连续性 策略。让我们证明一个连续性陈述，它将在下面的一个练习中用到。请注意，Lean 知道如何将两个度量空间的乘积视为一个度量空间，因此考虑从 X × X 到 ℝ 的连续函数是有意义的。 特别是距离函数（未卷曲的版本）就是这样一种函数。

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by continuity

这种策略有点慢，所以了解如何手动操作也是有用的。我们首先需要利用 fun p : X × X ↦ f p.1 是连续的这一事实，因为它是连续函数 f （由假设 hf 给出）与投影 prod.fst 的复合，而 prod.fst 的连续性正是引理 continuous_fst 的内容。复合性质是 Continuous.comp ，它在 Continuous 命名空间中，所以我们可以用点表示法将 Continuous.comp hf continuous_fst 压缩为 hf.comp continuous_fst ，这实际上更易读，因为它确实读作将我们的假设和引理进行复合。我们对第二个分量做同样的操作，以获得 fun p ： X × X ↦ f p.2 的连续性。然后，我们使用 Continuous.prod_mk 将这两个连续性组合起来，得到 (hf.comp continuous_fst).prod_mk (hf.comp continuous_snd) : Continuous (fun p : X × X ↦ (f p.1， f p.2)) ，并再次复合以完成我们的完整证明。

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  continuous_dist.comp ((hf.comp continuous_fst).prod_mk (hf.comp continuous_snd))

通过 Continuous.comp 将 Continuous.prod_mk 和 continuous_dist 结合起来的方式感觉很笨拙，即便像上面那样大量使用点标记也是如此。更严重的问题在于，这个漂亮的证明需要大量的规划。Lean 接受上述证明项是因为它是一个完整的项，证明了一个与我们的目标定义上等价的陈述，关键在于要展开的定义是函数的复合。实际上，我们的目标函数 fun p ： X × X ↦ dist (f p.1) (f p.2) 并未以复合的形式给出。我们提供的证明项证明了 dist ∘ (fun p ： X × X ↦ (f p.1， f p.2)) 的连续性，而这恰好与我们的目标函数定义上相等。但如果尝试从 apply continuous_dist.comp 开始逐步使用战术构建这个证明，Lean 的繁饰器将无法识别复合函数并拒绝应用此引理。当涉及类型乘积时，这种情况尤其糟糕。

这里更适用的引理是

Continuous.dist {f g : X → Y} : Continuous f → Continuous g → Continuous (fun x ↦ dist (f x) (g x))

它对 Lean 的繁饰器更友好，并且在直接提供完整证明项时也能提供更简短的证明，这一点从以下两个对上述陈述的新证明中可以看出：

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by
  apply Continuous.dist
  exact hf.comp continuous_fst
  exact hf.comp continuous_snd

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  (hf.comp continuous_fst).dist (hf.comp continuous_snd)

请注意，如果不考虑来自组合的详细说明问题，压缩我们证明的另一种方法是使用 Continuous.prod_map ，它有时很有用，并给出一个替代的证明项 continuous_dist.comp (hf.prod_map hf) ，这个证明项甚至更短，输入起来也更方便。

由于在便于详细阐述的版本和便于输入的较短版本之间做出选择令人感到遗憾，让我们以 Continuous.fst' 提供的最后一点压缩来结束这个讨论，它允许将 hf.comp continuous_fst 压缩为 hf.fst' （ snd 也是如此），从而得到我们的最终证明，现在已接近晦涩难懂的程度。

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  hf.fst'.dist hf.snd'

现在轮到你来证明一些连续性引理了。在尝试了连续性策略之后，你将需要使用 Continuous.add 、 continuous_pow 和 continuous_id 手动完成证明。

example {f : ℝ → X} (hf : Continuous f) : Continuous fun x : ℝ ↦ f (x ^ 2 + x) :=
  sorry

到目前为止，我们把连续性视为一个整体概念，但也可以定义某一点处的连续性。

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (a : X) :
    ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x}, dist x a < δ → dist (f x) (f a) < ε :=
  Metric.continuousAt_iff

10.2.2. 球、开集与闭集

一旦我们有了距离函数，最重要的几何定义就是（开）球和闭球。

variable (r : ℝ)

example : Metric.ball a r = { b | dist b a < r } :=
  rfl

example : Metric.closedBall a r = { b | dist b a ≤ r } :=
  rfl

请注意，这里的 r 是任意实数，没有符号限制。当然，有些陈述确实需要半径条件。

example (hr : 0 < r) : a ∈ Metric.ball a r :=
  Metric.mem_ball_self hr

example (hr : 0 ≤ r) : a ∈ Metric.closedBall a r :=
  Metric.mem_closedBall_self hr

一旦我们有了球，就可以定义开集。实际上，它们是在下一节所涵盖的更一般的情形中定义的，但我们有一些引理将定义重新表述为用球来表示。

example (s : Set X) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s :=
  Metric.isOpen_iff

那么闭集就是其补集为开集的集合。它们的重要性质是它们在极限运算下是封闭的。一个集合的闭包是包含它的最小闭集。

example {s : Set X} : IsClosed s ↔ IsOpen (sᶜ) :=
  isOpen_compl_iff.symm

example {s : Set X} (hs : IsClosed s) {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a))
    (hus : ∀ n, u n ∈ s) : a ∈ s :=
  hs.mem_of_tendsto hu (Eventually.of_forall hus)

example {s : Set X} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, a ∈ Metric.ball b ε :=
  Metric.mem_closure_iff

请在不使用 mem_closure_iff_seq_limit 的情况下完成下一个练习。

example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) :
    a ∈ closure s :=
  sorry

请记住，在滤子部分中提到，邻域滤子在 Mathlib 中起着重要作用。在度量空间的背景下，关键在于球体为这些滤子提供了基。这里的主要引理是 Metric.nhds_basis_ball 和 Metric.nhds_basis_closedBall ，它们分别表明具有正半径的开球和闭球具有这一性质。中心点是一个隐式参数，因此我们可以像下面的例子那样调用 Filter.HasBasis.mem_iff 。

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s :=
  Metric.nhds_basis_ball.mem_iff

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.closedBall x ε ⊆ s :=
  Metric.nhds_basis_closedBall.mem_iff

10.2.3. 紧致性

紧性是一个重要的拓扑概念。它区分了度量空间中的子集，这些子集具有与实数中的线段相同的性质，而与其他区间不同：

  • 任何取值于紧集中的序列都有一个子序列在该紧集中收敛。

  • 在非空紧集上取实数值的任何连续函数都是有界的，并且在某个地方达到其界值（这被称为极值定理）。

  • 紧集是闭集。

首先让我们验证实数中的单位区间确实是一个紧集，然后验证一般度量空间中紧集的上述断言。在第二个陈述中，我们只需要在给定的集合上连续，因此我们将使用 ContinuousOn 而不是 Continuous ，并且我们将分别给出最小值和最大值的陈述。当然，所有这些结果都是从更一般的形式推导出来的，其中一些将在后面的章节中讨论。

example : IsCompact (Set.Icc 0 1 : Set ℝ) :=
  isCompact_Icc

example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) :
    ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) :=
  hs.tendsto_subseq hu

example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ}
      (hfs : ContinuousOn f s) :
    ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y :=
  hs.exists_isMinOn hs' hfs

example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ}
      (hfs : ContinuousOn f s) :
    ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x :=
  hs.exists_isMaxOn hs' hfs

example {s : Set X} (hs : IsCompact s) : IsClosed s :=
  hs.isClosed

我们还可以通过添加一个额外的 Prop 值类型类来指定度量空间是全局紧致的：

example {X : Type*} [MetricSpace X] [CompactSpace X] : IsCompact (univ : Set X) :=
  isCompact_univ

在紧致度量空间中，任何闭集都是紧致的，这就是 IsClosed.isCompact 。 一致连续函数 ^^^^^^^^^^^

现在我们来探讨度量空间上的均匀性概念：一致连续函数、柯西序列和完备性。 同样，这些概念是在更一般的背景下定义的，但在度量空间中我们有引理来获取它们的基本定义。 我们先从一致连续性讲起。

example {X : Type*} [MetricSpace X] {Y : Type*} [MetricSpace Y] {f : X → Y} :
    UniformContinuous f ↔
      ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε :=
  Metric.uniformContinuous_iff

为了练习运用所有这些定义，我们将证明从紧致度量空间到度量空间的连续函数是一致连续的（在后面的章节中我们将看到更一般的形式）。

我们首先给出一个非正式的概述。设 f : X → Y 是从一个紧致度量空间到一个度量空间的连续函数。 我们固定 ε > 0 ，然后开始寻找某个 δ 。

令 φ : X × X → ℝ ：= fun p ↦ dist (f p.1) (f p.2) 以及 K := { p ： X × X | ε ≤ φ p } 。 注意到由于 f 和距离函数都是连续的，所以 φ 也是连续的。 并且 K 显然是闭集（使用 isClosed_le ），因此由于 X 是紧致的，所以 K 也是紧致的。

然后我们使用 eq_empty_or_nonempty 来讨论两种可能性。如果集合 K 为空，那么显然我们已经完成了（例如，我们可以设 δ = 1 ）。所以假设 K 不为空，利用极值定理选择 (x₀, x₁) 使得距离函数在 K 上达到最小值。然后我们可以设 δ = dist x₀ x₁ 并检查一切是否都正常。

example {X : Type*} [MetricSpace X] [CompactSpace X]
      {Y : Type*} [MetricSpace Y] {f : X → Y}
    (hf : Continuous f) : UniformContinuous f :=
  sorry

10.2.4. 完备性

度量空间中的柯西序列是指其各项越来越接近的序列。 表述这一概念有几种等价的方式。 特别是收敛序列是柯西序列。但反过来只有在所谓的 完备 空间中才成立。

example (u : ℕ → X) :
    CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε :=
  Metric.cauchySeq_iff

example (u : ℕ → X) :
    CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε :=
  Metric.cauchySeq_iff'

example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) :
    ∃ x, Tendsto u atTop (𝓝 x) :=
  cauchySeq_tendsto_of_complete hu

我们将通过证明一个方便的判别式来练习使用这个定义，该判别式是 Mathlib 中出现的一个判别式的特殊情况。这也是一个在几何背景下练习使用大求和符号的好机会。除了滤子部分的解释外，您可能还需要使用 tendsto_pow_atTop_nhds_zero_of_lt_one 、 Tendsto.mul 和 dist_le_range_sum_dist 。

theorem cauchySeq_of_le_geometric_two' {u : ℕ → X}
    (hu : ∀ n : ℕ, dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : CauchySeq u := by
  rw [Metric.cauchySeq_iff']
  intro ε ε_pos
  obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε := by sorry
  use N
  intro n hn
  obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn
  calc
    dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
    _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
    _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry
    _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry
    _ ≤ 1 / 2 ^ N * 2 := sorry
    _ < ε := sorry

我们已准备好迎接本节的最终大 Boss：完备度量空间上的贝尔纲定理（Baire’s theorem）！ 下面的证明框架展示了有趣的技术。它使用了感叹号形式的 choose 策略（您应该尝试去掉这个感叹号），并且展示了如何在证明过程中使用 Nat.rec_on 来递归定义某些内容。

open Metric

example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : ∀ n, Dense (f n)) :
    Dense (⋂ n, f n) := by
  let B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
  have Bpos : ∀ n, 0 < B n
  sorry
  /- 将密度假设转化为两个函数 `center` 和 `radius`，对于任意的 n、x、δ、δpos，这两个函数分别关联一个中心和一个正半径，使得 `closedBall center radius` 同时包含在 `f n` 和 `closedBall x δ` 中。我们还可以要求 `radius ≤ (1/2)^(n+1)`，以确保之后能得到一个柯西序列。-/
  have :
    ∀ (n : ℕ) (x : X),
      ∀ δ > 0, ∃ y : X, ∃ r > 0, r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n :=
    by sorry
  choose! center radius Hpos HB Hball using this
  intro x
  rw [mem_closure_iff_nhds_basis nhds_basis_closedBall]
  intro ε εpos
  /-  设 `ε` 为正数。我们需要在以 `x` 为圆心、半径为 `ε` 的球内找到一个点，该点属于所有的 `f n`。为此，我们递归地构造一个序列 `F n = (c n, r n)`，使得闭球 `closedBall (c n) (r n)` 包含在前一个球内且属于 `f n`，并且 `r n` 足够小以确保 `c n` 是一个柯西序列。那么 `c n` 收敛到一个极限，该极限属于所有的 `f n`。-/
  let F : ℕ → X × ℝ := fun n ↦
    Nat.recOn n (Prod.mk x (min ε (B 0)))
      fun n p ↦ Prod.mk (center n p.1 p.2) (radius n p.1 p.2)
  let c : ℕ → X := fun n ↦ (F n).1
  let r : ℕ → ℝ := fun n ↦ (F n).2
  have rpos : ∀ n, 0 < r n := by sorry
  have rB : ∀ n, r n ≤ B n := by sorry
  have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by
    sorry
  have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by sorry
  have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist
  -- 由于序列 `c n` 在完备空间中是柯西序列，所以它收敛于极限 `y`。
  -- 根据完备空间中柯西序列收敛的定理，存在 `y` 使得 `c n` 收敛于 `y`，记为 `ylim`。
  -- 这个点 `y` 就是我们想要的点。接下来我们要验证它属于所有的 `f n` 以及 `ball x ε`。
  use y
  have I : ∀ n, ∀ m ≥ n, closedBall (c m) (r m) ⊆ closedBall (c n) (r n) := by sorry
  have yball : ∀ n, y ∈ closedBall (c n) (r n) := by sorry
  sorry

10.3. 拓扑空间

10.3.1. 基础

我们现在提高一般性，引入拓扑空间。我们将回顾定义拓扑空间的两种主要方式，然后解释拓扑空间范畴比度量空间范畴表现得要好得多。请注意，这里我们不会使用 Mathlib 的范畴论，只是采用一种稍微范畴化一点的观点。

从度量空间到拓扑空间转变的第一种思考方式是，我们只记住开集（或等价地，闭集）的概念。从这个角度来看，拓扑空间是一种配备了被称为开集的集合族的类型。这个集合族必须满足下面给出的若干公理（这个集合族稍有冗余，但我们忽略这一点）。

section
variable {X : Type*} [TopologicalSpace X]

example : IsOpen (univ : Set X) :=
  isOpen_univ

example : IsOpen (∅ : Set X) :=
  isOpen_empty

example {ι : Type*} {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) : IsOpen (⋃ i, s i) :=
  isOpen_iUnion hs

example {ι : Type*} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) :
    IsOpen (⋂ i, s i) :=
  isOpen_iInter_of_finite hs

闭集被定义为补集是开集的集合。拓扑空间之间的函数是（全局）连续的，当且仅当所有开集的原像都是开集。

variable {Y : Type*} [TopologicalSpace Y]

example {f : X → Y} : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
  continuous_def

根据这个定义，我们已经可以看出，与度量空间相比，拓扑空间仅保留了足够的信息来讨论连续函数：如果且仅如果两种拓扑结构具有相同的连续函数，则类型上的两种拓扑结构相同（实际上，当且仅当两种结构具有相同的开集时，恒等函数在两个方向上都是连续的）。

然而，一旦我们转向某一点的连续性，就会看到基于开集的方法的局限性。在 Mathlib 中，我们经常将拓扑空间视为每个点 x 都附带一个邻域滤子 𝓝 x 的类型（相应的函数 X → Filter X 满足进一步说明的某些条件）。回想一下滤子部分的内容，这些工具发挥着两个相关的作用。首先， 𝓝 x 被视为 X 中接近 x 的点的广义集合。其次，它被视为一种方式，用于说明对于任何谓词 P : X → Prop ，该谓词对于足够接近 x 的点成立。让我们来陈述 f ： X → Y 在 x 处连续。纯粹基于滤子的说法是， f 下 x 附近点的广义集合的直接像包含在 f x 附近点的广义集合中。回想一下，这可以写成 map f (𝓝 x) ≤ 𝓝 (f x) 或者 Tendsto f (𝓝 x) (𝓝 (f x)) 。

example {f : X → Y} {x : X} : ContinuousAt f x ↔ map f (𝓝 x) ≤ 𝓝 (f x) :=
  Iff.rfl

还可以使用被视为普通集合的邻域和被视为广义集合的邻域滤子来拼写它：“对于 f x 的任何邻域 U ，所有靠近 x 的点都被发送到 U ”。请注意，证明又是 iff.rfl ，这种观点在定义上与前一种观点等价。

example {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ U ∈ 𝓝 (f x), ∀ᶠ x in 𝓝 x, f x ∈ U :=
  Iff.rfl

现在我们来解释如何从一种观点转换到另一种观点。就开集而言，我们可以简单地将 𝓝 x 的成员定义为包含一个包含 x 的开集的集合。

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t :=
  mem_nhds_iff

要朝另一方向进行，我们需要讨论 𝓝 ： X → Filter X 成为拓扑的邻域函数必须满足的条件。

第一个约束条件是，将 𝓝 x 视为广义集合时，它将包含被视为广义集合 pure x 的集合 {x} （解释这个奇怪的名字会离题太远，所以我们暂时接受它）。另一种说法是，如果一个谓词对靠近 x 的点成立，那么它在 x 处也成立。

example (x : X) : pure x ≤ 𝓝 x :=
  pure_le_nhds x

example (x : X) (P : X → Prop) (h : ∀ᶠ y in 𝓝 x, P y) : P x :=
  h.self_of_nhds

然后一个更微妙的要求是，对于任何谓词 P : X → Prop 以及任何 x ，如果 P y 对于接近 x 的 y 成立，那么对于接近 x 的 y 以及接近 y 的 z ， P z 也成立。更确切地说，我们有：

example {P : X → Prop} {x : X} (h : ∀ᶠ y in 𝓝 x, P y) : ∀ᶠ y in 𝓝 x, ∀ᶠ z in 𝓝 y, P z :=
  eventually_eventually_nhds.mpr h

这两个结果描述了对于集合 X 上的拓扑空间结构而言，函数 X → Filter X 成为邻域函数的特征。仍然存在一个函数 TopologicalSpace.mkOfNhds : (X → Filter X) → TopologicalSpace X ，但只有当输入满足上述两个约束条件时，它才会将其作为邻域函数返回。更确切地说，我们有一个引理 TopologicalSpace.nhds_mkOfNhds ，以另一种方式说明了这一点，而我们的下一个练习将从上述表述方式推导出这种不同的表述方式。

example {α : Type*} (n : α → Filter α) (H₀ : ∀ a, pure a ≤ n a)
    (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x) :
    ∀ a, ∀ s ∈ n a, ∃ t ∈ n a, t ⊆ s ∧ ∀ a' ∈ t, s ∈ n a' :=
  sorry

请注意， TopologicalSpace.mkOfNhds 并不经常使用，但了解拓扑空间结构中邻域滤子的精确含义仍然是很有好处的。

要在 Mathlib 中高效地使用拓扑空间，接下来需要了解的是，我们大量使用了 TopologicalSpace : Type u → Type u 的形式属性。从纯粹的数学角度来看，这些形式属性是解释拓扑空间如何解决度量空间存在的问题的一种非常清晰的方式。从这个角度来看，拓扑空间解决的问题在于度量空间的函子性非常差，而且总体上具有非常糟糕的范畴性质。这还不包括前面已经讨论过的度量空间包含大量拓扑上无关的几何信息这一事实。

我们先关注函子性。度量空间结构可以诱导到子集上，或者等价地说，可以通过单射映射拉回。但也就仅此而已。它们不能通过一般的映射拉回，甚至不能通过满射映射推前。

特别是对于度量空间的商空间或不可数个度量空间的乘积，不存在合理的距离。例如，考虑类型 ℝ → ℝ ，将其视为由 ℝ 索引的 ℝ 的副本的乘积。我们希望说函数序列的逐点收敛是一种值得考虑的收敛概念。但在 ℝ → ℝ 上不存在能给出这种收敛概念距离。与此相关的是，不存在这样的距离，使得映射 f : X → (ℝ → ℝ) 是连续的当且仅当对于每个 t ： ℝ ， fun x ↦ f x t 是连续的。

现在我们来回顾一下用于解决所有这些问题的数据。首先，我们可以使用任何映射 f : X → Y 将拓扑从一侧推到另一侧或从另一侧拉到这一侧。这两个操作形成了一个伽罗瓦连接。

variable {X Y : Type*}

example (f : X → Y) : TopologicalSpace X → TopologicalSpace Y :=
  TopologicalSpace.coinduced f

example (f : X → Y) : TopologicalSpace Y → TopologicalSpace X :=
  TopologicalSpace.induced f

example (f : X → Y) (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) :
    TopologicalSpace.coinduced f T_X ≤ T_Y ↔ T_X ≤ TopologicalSpace.induced f T_Y :=
  coinduced_le_iff_le_induced

这些操作与函数的复合兼容。 通常，前推是协变的，后拉是逆变的，参见 coinduced_compose 和 induced_compose 。 在纸上，我们将使用记号 \(f_*T\) 表示 TopologicalSpace.coinduced f T ，使用记号 \(f^*T\) 表示 TopologicalSpace.induced f T 。 接下来的一个重要部分是在给定结构下对 拓扑空间 X 建立一个完整的格结构。如果您认为拓扑主要是开集的数据，那么您会期望 拓扑空间 X 上的序关系来自 Set (Set X) ，即您期望 t ≤ t' 当且仅当对于 t' 中的开集 u ，它在 t 中也是开集。然而，我们已经知道 Mathlib 更侧重于邻域而非开集，因此对于任何 x ： X ，我们希望从拓扑空间到邻域的映射 fun T ： TopologicalSpace X ↦ @nhds X T x 是保序的。而且我们知道 Filter X 上的序关系是为确保 principal : Set X → Filter X 保序而设计的，从而可以将滤子视为广义集合。所以我们在 TopologicalSpace X 上使用的序关系与来自 Set (Set X) 的序关系是相反的。

example {T T' : TopologicalSpace X} : T ≤ T' ↔ ∀ s, T'.IsOpen s → T.IsOpen s :=
  Iff.rfl

现在，我们可以通过将推进（或拉回）操作与序关系相结合来恢复连续性。

example (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) (f : X → Y) :
    Continuous f ↔ TopologicalSpace.coinduced f T_X ≤ T_Y :=
  continuous_iff_coinduced_le

有了这个定义以及前推和复合的兼容性，我们自然地得到了这样一个通用性质：对于任何拓扑空间 \(Z\) ，函数 \(g : Y → Z\) 对于拓扑 ：math:f_*T_X 是连续的，当且仅当 \(g ∘ f\) 是连续的。

\[\begin{split}g \text{ continuous } &⇔ g_*(f_*T_X) ≤ T_Z \\ &⇔ (g ∘ f)_* T_X ≤ T_Z \\ &⇔ g ∘ f \text{ continuous}\end{split}\]
example {Z : Type*} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z)
      (g : Y → Z) :
    @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔
      @Continuous X Z T_X T_Z (g ∘ f) := by
  rw [continuous_iff_coinduced_le, coinduced_compose, continuous_iff_coinduced_le]

因此，我们已经得到了商拓扑（使用投影映射作为 f ）。这并没有用到对于所有 X ， TopologicalSpace X 都是一个完备格这一事实。现在让我们看看所有这些结构如何通过抽象的废话证明积拓扑的存在性。 我们上面考虑了 ℝ → ℝ 的情况，但现在让我们考虑一般情况 Π i, X i ，其中 ι : Type* 且 X ： ι → Type* 。我们希望对于任何拓扑空间 Z 以及任何函数 f ： Z → Π i， X i ， f 是连续的当且仅当 (fun x ↦ x i) ∘ f 对于所有 i 都是连续的。 让我们在纸上用符号 p_i 表示投影 (fun (x ： Π i， X i) ↦ x i) 来探究这个约束条件：

\[\begin{split}(∀ i, p_i ∘ f \text{ continuous}) &⇔ ∀ i, (p_i ∘ f)_* T_Z ≤ T_{X_i} \\ &⇔ ∀ i, (p_i)_* f_* T_Z ≤ T_{X_i}\\ &⇔ ∀ i, f_* T_Z ≤ (p_i)^*T_{X_i}\\ &⇔ f_* T_Z ≤ \inf \left[(p_i)^*T_{X_i}\right]\end{split}\]

因此我们看到，对于 Π i, X i ，我们想要的拓扑结构是什么：

example (ι : Type*) (X : ι → Type*) (T_X : ∀ i, TopologicalSpace (X i)) :
    (Pi.topologicalSpace : TopologicalSpace (∀ i, X i)) =
      ⨅ i, TopologicalSpace.induced (fun x ↦ x i) (T_X i) :=
  rfl

这就结束了我们关于 Mathlib 的探讨，其如何认为拓扑空间通过成为更具函子性的理论与对于任何固定类型都具有完备格结构的特性，从而弥补度量空间理论的缺陷。

10.3.2. 分离性与可数性

我们看到拓扑空间范畴具有非常良好的性质。为此付出的代价是存在一些相当病态的拓扑空间。 你可以对拓扑空间做出一些假设，以确保其行为更接近度量空间。其中最重要的是 T2 空间 ，也称为“豪斯多夫空间”，它能确保极限是唯一的。 更强的分离性质是 T3 空间 ，它还确保了 正则空间 性质：每个点都有一个闭邻域基。

example [TopologicalSpace X] [T2Space X] {u : ℕ → X} {a b : X} (ha : Tendsto u atTop (𝓝 a))
    (hb : Tendsto u atTop (𝓝 b)) : a = b :=
  tendsto_nhds_unique ha hb

example [TopologicalSpace X] [RegularSpace X] (a : X) :
    (𝓝 a).HasBasis (fun s : Set X ↦ s ∈ 𝓝 a ∧ IsClosed s) id :=
  closed_nhds_basis a

请注意，根据定义，在每个拓扑空间中，每个点都有一个开邻域基。

example [TopologicalSpace X] {x : X} :
    (𝓝 x).HasBasis (fun t : Set X ↦ t ∈ 𝓝 x ∧ IsOpen t) id :=
  nhds_basis_opens' x

我们现在的主要目标是证明基本定理，该定理允许通过连续性进行延拓。从布尔巴基学派的《一般拓扑学》一书，第 I 卷第 8.5 节，定理 1（仅取非平凡的蕴含部分）：

设 \(X\) 为拓扑空间，\(A\) 是 \(X\) 的一个稠密子集，\(f : A → Y\) 是将 \(A\) 映射到 \(T_3\) 空间 \(Y\) 的连续映射。若对于 \(X\) 中的每个点 \(x\) ，当 \(y\) 趋近于 \(x\) 且始终处于 \(A\) 内时，\(f(y)\) 在 \(Y\) 中趋于一个极限，则存在 \(f\) 在 \(X\) 上的连续延拓 \(φ\) 。

实际上，Mathlib 包含了上述引理的一个更通用的版本 DenseInducing.continuousAt_extend ，但在这里我们将遵循布尔巴基的版本。

请记住，对于 A : Set X ， ↥A 是与 A 相关联的子类型，并且在需要时，Lean 会自动插入那个有趣的上箭头。而（包含）强制转换映射为 (↑) : A → X 。假设“趋向于 \(x\) 且始终处于 \(A\) 中”对应于拉回滤子 comap (↑) (𝓝 x) 。

我们首先证明一个辅助引理，将其提取出来以简化上下文（特别是这里我们不需要 Y 是拓扑空间）。

theorem aux {X Y A : Type*} [TopologicalSpace X] {c : A → X}
      {f : A → Y} {x : X} {F : Filter Y}
      (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) :
    ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := by
  sorry

现在让我们来证明连续性延拓定理的主要内容。

当需要在 ↥A 上定义拓扑时，Lean 会自动使用诱导拓扑。 唯一相关的引理是

nhds_induced (↑) : ∀ a ： ↥A， 𝓝 a = comap (↑) (𝓝 ↑a)

（这实际上是一个关于诱导拓扑的一般引理）。

证明的大致思路是：

主要假设和选择公理给出一个函数 φ ，使得

∀ x, Tendsto f (comap (↑) (𝓝 x)) (𝓝 (φ x))

（因为 Y 是豪斯多夫空间， φ 是完全确定的，但在我们试图证明 φ 确实扩展了 f 之前，我们不需要这一点）。

首先证明 φ 是连续的。固定任意的 x : X 。 由于 Y 是正则的，只需检查对于 φ x 的每个 闭 邻域 V' ， φ⁻¹' V' ∈ 𝓝 x 。 极限假设（通过上面的辅助引理）给出了某个 V ∈ 𝓝 x ，使得 IsOpen V ∧ (↑)⁻¹' V ⊆ f⁻¹' V' 。 由于 V ∈ 𝓝 x ，只需证明 V ⊆ φ⁻¹' V' ，即 ∀ y ∈ V， φ y ∈ V' 。 固定 V 中的 y 。因为 V 是 开 的，所以它是 y 的邻域。 特别是 (↑)⁻¹' V ∈ comap (↑) (𝓝 y) 且更进一步 f⁻¹' V' ∈ comap (↑) (𝓝 y) 。 此外， comap (↑) (𝓝 y) ≠ ⊥ 因为 A 是稠密的。 因为我们知道 Tendsto f (comap (↑) (𝓝 y)) (𝓝 (φ y)) ，这表明 φ y ∈ closure V' ，并且由于 V' 是闭的，我们已经证明了 φ y ∈ V' 。

接下来要证明的是 φ 延拓了 f 。这里就要用到 f 的连续性以及 Y 是豪斯多夫空间这一事实。

example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X}
    (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f)
    (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) (𝓝 x)) (𝓝 c)) :
    ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := by
  sorry

#check HasBasis.tendsto_right_iff

除了分离性之外，您还可以对拓扑空间做出的主要假设是可数性假设，以使其更接近度量空间。其中最主要的是第一可数性，即要求每个点都有一个可数的邻域基。特别是，这确保了集合的闭包可以通过序列来理解。

example [TopologicalSpace X] [FirstCountableTopology X]
      {s : Set X} {a : X} :
    a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) :=
  mem_closure_iff_seq_limit

10.3.3. 紧致性

现在让我们来讨论一下拓扑空间的紧致性是如何定义的。和往常一样，对此有多种思考方式，而 Mathlib 采用的是滤子版本。

我们首先需要定义滤子的聚点。给定拓扑空间 X 上的一个滤子 F ，若将 F 视为广义集合，则点 x : X 是 F 的聚点，当且仅当 F 与广义集合中所有接近 x 的点的集合有非空交集。

那么我们就可以说，集合 s 是紧致的，当且仅当包含于 s 中的每一个非空广义集合 F ，即满足 F ≤ 𝓟 s 的集合，都在 s 中有一个聚点。

variable [TopologicalSpace X]

example {F : Filter X} {x : X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) :=
  Iff.rfl

example {s : Set X} :
    IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F :=
  Iff.rfl

例如，如果 F 是 map u atTop ，即 u ： ℕ → X 在 atTop 下的像，其中 atTop 是非常大的自然数的广义集合，那么假设 F ≤ 𝓟 s 意味着对于足够大的 n ， u n 属于 s 。说 x 是 map u atTop 的聚点意味着非常大的数的像与接近 x 的点的集合相交。如果 𝓝 x 有一个可数基，我们可以将其解释为说 u 有一个子序列收敛于 x ，这样我们就得到了度量空间中紧致性的样子。

example [FirstCountableTopology X] {s : Set X} {u : ℕ → X} (hs : IsCompact s)
    (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) :=
  hs.tendsto_subseq hu

聚点与连续函数的性质相容。

variable [TopologicalSpace Y]

example {x : X} {F : Filter X} {G : Filter Y} (H : ClusterPt x F) {f : X → Y}
    (hfx : ContinuousAt f x) (hf : Tendsto f F G) : ClusterPt (f x) G :=
  ClusterPt.map H hfx hf

作为练习，我们将证明连续映射下的紧集的像是紧集。除了我们已经看到的内容外，您还应该使用 Filter.push_pull 和 NeBot.of_map 。

example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) :
    IsCompact (f '' s) := by
  intro F F_ne F_le
  have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F := by sorry
  have Hne : (𝓟 s ⊓ comap f F).NeBot := by sorry
  have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s := inf_le_left
  sorry

也可以用开覆盖来表述紧性： s 是紧的，当且仅当覆盖 s 的每一个开集族都有一个有限的覆盖子族。

example {ι : Type*} {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i))
    (hsU : s ⊆ ⋃ i, U i) : ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i :=
  hs.elim_finite_subcover U hUo hsU