\title{The Hahn-Banach Theorem \\ for Real Vector Spaces} \author{Gertrud Bauer} \maketitle
\begin{abstract}
The Hahn-Banach Theorem is one of the most fundamental results in functional
analysis. We present a fully formal proof of two versions of the theorem,
one for general linear spaces and another for normed spaces. This
development is based on simply-typed classical set-theory, as provided by
Isabelle/HOL. \end{abstract}
\tableofcontents \parindent 0pt \parskip 0.5ex
\clearpage \section{Preface}
This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
the informal presentation given in Heuser's textbook \cite[{\S} 36]{Heuser:1986}.
Another formal proof of the same theorem has been done in Mizar \cite{Nowak:1993}. A general overview of the relevance and history of the
Hahn-Banach Theorem is given by Narici and Beckenstein \cite{Narici:1996}.
\medskip The document is structured as follows. The first part contains
definitions of basic notions of linear algebra: vector spaces, subspaces,
normed spaces, continuous linear-forms, norm of functions and an order on
functions by domain extension. The second part contains some lemmas about the
supremum (w.r.t.\ the function order) and extension of non-maximal functions.
With these preliminaries, the main proof of the theorem (in its two versions)
is conducted in the third part. The dependencies of individual theories are
as follows.
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.8Bemerkung:
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
