ハーン–バナッハの定理
一般には、拡張 ψ は φ によって一意に定まるものではなく、また、定理の証明を見ても ψ を見つける明示的な方法は分からない。無限次元空間 V の場合には、選択公理の一形態であるツォルンの補題が、証明に必要とされる。
(Reed & Simon 1980)によれば、 N {\displaystyle \scriptstyle {\mathcal {N}}} に対する劣線形性の条件は、条件
N ( a x + b y ) ≤ | a | N ( x ) + | b | N ( y ) , x , y ∈ V , | a | + | b | ≤ 1 {\displaystyle {\mathcal {N}}(ax+by)\leq |a|\,{\mathcal {N}}(x)+|b|\,{\mathcal {N}}(y),\qquad x,y\in V,\quad |a|+|b|\leq 1}
に、少し弱めることが出来る。この条件は、ハーン–バナッハの定理と凸性の間の深い関係を明らかにするものである。
Mizarプロジェクトは、ハーン–バナッハの定理の完全な定式化と自動検証された証明をHAHNBAN fileに有している。