# How to prove the Hahn-Banach constructively

I am just wondering, how to prove the Hahn-Banach theorem constructively for a finite dimensional normed vector space.

-
I am not sure this question reflects the level of this site. I am a bit puzzled about the attention it gets. –  András Bátkai Sep 27 '11 at 21:55
@Andras: IMHO, the question might be borderline, but it is definitely not trivial (or at least, it is as non-trivial as the usual proof of the Hahn-Banach theorem, where the inductive step is actually a bit delicate). –  Yemon Choi Sep 28 '11 at 1:00
I believe that constructive versions of the Hahn-Banach theorem have been studied in several papers by Thierry Coquand. You might look at, e.g., his paper "Geometric Hahn-Banach Theorem" in Math. Proc. Camb. Phil. Soc. (2006), 140, 313. –  Michael A Warren Sep 28 '11 at 2:40
I was confused because this is usually optional homework on my beginning FA course. –  András Bátkai Sep 28 '11 at 7:42

The idea is to show that one can extend a linear functional from an $n$-dimensional space to a space of dimension $n+1$ without increasing its norm. See, for instance, my notes (Lemma E.2)