Editing Hahn–Banach theorem (section)

===For seminorms===

{{Math theorem
| name = {{visible anchor|Hahn–Banach theorem for seminorms}}{{sfn|Wilansky|2013|pp=18-21}}{{sfn|Narici|Beckenstein|2011|pp=150}}
| math_statement = If <math>p : M \to \Reals</math> is a [[seminorm]] defined on a vector subspace <math>M</math> of <math>X,</math> and if <math>q : X \to \Reals</math> is a seminorm on <math>X</math> such that <math>p \leq q\big\vert_M,</math> then there exists a seminorm <math>P : X \to \Reals</math> on <math>X</math> such that <math>P\big\vert_M = p</math> on <math>M</math> and <math>P \leq q</math> on <math>X.</math>
}}

{{Math proof|title=Proof of the [[#Hahn–Banach theorem for seminorms|Hahn–Banach theorem for seminorms]]|drop=hidden|proof=
Let <math>S</math> be the convex hull of <math>\{m \in M : p(m) \leq 1\} \cup \{x \in X : q(x) \leq 1\}.</math> Because <math>S</math> is an [[Absorbing set|absorbing]] [[Absolutely convex set|disk]] in <math>X,</math> its [[Minkowski functional]] <math>P</math> is a seminorm. Then <math>p = P</math> on <math>M</math> and <math>P \leq q</math> on <math>X.</math>
}}

So for example, suppose that <math>f</math> is a [[bounded linear functional]] defined on a vector subspace <math>M</math> of a [[normed space]] <math>X,</math> so its the [[operator norm]] <math>\|f\|</math> is a non-negative real number. 
Then the linear functional's [[absolute value]] <math>p := |f|</math> is a seminorm on <math>M</math> and the map <math>q : X \to \Reals</math> defined by <math>q(x) = \|f\| \, \|x\|</math> is a seminorm on <math>X</math> that satisfies <math>p \leq q\big\vert_M</math> on <math>M.</math> 
The [[#Hahn–Banach theorem for seminorms|Hahn–Banach theorem for seminorms]] guarantees the existence of a seminorm <math>P : X \to \Reals</math> that is equal to <math>|f|</math> on <math>M</math> (since <math>P\big\vert_M = p = |f|</math>) and is bounded above by <math>P(x) \leq \|f\| \, \|x\|</math> everywhere on <math>X</math> (since <math>P \leq q</math>).