2 \documentclass[10pt,a4paper,twoside]{article}
4 \usepackage{latexsym,theorem}
5 \usepackage{isabelle,isabellesym}
6 \usepackage{pdfsetup} %last one!
11 \newcommand{\isasymsup}{\isamath{\sup\,}}
12 \newcommand{\skp}{\smallskip}
18 \pagenumbering{arabic}
20 \title{The Hahn-Banach Theorem for Real Vector Spaces}
21 \author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
25 The Hahn-Banach Theorem is one of the most fundamental results in functional
26 analysis. We present a fully formal proof of two versions of the theorem,
27 one for general linear spaces and another for normed spaces. This
28 development is based on simply-typed classical set-theory, as provided by
34 \parindent 0pt \parskip 0.5ex
39 This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
40 the informal presentation given in the textbook \cite[{\S} 36]{Heuser:1986}.
41 Another formal proof of the same theorem has been done in Mizar
42 \cite{Nowak:1993}. A general overview of the relevance and history of the
43 Hahn-Banach Theorem is given in \cite{Narici:1996}.
45 \medskip The document is structured as follows. The first part contains
46 definitions of basic notions of linear algebra: vector spaces, subspaces,
47 normed spaces, continuous linearforms, norm of functions and an order on
48 functions by domain extension. The second part contains some lemmas about the
49 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
50 With these preliminaries, the main proof of the theorem (in its two versions)
51 is conducted in the third part.
68 \part {Lemmas for the Proof}
70 \input{HahnBanachSupLemmas}
71 \input{HahnBanachExtLemmas}
72 \input{HahnBanachLemmas}
75 \part {The Main Proof}
78 \bibliographystyle{abbrv}