Hirsch-Analysis Lean formalization
Formalization of some results of the book
Éléments d'Analyse Fonctionnelle
by Francis Hirsch and Gilles Lacombe.
HTML-rendered Lean proofs:
Countable.lean