We give a proof of this theorem in lean using mathlib. This is the precise statement
theorem compact_unit_ball_implies_finite_dim :
compact (closed_ball 0 1 : set V) → vector_space.dim ℝ V < cardinal.omega
The mathematical proof we formalize goes like this:
Let V be a normed real vector space and assume its closed unit ball B
is compact. Cover B with finitely many open balls of radius 1/2 with
centers a_1, ..., a_N
. It suffices to show show that any v in B is in the span of a_1, ..., a_N
. So let v in B and define a sequence u n
by
u 0 = v
and u (n+1) = 2 (u n - b_n)
, where b_n
is of the a_1, ..., a_N
such that |u n - b_n| < 1/2
. Then v n = b 0 + 1/2 b 1 + ... + 1/2^n b n
satisfies
|v n - v| < 1/2^(n+1)
and hence v n
converges to v
and since the span of a finite set is closed this implies that v
is in the span of a_1, ..., a_N
.