Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Preface

The Mizar system consists of three parts: a formal language to write mathematical proofs in, a programm to check these proofs for correctness automatically and the Mizar Mathematical Library (MML). The MML has gotten quite large since its founding in 1989 and therein lies a small problem:

The most difficult part of writing Mizar is finding what you need in the MML which is the name of the Mizar Mathematical Library. Unfortunately that problem has no easy solution. You will discover that apart from that, writing a Mizar article is straight-forward.

—F. Wiedijk, Writing a Mizar article in nine easy steps

This book is an attempt to overcome this problem. We've selected the well known classic analysis book Principles of Mathematical Analysis ("the Book" within this book) written by Walter Rudin and wrote down where to find the definitions and theorems of the Book in the MML. If mathematical concepts differ between the Book and the MML, this is explained as well where appropriate. For example, in the Book it isn't explained what exactly a relation is, but rather what a function and (later) equivalence relation is, while both are a special kind of relation in Mizar.

Of course, since the MML doesn't contain all of mathematics, some definitions or theorems may have not been formalized yet. Additionally, as Wiedijk wrote, it is not necessarily easy to search the MML for a specific statement, so the authors of this book could have simply overlooked it despite their efforts. So if a statement is commented with "no reference" it means "no reference found".

For this book, the third edition of the Book and version 5.54.1341 of the MML are used, unless otherwise stated.