Editing Hahn–Banach theorem (section)

===Proof of the continuous extension theorem===

The following observations allow the [[#Hahn–Banach continuous extension theorem|continuous extension theorem]] to be deduced from the [[#Hahn–Banach theorem for real or complex vector spaces|Hahn–Banach theorem]].{{sfn|Narici|Beckenstein|2011|p=182}} 

The absolute value of a linear functional is always a seminorm. A linear functional <math>F</math> on a [[topological vector space]] <math>X</math> is continuous if and only if its absolute value <math>|F|</math> is continuous, which happens if and only if there exists a continuous seminorm <math>p</math> on <math>X</math> such that <math>|F| \leq p</math> on the domain of <math>F.</math>{{sfn|Narici|Beckenstein|2011|p=126}} 
If <math>X</math> is a locally convex space then this statement remains true when the linear functional <math>F</math> is defined on a {{em|proper}} vector subspace of <math>X.</math> 
<!-- Suppose <math>X</math> is a locally convex space whose topology is generated by a family <math>\mathcal{P}</math> of (necessarily continuous) seminorms (if <math>X</math> is a normed space then <math>\mathcal{P}</math> may be <math>\{\|\cdot\|\},</math> for instance). 
Then the topology on the vector subspace <math>M</math> is generated by the restrictions <math>\mathcal{P}\big\vert_M = \{p\big\vert_M : p \in \mathcal{P}\}</math> of these seminorms to <math>M.</math> Furthermore, for any continuous seminorm <math>q : M \to \Reals</math> on <math>M,</math> there exists some <math>p \in \mathcal{P}</math> such that <math>q \leq p.</math> --> 

{{Math proof|title=Proof of the [[#Hahn–Banach continuous extension theorem|continuous extension theorem]] for locally convex spaces{{sfn|Narici|Beckenstein|2011|p=182}}{{anchor|Proof of the continuous extension theorem for locally convex topological vector spaces}}|drop=hidden|proof=
Let <math>f</math> be a continuous linear functional defined on a vector subspace <math>M</math> of a [[locally convex topological vector space]] <math>X.</math> 
Because <math>X</math> is locally convex, there exists a continuous seminorm <math>p : X \to \Reals</math> on <math>X</math> that [[#dominated complex functional|dominates]] <math>f</math> (meaning that <math>|f(m)| \leq p(m)</math> for all <math>m \in M</math>). 
By the [[#Hahn–Banach theorem for real or complex vector spaces|Hahn–Banach theorem]], there exists a linear extension of <math>f</math> to <math>X,</math> call it <math>F,</math> that satisfies <math>|F| \leq p</math> on <math>X.</math> 
This linear functional <math>F</math> is continuous since <math>|F| \leq p</math> and <math>p</math> is a continuous seminorm.
}}

'''Proof for normed spaces'''

A linear functional <math>f</math> on a [[normed space]] is [[Continuous linear functional|continuous]] if and only if it is [[Bounded linear functional|bounded]], which means that its [[dual norm]] 
<math display=block>\|f\| = \sup \{|f(m)| : \|m\| \leq 1, m \in \operatorname{domain} f\}</math>
is finite, in which case <math>|f(m)| \leq \|f\| \|m\|</math> holds for every point <math>m</math> in its domain. 
Moreover, if <math>c \geq 0</math> is such that <math>|f(m)| \leq c \|m\|</math> for all <math>m</math> in the functional's domain, then necessarily <math>\|f\| \leq c.</math>
If <math>F</math> is a linear extension of a linear functional <math>f</math> then their dual norms always satisfy <math>\|f\| \leq \|F\|</math><ref group=proof name="ProofNormOfExtensionIsLarger" /> 
<!--(because <math display=inline>\{|f(m)| : \|m\| \leq 1, m \in \operatorname{domain} f\} \subseteq \{|F(x)| : \|x\| \leq 1, x \in \operatorname{domain} F\}</math>) -->
so that equality <math>\|f\| = \|F\|</math> is equivalent to <math>\|F\| \leq \|f\|,</math> which holds if and only if <math>|F(x)| \leq \|f\| \|x\|</math> for every point <math>x</math> in the extension's domain. 
This can be restated in terms of the function <math>\|f\| \, \|\cdot\| : X \to \Reals</math> defined by <math>x \mapsto \|f\| \, \|x\|,</math> which is always a [[seminorm]]:<ref group=note>Like every non-negative scalar multiple of a [[Norm (mathematics)|norm]], this seminorm <math>\|f\| \, \|\cdot\|</math> (the product of the non-negative real number <math>\|f\|</math> with the norm <math>\|\cdot\|</math>) is a norm when <math>\|f\|</math> is positive, although this fact is not needed for the proof.</ref>

:A linear extension of a [[bounded linear functional]] <math>f</math> is [[#norm-preserving linear extension|norm-preserving]] if and only if the extension is [[#dominated complex functional|dominated by]] the seminorm <math>\|f\| \, \|\cdot\|.</math>

Applying the [[#Hahn–Banach theorem for real or complex vector spaces|Hahn–Banach theorem]] to <math>f</math> with this seminorm <math>\|f\| \, \|\cdot\|</math> thus produces a dominated linear extension whose norm is (necessarily) equal to that of <math>f,</math> which proves the theorem:

{{Math proof|title=Proof of the [[#Norm-preserving Hahn–Banach continuous extension theorem|norm-preserving Hahn–Banach continuous extension theorem]]{{sfn|Narici|Beckenstein|2011|p=184}}|drop=hidden|proof=
Let <math>f</math> be a continuous linear functional defined on a vector subspace <math>M</math> of a normed space <math>X.</math> 
Then the function <math>p : X \to \Reals</math> defined by <math>p(x) = \|f\| \, \|x\|</math> is a seminorm on <math>X</math> that [[#dominated complex functional|dominates]] <math>f,</math> meaning that <math>|f(m)| \leq p(m)</math> holds for every <math>m \in M.</math>
By the [[#Hahn–Banach theorem for real or complex vector spaces|Hahn–Banach theorem]], there exists a linear functional <math>F</math> on <math>X</math> that extends <math>f</math> (which guarantees <math>\|f\| \leq \|F\|</math>) and that is also dominated by <math>p,</math> meaning that <math>|F(x)| \leq p(x)</math> for every <math>x \in X.</math> 
The fact that <math>\|f\|</math> is a real number such that <math>|F(x)| \leq \|f\| \|x\|</math> for every <math>x \in X,</math> guarantees <math>\|F\| \leq \|f\|.</math> 
Since <math>\|F\| = \|f\|</math> is finite, the linear functional <math>F</math> is bounded and thus continuous. 
}}