## 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.

Thanks in advance for any helpful answers.

-
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 2011 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 2011 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 2011 at 2:40
I was confused because this is usually optional homework on my beginning FA course. – András Bátkai Sep 28 2011 at 7:42

## 2 Answers

Same way as for the infinite dimensional case, except you avoid Zorn's lemma by counting dimensions.

-
Isn't the whole thing trivial as soon as you know that your subspace is complemented? – András Bátkai Sep 27 2011 at 20:52
Preserving norms isn't trivial. – Benjamin Hayes Sep 27 2011 at 20:54

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)

In fact, by doing so, you can prove THBT constructively for any separable space.

-