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 版本。