Mizar 对 Walter Rudin 的《数学分析原理》的评注/前言

The Mizar 系统 包含三个部分：一种用于编写数学证明的形式语言、一个用于自动检查这些证明的正确性的程序以及 Mizar 数学库 (MML)。自 1989 年成立以来，MML 规模已经相当庞大，其中存在一个小问题

编写 Mizar 最困难的部分是在 MML 中找到你需要的部分，这就是 Mizar 数学库的名称。不幸的是，这个问题没有简单的解决方案。你会发现除了这一点之外，编写 Mizar 文章是直截了当的。

—F. Wiedijk, 用九个简单的步骤编写 Mizar 文章

本书试图克服这个问题。我们选择了著名的经典分析书籍 《数学分析原理》（本书内的“这本书”）由 Walter Rudin 编写，并写下了在 MML 中找到本书定义和定理的位置。如果数学概念在本书和 MML 之间存在差异，则也会在适当的地方解释。例如，在本书中，没有解释什么是关系，而是解释了什么函数和（后来）等价关系，而这两种都是 Mizar 中的一种特殊类型的关系。

当然，由于 MML 并不包含所有数学，因此某些定义或定理可能尚未被形式化。此外，正如 Wiedijk 所写，在 MML 中搜索特定语句并不一定容易，因此本书的作者可能只是忽略了它，尽管他们付出了努力。因此，如果一个陈述被注释为“无参考”，则意味着“未找到参考”。

对于本书，除非另有说明，否则使用本书的第三版和 MML 的 5.54.1341 版本。