author wenzelm
Thu, 29 Aug 2002 16:08:32 +0200
changeset 13548 36cb5fb8188c
parent 11851 d190028f43c5
child 14721 782932b1e931
permissions -rw-r--r--
*** empty log message ***

\usepackage{pdfsetup} %last one!





\title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
\author{Gertrud Bauer \\ \url{}}

  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

\parindent 0pt \parskip 0.5ex


This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
the informal presentation given in the 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 in \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.


\part {Basic Notions}


\part {Lemmas for the Proof}


\part {The Main Proof}