Heine Borel in Lean

In this project gives a forzalisation using LEAN of the Heine-Borel theorem. It was developed as the final project for the Topology in LEAN course under the constraint of not relying on the standard Mathlib.Topology library. Every foundation was constructed from first principles.

The Heine-Borel Theorem

In metric spaces, the Heine-Borel theorem is one of the most classical results, characterizing compactness in terms of completeness and total boundedness.

Theorem: A metric space $X$ is compact if and only if it is complete and totally bounded.

Using Filters

While informal proofs of this theorem often rely on subsequence extraction and diagonal arguments, such approaches can become very hard to handle when formalized. This project adopts an approach based on Filters. This abstraction provides a more elegant and powerful framework for “classical” topological notions. The proof of Heine-Borel becomes a study of the interaction between compacteness (where maximal filters congerge), completeness (where Cauchy filters converge) and total boundedness (where every ultrafilter is Cauchy filter).

Resources

---

Selected Bibliography:

• de Moura, L., & Ullrich, S., The Lean 4 Theorem Prover and Programming Language. CADE 28, 2021.
• Ambrosio, L., Mantegazza, C., & Ricci, F., Complementi di matematica, 2021.
• Kelley, J. L., General Topology, Springer Graduate Texts in Mathematics, 1975.
• Munkres, J., Topology (Classic Version), Pearson, 2017.