ハーン–バナッハの定理
数学におけるハーン–バナッハの定理（ハーン–バナッハのていり、）は、関数解析学の分野における中心的な道具で、ベクトル空間の部分空間上で定義される有界線形汎関数が全空間へ拡張できることについて述べたものである。これにより、どのようなノルム線形空間においても、その上で定義される連続線形汎関数が、双対空間の研究を「面白い」ものにするに「十分」なほどたくさんあることがわかる。ハーン-バナッハの定理の別形態のものとして、ハーン–バナッハの分離定理あるいは分離超平面定理と呼ばれるものがあり、の分野で多く用いられている。
定理の名前の由来は、1920年代後半にそれぞれ独立にこの定理を証明したハンス・ハーンとステファン・バナッハである。定理の特別な場合については、より早い段階（1912年）でエードゥアルト・ヘリーによって証明されており、またこの定理が導出されるようなある一般の拡張定理が、1923年にマルツェル・リースによって証明されていた。
定理の最も一般な定式化においては、いくつかの準備が必要とされる。実数体 R 上のベクトル空間 "V" に対し、関数 がであるとは、
が成立することを言う。
"V" 上のすべての半ノルム（特に、"V" 上のすべてのノルム）は劣線形である。他の劣線形関数、特に凸集合のミンコフスキー汎関数なども同様に有用なものとなりうる。
ハーン–バナッハの定理の別形態は次のようなものである: "V" を係数体 K （実数 R あるいは複素数 C）上のベクトル空間とし、formula_4 を半ノルムとし、φ: "U" → K を "V" の K-線形部分空間 "U" 上の K-線形汎関数とし、"U" 上ではその絶対値が formula_5 によって支配されるもの、すなわち
が成立するものとする。このとき、φ には全空間 "V" への線形拡張 ψ: "V" → K が存在する。すなわち、次を満たすような K-線形汎関数 ψ が存在する:
この定理の複素数の場合において C-線形性を仮定として要求するということは、実数の場合での仮定に、すべてのベクトル "x" ∈ "U" に対して、ベクトル も "U" に属し、 が成立するという仮定を加えて要求するということである。
一般には、拡張 ψ は φ によって一意に定まるものではなく、また、定理の証明を見ても ψ を見つける明示的な方法は分からない。無限次元空間 "V" の場合には、選択公理の一形態であるツォルンの補題が、証明に必要とされる。
によれば、formula_5 に対する劣線形性の条件は、条件
に、少し弱めることが出来る。この条件は、ハーン–バナッハの定理と凸性の間の深い関係を明らかにするものである。
Mizarプロジェクトは、ハーン–バナッハの定理の完全な定式化と自動検証された証明をHAHNBAN fileに有している。
この定理にはいくつかの重要な帰結が存在し、しばしばそれらも「ハーン–バナッハの定理」と呼ばれることがある。ハーン–バナッハの定理の別形態のものとして、ハーン–バナッハの分離定理というものが知られている 。この定理は、最適化理論、経済学の分野で幅広く用いられている。上述のように、選択公理からハーン–バナッハの定理は従うが、その逆は真ではない。このことを示す一つの方法としては、選択公理よりも真に弱いからハーン・バナッハの定理を証明することができるが、この場合その逆は成り立たないということに着目すればよい。ハーン–バナッハの定理は、実は、ウルトラフィルターの補題よりもさらに弱い仮定を用いて証明することも出来る。 
更に、ブラウンとシンプソンは、弱ケーニヒの補題を公理の一つとするの部分体系WKL から可分なバナッハ空間上の有界線型汎関数に対するハーン-バナッハの定理がしたがう、ということを証明した。
ハーン–バナッハの定理の帰結として、次のようなものも存在する。