Hahn-Banach theorem

The most general formulation of the theorem needs some preparations. If V is a vector space over the scalar field K (either the real numbers R or the complex numbers C), we call a function N : V -> R sublinear if N(ax + by) ≤ |a| N(x) + |b| N(y) for all x and y in V and all scalars a and b in K. Every norm on V is sublinear, but there are other examples.

The Hahn-Banach theorem states that:

Let N : V -> R be sublinear, let U be a subspace of V and let φ : U -> K be a linear functional such that |φ(x)| ≤ N(x) for all x in U. Then there exists a linear map ψ : V -> K which extends φ (meaning ψ(x) = φ(x) for all x in U) and which is dominated by N on all of V (meaning |ψ(x)| ≤ N(x) for all x in V).

The extension ψ is in general not uniquely specified by φ and the proof gives no method as to how to find ψ: it depends on Zorn's lemma.

Several important consequences of the theorem are also sometimes called "Hahn-Banach theorem":

• If V is a normed vector space with subspace U (not necessarily closed) and if φ : U -> K is continuous and linear, then there exists an extension ψ : V -> K of φ which is also continuous and linear and which has the same norm as φ (see Banach space for a discussion of the norm of a linear map).
• If V is a normed vector space with subspace U (not necessarily closed) and if z is an element of V not in the closure of U, then there exists a continuous linear map ψ : V -> K with ψ(x) = 0 for all x in U, ψ(z) = 1, and ||ψ|| = ||z||^-1.

The Mizar project has completely formalized and automatically checked the proof of the Hahn-Banach theorem in the HAHNBAN file (http://mizar.uwb.edu.pl/JFM/Vol5/hahnban).