.. _topology:

.. index:: topology

拓扑学
========

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

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

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

虽然前面的章节所依赖的数学概念您可能已经熟悉，但“滤子”这一概念对您来说可能不太熟悉，甚至对许多从事数学工作的人员来说也是如此。
然而，这一概念对于有效地形式化数学来说是必不可少的。让我们解释一下原因。
设 ``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 种不同的极限表述，而且我们甚至还没有开始处理序列的极限，就像我们在 :numref:`sequences_and_convergence` 中所做的那样。

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

.. include:: C10_Topology/S01_Filters.inc
.. include:: C10_Topology/S02_Metric_Spaces.inc
.. include:: C10_Topology/S03_Topological_Spaces.inc