Editing Hahn–Banach theorem (section)

==Hahn–Banach theorem==

A real-valued function <math>f : M \to \R</math> defined on a subset <math>M</math> of <math>X</math> is said to be {{em|{{visible anchor|dominated real functional|text=dominated (above) by}}}} a function <math>p : X \to \R</math> if <math>f(m) \leq p(m)</math> for every <math>m \in M.</math> 
For this reason, the following version of the Hahn–Banach theorem is called {{em|the dominated [[Extension of a function|extension]] theorem}}. 

{{Math theorem
| name = {{visible anchor|Hahn–Banach dominated extension theorem}} (for real linear functionals){{sfn|Rudin|1991|pp=56-62}}<ref>{{harvnb|Rudin|1991}}, Th. 3.2</ref>{{sfn|Narici|Beckenstein|2011|pp=177-183}}
| math_statement =
If <math>p : X \to \R</math> is a [[sublinear function]] (such as a [[Norm (mathematics)|norm]] or [[seminorm]] for example) defined on a real vector space <math>X</math> then any [[linear functional]] defined on a vector subspace of <math>X</math> that is [[#dominated real functional|dominated above]] by <math>p</math> has at least one [[Linear extension (linear algebra)|linear extension]] to all of <math>X</math> that is also dominated above by <math>p.</math> 

Explicitly, if <math>p : X \to \R</math> is a [[sublinear function]], which by definition means that it satisfies 
<math display=block>p(x + y) \leq p(x) + p(y) \quad \text{ and } \quad p(t x) = t p(x) \qquad \text{ for all } \; x, y \in X \; \text{ and all real } \; t \geq 0,</math> 
and if <math>f : M \to \R</math> is a linear functional defined on a vector subspace <math>M</math> of <math>X</math> such that 
<math display=block>f(m) \leq p(m) \quad \text{ for all } m \in M</math> 
then there exists a linear functional <math>F : X \to \R</math> such that
<math display=block>F(m) = f(m) \quad \text{ for all } m \in M,</math>
<math display=block>F(x) \leq p(x) \quad ~\;\, \text{ for all } x \in X.</math> 
Moreover, if <math>p</math> is a [[seminorm]] then <math>|F(x)| \leq p(x)</math> necessarily holds for all <math>x \in X.</math> 
}}

The theorem remains true if the requirements on <math>p</math> are relaxed to require only that <math>p</math> be a [[convex function]]:{{Sfn|Schechter|1996|pp=318-319}}{{Sfn|Reed|Simon|1980|p=}}
<math display=block>p(t x + (1 - t) y) \leq t p(x) + (1 - t) p(y) \qquad \text{ for all } 0 < t < 1 \text{ and } x, y \in X.</math> 
<!-- Substituting <math>\tfrac{t}{1-t} y</math> in for <math>y</math> gives <math>p(t x + t y) \leq t p(x) + (1 - t) p\left(\tfrac{t}{1-t} y\right).</math> Substituting <math>\tfrac{1}{t} x</math> in for <math>x</math> and <math>\tfrac{1}{1-t} y</math> in for <math>y</math> gives <math>p(x + y) \leq \tfrac{p((1/t) x)}{1/t} + \tfrac{p(1/(1-t) y)}{1/(1-t)}.</math> --> 
A function <math>p : X \to \R</math> is convex and satisfies <math>p(0) \leq 0</math> if and only if <math>p(a x + b y) \leq a p(x) + b p(y)</math> for all vectors <math>x, y \in X</math> and all non-negative real <math>a, b \geq 0</math> such that <math>a + b \leq 1.</math> Every [[sublinear function]] is a convex function. 
On the other hand, if <math>p : X \to \R</math> is convex with <math>p(0) \geq 0,</math> then the function defined by <math>p_0(x) \;\stackrel{\scriptscriptstyle\text{def}}{=}\; \inf_{t > 0} \frac{p(tx)}{t}</math> is [[Homogeneous_function#Positive_homogeneity|positively homogeneous]] 
(because for all <math>x</math> and <math>r>0</math> one has <math>p_0(rx)=\inf_{t > 0} \frac{p(trx)}{t} =r\inf_{t > 0} \frac{p(trx)}{tr} = r\inf_{\tau > 0} \frac{p(\tau x)}{\tau}=rp_0(x)</math>), hence, being convex, [[Sublinear_function#Examples_and_sufficient_conditions|it is sublinear]]. It is also bounded above by <math>p_0 \leq p,</math> and satisfies <math>F \leq p_0</math> for every linear functional <math>F \leq p.</math> So the extension of the Hahn–Banach theorem to convex functionals does not have a much larger content than the classical one stated for sublinear functionals.

If <math>F : X \to \R</math> is linear then <math>F \leq p</math> if and only if{{sfn|Rudin|1991|pp=56-62}} <math display=block>-p(-x) \leq F(x) \leq p(x) \quad \text{ for all } x \in X,</math> 
which is the (equivalent) conclusion that some authors{{sfn|Rudin|1991|pp=56-62}} write instead of <math>F \leq p.</math>
It follows that if <math>p : X \to \R</math> is also {{em|symmetric}}, meaning that <math>p(-x) = p(x)</math> holds for all <math>x \in X,</math> then <math>F \leq p</math> if and only <math>|F| \leq p.</math> 
Every [[Norm (mathematics)|norm]] is a [[seminorm]] and both are symmetric [[Balanced function|balanced]] sublinear functions. A sublinear function is a seminorm if and only if it is a [[balanced function]]. On a real vector space (although not on a complex vector space), a sublinear function is a seminorm if and only if it is symmetric. The [[identity function]] <math>\R \to \R</math> on <math>X := \R</math> is an example of a sublinear function that is not a seminorm. 

===For complex or real vector spaces===

The dominated extension theorem for real linear functionals implies the following alternative statement of the Hahn–Banach theorem that can be applied to linear functionals on real or complex vector spaces. 

{{Math theorem
| name = {{visible anchor|Hahn–Banach theorem for real or complex vector spaces|text=Hahn–Banach theorem}}{{sfn|Narici|Beckenstein|2011|pp=177-220}}<ref>{{harvnb|Rudin|1991}}, Th. 3.2</ref>
| math_statement = Suppose <math>p : X \to \R</math> a [[seminorm]] on a vector space <math>X</math> over the field <math>\mathbf{K},</math> which is either <math>\R</math> or <math>\Complex.</math> 
If <math>f : M \to \mathbf{K}</math> is a linear functional on a vector subspace <math>M</math> such that 
<math display=block>|f(m)| \leq p(m) \quad \text{ for all } m \in M,</math>
then there exists a linear functional <math>F : X \to \mathbf{K}</math> such that
<math display=block>F(m) = f(m) \quad \; \text{ for all } m \in M,</math>
<math display=block>|F(x)| \leq p(x) \quad \;\, \text{ for all } x \in X.</math>
}}

The theorem remains true if the requirements on <math>p</math> are relaxed to require only that for all <math>x, y \in X</math> and all scalars <math>a</math> and <math>b</math> satisfying <math>|a| + |b| \leq 1,</math>{{Sfn|Reed|Simon|1980|p=}}
<math display=block>p(a x + b y) \leq |a| p(x) + |b| p(y).</math>
This condition holds if and only if <math>p</math> is a [[Convex function|convex]] and [[balanced function]] satisfying <math>p(0) \leq 0,</math> or equivalently, if and only if it is convex, satisfies <math>p(0) \leq 0,</math> and <math>p(u x) \leq p(x)</math> for all <math>x \in X</math> and all [[unit length]] scalars <math>u.</math> 

A complex-valued functional <math>F</math> is said to be {{em|{{visible anchor|dominated complex functional|text=dominated by <math>p</math>}}}} if <math>|F(x)| \leq p(x)</math> for all <math>x</math> in the domain of <math>F.</math> 
With this terminology, the above statements of the Hahn–Banach theorem can be restated more succinctly:

:'''Hahn–Banach dominated extension theorem''': If <math>p : X \to \R</math> is a [[seminorm]] defined on a real or complex vector space <math>X,</math> then every [[#dominated complex functional|dominated]] linear functional defined on a vector subspace of <math>X</math> has a dominated linear extension to all of <math>X.</math> In the case where <math>X</math> is a real vector space and <math>p : X \to \R</math> is merely a [[Convex function|convex]] or [[sublinear function]], this conclusion will remain true if both instances of "[[#dominated complex functional|dominated]]" (meaning <math>|F| \leq p</math>) are weakened to instead mean "[[#dominated real functional|dominated {{em|above}}]]" (meaning <math>F \leq p</math>).{{Sfn|Schechter|1996|pp=318-319}}{{Sfn|Reed|Simon|1980|p=}} 

'''Proof'''

The following observations allow the [[#Hahn–Banach dominated extension theorem|Hahn–Banach theorem for real vector spaces]] to be applied to (complex-valued) linear functionals on complex vector spaces.

Every linear functional <math>F : X \to \Complex</math> on a complex vector space is [[Linear form#Real and imaginary parts of a linear functional|completely determined]] by its [[real part]] <math>\; \operatorname{Re} F : X \to \R \;</math> through the formula{{sfn|Narici|Beckenstein|2011|pp=177-183}}<ref group=proof>If <math>z = a + i b \in \Complex</math> has real part <math>\operatorname{Re} z = a</math> then <math>- \operatorname{Re} (i z) = b,</math> which proves that <math>z = \operatorname{Re} z - i \operatorname{Re} (i z).</math> Substituting <math>F(x)</math> in for <math>z</math> and using <math>i F(x) = F(i x)</math> gives <math>F(x) = \operatorname{Re} F(x) - i \operatorname{Re} F(i x).</math> <math>\blacksquare</math></ref> 
<math display=block>F(x) \;=\; \operatorname{Re} F(x) - i \operatorname{Re} F(i x) \qquad \text{ for all } x \in X</math>
and moreover, if <math>\|\cdot\|</math> is a [[Norm (mathematics)|norm]] on <math>X</math> then their [[dual norm]]s are equal: <math>\|F\| = \|\operatorname{Re} F\|.</math>{{sfn|Narici|Beckenstein|2011|pp=126-128}} 
In particular, a linear functional on <math>X</math> extends another one defined on <math>M \subseteq X</math> if and only if their real parts are equal on <math>M</math> (in other words, a linear functional <math>F</math> extends <math>f</math> if and only if <math>\operatorname{Re} F</math> extends <math>\operatorname{Re} f</math>). 
The real part of a linear functional on <math>X</math> is always a {{visible anchor|real-linear functional}} (meaning that it is linear when <math>X</math> is considered as a real vector space) and if <math>R : X \to \R</math> is a real-linear functional on a complex vector space then <math>x \mapsto R(x) - i R(i x)</math> defines the unique linear functional on <math>X</math> whose real part is <math>R.</math> 

If <math>F</math> is a linear functional on a (complex or real) vector space <math>X</math> and if <math>p : X \to \R</math> is a seminorm then{{sfn|Narici|Beckenstein|2011|pp=177-183}}<ref group=proof>Let <math>F</math> be any [[Homogeneous function#Homogeneity|homogeneous]] scalar-valued map on <math>X</math> (such as a linear functional) and let <math>p : X \to \R</math> be any map that satisfies <math>p(u x) = p(x)</math> for all <math>x</math> and [[unit length]] scalars <math>u</math> (such as a seminorm). If <math>|F| \leq p</math> then <math>\operatorname{Re} F \leq |\operatorname{Re} F| \leq |F| \leq p.</math> For the converse, assume <math>\operatorname{Re} F \leq p</math> and fix <math>x \in X.</math> Let <math>r = |F(x)|</math> and pick any <math>\theta \in \R</math> such that <math>F(x) = r e^{i \theta};</math> it remains to show <math>r \leq p(x).</math> Homogeneity of <math>F</math> implies <math>F\left(e^{-i \theta} x\right) = r</math> is real so that <math>\operatorname{Re} F\left(e^{-i \theta} x\right) = F\left(e^{-i \theta} x\right).</math> By assumption, <math>\operatorname{Re} F \leq p</math> and <math>p\left(e^{-i \theta} x\right) = p(x),</math> so that <math>r = \operatorname{Re} F\left(e^{-i \theta} x\right) \leq p\left(e^{-i \theta} x\right) = p(x),</math> as desired. <math>\blacksquare</math></ref> 
<math display=block>|F| \,\leq\, p \quad \text{ if and only if } \quad \operatorname{Re} F \,\leq\, p.</math>
Stated in simpler language, a linear functional is [[#dominated complex functional|dominated]] by a seminorm <math>p</math> if and only if its [[#dominated real functional|real part is dominated above]] by <math>p.</math> 

{{Math proof|title=Proof of [[#Hahn–Banach theorem for real or complex vector spaces|Hahn–Banach for complex vector spaces]] by reduction to real vector spaces{{sfn|Narici|Beckenstein|2011|pp=177-220}}|drop=hidden|proof=
Suppose <math>p : X \to \R</math> is a seminorm on a complex vector space <math>X</math> and let <math>f : M \to \Complex</math> be a linear functional defined on a vector subspace <math>M</math> of <math>X</math> that satisfies <math>|f| \leq p</math> on <math>M.</math> 
Consider <math>X</math> as a real vector space and apply the [[#Hahn–Banach dominated extension theorem|Hahn–Banach theorem for real vector spaces]] to the [[#real-linear functional|real-linear functional]] <math>\; \operatorname{Re} f : M \to \R \;</math> to obtain a real-linear extension <math>R : X \to \R</math> that is also dominated above by <math>p,</math> so that it satisfies <math>R \leq p</math> on <math>X</math> and <math>R = \operatorname{Re} f</math> on <math>M.</math> 
The map <math>F : X \to \Complex</math> defined by <math>F(x) \;=\; R(x) - i R(i x)</math> is a linear functional on <math>X</math> that extends <math>f</math> (because their real parts agree on <math>M</math>) and satisfies <math>|F| \leq p</math> on <math>X</math> (because <math>\operatorname{Re} F \leq p</math> and <math>p</math> is a seminorm). 
<math>\blacksquare</math>
}}

The proof above shows that when <math>p</math> is a seminorm then there is a one-to-one correspondence between dominated linear extensions of <math>f : M \to \Complex</math> and dominated real-linear extensions of <math>\operatorname{Re} f : M \to \R;</math> the proof even gives a formula for explicitly constructing a linear extension of <math>f</math> from any given real-linear extension of its real part.

'''Continuity'''

A linear functional <math>F</math> on a [[topological vector space]]  is [[Continuous linear functional|continuous]] if and only if this is true of its real part <math>\operatorname{Re} F;</math> if the domain is a normed space then <math>\|F\| = \|\operatorname{Re} F\|</math> (where one side is infinite if and only if the other side is infinite).{{sfn|Narici|Beckenstein|2011|pp=126-128}} 
Assume <math>X</math> is a [[topological vector space]] and <math>p : X \to \R</math> is [[sublinear function]]. 
If <math>p</math> is a [[Continuity (topology)|continuous]] sublinear function that dominates a linear functional <math>F</math> then <math>F</math> is necessarily continuous.{{sfn|Narici|Beckenstein|2011|pp=177-183}} Moreover, a linear functional <math>F</math> is continuous if and only if its [[absolute value]] <math>|F|</math> (which is a [[seminorm]] that dominates <math>F</math>) is continuous.{{sfn|Narici|Beckenstein|2011|pp=177-183}} In particular, a linear functional is continuous if and only if it is dominated by some continuous sublinear function.

===Proof===

The [[#Hahn–Banach dominated extension theorem|Hahn–Banach theorem for real vector spaces]] ultimately follows from Helly's initial result for the special case where the linear functional is extended from <math>M</math> to a larger vector space in which <math>M</math> has [[codimension]] <math>1.</math>{{sfn|Narici|Beckenstein|2011|pp=177-220}}

{{Math theorem
| name = Lemma{{sfn|Narici|Beckenstein|2011|pp=177-183}}
| note = {{visible anchor|One–dimensional dominated extension theorem}}
| math_statement = Let <math>p : X \to \R</math> be a [[sublinear function]] on a real vector space <math>X,</math> let <math>f : M \to \R</math> a [[linear functional]] on a [[Proper subset|proper]] [[vector subspace]] <math>M \subsetneq X</math> such that <math>f \leq p</math> on <math>M</math> (meaning <math>f(m) \leq p(m)</math> for all <math>m \in M</math>), and let <math>x \in X</math> be a vector {{em|not}} in <math>M</math> (so <math>M \oplus \R x = \operatorname{span} \{M, x\}</math>). 
There exists a linear extension <math>F : M \oplus \R x \to \R</math> of <math>f</math> such that <math>F \leq p</math> on <math>M \oplus \R x.</math>
}}

{{Math proof|title=Proof{{sfn|Narici|Beckenstein|2011|pp=177-183}}|drop=hidden|proof=
Given any real number <math>b,</math> the map <math>F_b : M \oplus \R x \to \R</math> defined by <math>F_b(m + r x) = f(m) + r b</math> is always a linear extension of <math>f</math> to <math>M \oplus \R x</math><ref group=note>This definition means, for instance, that <math>F_b(x) = F_b(0 + 1 x) = f(0) + 1 b = b</math> and if <math>m \in M</math> then <math>F_b(m) = F_b(m + 0 x) = f(m) + 0 b = f(m).</math> In fact, if <math>G : M \oplus \R x \to \R</math> is any linear extension of <math>f</math> to <math>M \oplus \R x</math> then <math>G = F_b</math> for <math>b := G(x).</math> In other words, every linear extension of <math>f</math> to <math>M \oplus \R x</math> is of the form <math>F_b</math> for some (unique) <math>b.</math></ref> but it might not satisfy <math>F_b \leq p.</math> 
It will be shown that <math>b</math> can always be chosen so as to guarantee that <math>F_b \leq p,</math> which will complete the proof. 

If <math>m, n \in M</math> then 
<math display=block>f(m) - f(n) = f(m - n) \leq p(m - n) = p(m + x - x - n) \leq p(m + x) + p(- x - n)</math>
which implies
<math display=block>-p(-n - x) - f(n) ~\leq~ p(m + x) - f(m).</math>
<!--where importantly, the left hand side is independent of <math>m</math> and the right hand side is independent of <math>n.</math>--> 
So define
<math display=block>a = \sup_{n \in M}[-p(-n - x) - f(n)] \qquad \text{ and } \qquad c = \inf_{m \in M} [p(m + x) - f(m)]</math>
where <math>a \leq c</math> are real numbers. 
To guarantee <math>F_b \leq p,</math> it suffices that <math>a \leq b \leq c</math> (in fact, this is also necessary<ref group=note>Explicitly, for any real number <math>b \in \R,</math> <math>F_b \leq p</math> on <math>M \oplus \R x</math> if and only if <math>a \leq b \leq c.</math> Combined with the fact that <math>F_b(x) = b,</math> it follows that the dominated linear extension of <math>f</math> to <math>M \oplus \R x</math> is unique if and only if <math>a = c,</math> in which case this scalar will be the extension's values at <math>x.</math> Since every linear extension of <math>f</math> to <math>M \oplus \R x</math> is of the form <math>F_b</math> for some <math>b,</math> the bounds <math>a \leq b = F_b(x) \leq c</math> thus also limit the range of possible values (at <math>x</math>) that can be taken by any of <math>f</math>'s dominated linear extensions. Specifically, if <math>F : X \to \R</math> is any linear extension of <math>f</math> satisfying <math>F \leq p</math> then for every <math>x \in X \setminus M,</math> <math>\sup_{m \in M}[-p(-m - x) - f(m)] ~\leq~ F(x) ~\leq~ \inf_{m \in M} [p(m + x) - f(m)].</math></ref>) because then <math>b</math> satisfies "the decisive inequality"{{sfn|Narici|Beckenstein|2011|pp=177-183}}
<math display=block>-p(-n - x) - f(n) ~\leq~ b ~\leq~ p(m + x) - f(m) \qquad \text{ for all }\;  m, n \in M.</math>

To see that <math>f(m) + r b \leq p(m + r x)</math> follows,<ref group=note name="GeometricIllustration" /> assume <math>r \neq 0</math> and substitute <math>\tfrac{1}{r} m</math> in for both <math>m</math> and <math>n</math> to obtain
<math display=block>-p\left(- \tfrac{1}{r} m - x\right) - \tfrac{1}{r} f\left(m\right) ~\leq~ b ~\leq~ p\left(\tfrac{1}{r} m + x\right) - \tfrac{1}{r} f\left(m\right).</math> 
If <math>r > 0</math> (respectively, if <math>r < 0</math>) then the right (respectively, the left) hand side equals <math>\tfrac{1}{r} \left[p(m + r x) - f(m)\right]</math> so that multiplying by <math>r</math> gives <math>r b \leq p(m + r x) - f(m).</math> 
<!--<math display=block>-p\left(- \tfrac{1}{r} m - x\right) - f\left(\tfrac{1}{r} m\right) = -p\left(\left(- \tfrac{1}{r}\right) \left(m + rx\right)\right) - \tfrac{1}{r} f(m) = \tfrac{1}{r} \left[p(m + r x) - f(m)\right].</math> -->
<math>\blacksquare</math>
}}

This lemma remains true if <math>p : X \to \R</math> is merely a [[convex function]] instead of a sublinear function.{{Sfn|Schechter|1996|pp=318-319}}{{Sfn|Reed|Simon|1980|p=}} 

{{collapse top|title=Proof|left=true}}
Assume that <math>p</math> is convex, which means that <math>p(t y + (1 - t) z) \leq t p(y) + (1 - t) p(z)</math> for all <math>0 \leq t \leq 1</math> and <math>y, z \in X.</math> Let <math>M,</math> <math>f : M \to \R,</math> and <math>x \in X \setminus M</math> be as in [[Hahn–Banach theorem#One–dimensional dominated extension theorem|the lemma's statement]]. Given any <math>m, n \in M</math> and any positive real <math>r, s > 0,</math> the positive real numbers <math>t := \tfrac{s}{r + s}</math> and <math>\tfrac{r}{r + s} = 1 - t</math> sum to <math>1</math> so that the convexity of <math>p</math> on <math>X</math> guarantees
<math display=block>\begin{alignat}{9}
p\left(\tfrac{s}{r + s} m + \tfrac{r}{r + s} n\right) 
~&=~ p\big(\tfrac{s}{r + s} (m - r x) &&+ \tfrac{r}{r + s} (n + s x)\big) &&  \\
&\leq~ \tfrac{s}{r + s} \; p(m - r x) &&+ \tfrac{r}{r + s} \; p(n + s x)  && \\
\end{alignat}</math>
and hence
<math display=block>\begin{alignat}{9}
s f(m) + r f(n) 
~&=~ (r + s) \; f\left(\tfrac{s}{r + s} m + \tfrac{r}{r + s} n\right)   && \qquad \text{ by linearity of } f \\
&\leq~ (r + s) \; p\left(\tfrac{s}{r + s} m + \tfrac{r}{r + s} n\right) && \qquad f \leq p \text{ on } M \\
&\leq~ s p(m - r x) + r p(n + s x) \\
\end{alignat}</math>
thus proving that <math>- s p(m - r x) + s f(m) ~\leq~ r p(n + s x) - r f(n),</math> which after multiplying both sides by <math>\tfrac{1}{rs}</math> becomes 
<math display=block>\tfrac{1}{r} [- p(m - r x) + f(m)] ~\leq~ \tfrac{1}{s} [p(n + s x) - f(n)].</math> 
This implies that the values defined by 
<math display=block>a = \sup_{\stackrel{m \in M}{r > 0}} \tfrac{1}{r} [- p(m - r x) + f(m)] \qquad \text{ and } \qquad c = \inf_{\stackrel{n \in M}{s > 0}} \tfrac{1}{s} [p(n + s x) - f(n)]</math> 
are real numbers that satisfy <math>a \leq c.</math> As in the above proof of the [[Hahn–Banach theorem#One–dimensional dominated extension theorem|one–dimensional dominated extension theorem]] above, for any real <math>b \in \R</math> define <math>F_b : M \oplus \R x \to \R</math> by <math>F_b(m + r x) = f(m) + r b.</math> 
It can be verified that if <math>a \leq b \leq c</math> then <math>F_b \leq p</math> where <math>r b \leq p(m + r x) - f(m)</math> follows from <math>b \leq c</math> when <math>r > 0</math> (respectively, follows from <math>a \leq b</math> when <math>r < 0</math>).
<math>\blacksquare</math>
{{collapse bottom}}

The [[#One–dimensional dominated extension theorem|lemma above]] is the key step in deducing the dominated extension theorem from [[Zorn's lemma]]. 

{{Math proof|title=Proof of dominated extension theorem using [[Zorn's lemma]]|drop=hidden|proof=
The set of all possible dominated linear extensions of <math>f</math> are partially ordered by extension of each other, so there is a maximal extension <math>F.</math>  By the codimension-1 result, if <math>F</math> is not defined on all of <math>X,</math> then it can be further extended.  Thus <math>F</math> must be defined everywhere, as claimed. 
<math>\blacksquare</math>
}}

When <math>M</math> has countable codimension, then using induction and the lemma completes the proof of the Hahn–Banach theorem. The standard proof of the general case uses [[Zorn's lemma]] although the strictly weaker [[ultrafilter lemma]]{{sfn|Luxemburg|1962|p=}} (which is equivalent to the [[compactness theorem]] and to the [[Boolean prime ideal theorem]]) may be used instead. Hahn–Banach can also be proved using [[Tychonoff's theorem]] for [[Compact space|compact]] [[Hausdorff space]]s{{sfn|Łoś|Ryll-Nardzewski|1951|pp=233–237}} (which is also equivalent to the ultrafilter lemma)

The [[Mizar system|Mizar project]] has completely formalized and automatically checked the proof of the Hahn–Banach theorem in the HAHNBAN file.<ref>[http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html HAHNBAN file]</ref>