Formalising Analysis in Lean: Compactness and Dimensionality

The theorem that a closed unit ball is compact if, and only if, its vector space is finite dimensional showcases how unintuitive infinite dimensional spaces can be. Many proofs skip over what’s considered obvious, leaving readers unaware of the underlying assumptions until they attempt formalization. We begin by proving a particular formulation of Riesz’s lemma in Lean. We then use it to construct a sequence in the unit ball where the distance between all elements is 1 and show that such a sequence cannot contain a convergent subsequence. Subsequently, we’ll establish that a closed unit ball is not sequentially compact. A significant challenge we encountered during this proof was the necessity to define the sequence through strong recursion, which posed some difficulties in its formalisation. We showcase Lean’s role in enhancing understanding and generalization of proofs by prompting us to explore broader definitions and theorems within the Mathlib library.