Updated files to remove 0r and 1r from theorems in descendant theories
of RealBin. Some new theorems added.
\documentclass[11pt,a4paper,twoside]{article}
\usepackage{latexsym,theorem}
\usepackage{isabelle,isabellesym,bbb}
\usepackage{pdfsetup} %last one!
\input{notation}
\begin{document}
\pagestyle{headings}
\pagenumbering{arabic}
\title{The Hahn-Banach Theorem for Real Vector Spaces}
\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
\maketitle
\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 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 linearforms, 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.
\clearpage
\part {Basic Notions}
\input{Bounds.tex}
\input{Aux.tex}
\input{VectorSpace.tex}
\input{Subspace.tex}
\input{NormedSpace.tex}
\input{Linearform.tex}
\input{FunctionOrder.tex}
\input{FunctionNorm.tex}
\input{ZornLemma.tex}
\clearpage
\part {Lemmas for the Proof}
\input{HahnBanachSupLemmas.tex}
\input{HahnBanachExtLemmas.tex}
\clearpage
\part {The Main Proof}
\input{HahnBanach.tex}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}