The Hahn-Banach theorem is rightly seen as one of the Big Theorems in functional analysis. Indeed, it can be said to be where functional analysis really starts. But as it's one of those "there exists ..." theorems that doesn't give you any information as to how to find it; indeed, it's quite usual when teaching it to introduce the separable case first (which is reasonably constructive) before going on to the full theorem. So it's real use is in situations where just knowing the functional exists is enough - if you can write down a functional that does the job then there's no need for the Hahn-Banach Theorem.

So my question is: what's a good example of a space where you need the Hahn-Banach theorem?

Ideally the space itself shouldn't be too difficult to express, and normed vector spaces are preferable to non-normed ones (a good non-normed vector space would still be nice to know but would be of less use pedagogically).

**Edit:** It seems wrong to accept one of these answers as "the" answer so I'm not going to do that. If forced, I would say that $\ell^\infty$ is the best example: it's probably the easiest non-separable space to think about and, as I've learnt, it does **need** the Hahn-Banach theorem.

Incidentally, one thing that wasn't said, and which I forgot about when asking the question, was that such an example is by necessity going to be non-separable since *countable* Hahn-Banach is provable merely with induction.

needthe Hahn-Banach" theorem. For one, it is an abstract thing, and it sound weird to say that has needs. The question rather should be: does a mathematician need to use the Hahn-Banach Theorem (or axiom here), in order to produce a continuous linear form outside $\ell^1$. I have never felt this need, but others could perhaps inform me about why they need such a thing. $\endgroup$