10687

1 

9375

2 
\documentclass[10pt,a4paper,twoside]{article}

11851

3 
\usepackage{graphicx}

7917

4 
\usepackage{latexsym,theorem}

10687

5 
\usepackage{isabelle,isabellesym}

7984

6 
\usepackage{pdfsetup} %last one!

10687

7 


8 
\isabellestyle{it}

9659

9 
\urlstyle{rm}

7747

10 

10687

11 
\newcommand{\isasymsup}{\isamath{\sup\,}}


12 
\newcommand{\skp}{\smallskip}


13 

7808

14 

7747

15 
\begin{document}


16 

7917

17 
\pagestyle{headings}


18 
\pagenumbering{arabic}


19 

11851

20 
\title{The HahnBanach Theorem \\ for Real Vector Spaces}

7978

21 
\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}


22 
\maketitle

7747

23 

7808

24 
\begin{abstract}

7978

25 
The HahnBanach Theorem is one of the most fundamental results in functional

7927

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 simplytyped classical settheory, as provided by


29 
Isabelle/HOL.

7808

30 
\end{abstract}


31 

7927

32 

7808

33 
\tableofcontents

7927

34 
\parindent 0pt \parskip 0.5ex


35 


36 
\clearpage


37 
\section{Preface}

7808

38 

7978

39 
This is a fully formal proof of the HahnBanach Theorem. It closely follows

9375

40 
the informal presentation given in the textbook \cite[{\S} 36]{Heuser:1986}.

7927

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

7978

43 
HahnBanach Theorem is given in \cite{Narici:1996}.

7927

44 


45 
\medskip The document is structured as follows. The first part contains


46 
definitions of basic notions of linear algebra: vector spaces, subspaces,

11851

47 
normed spaces, continuous linearforms, norm of functions and an order on

7927

48 
functions by domain extension. The second part contains some lemmas about the


49 
supremum (w.r.t.\ the function order) and extension of nonmaximal functions.


50 
With these preliminaries, the main proof of the theorem (in its two versions)

11851

51 
is conducted in the third part. The dependencies of individual theories are


52 
as follows.

7927

53 

11851

54 
\begin{center}

13548

55 
\includegraphics[scale=0.5]{session_graph}

11851

56 
\end{center}

7927

57 


58 
\clearpage


59 
\part {Basic Notions}

7917

60 

10687

61 
\input{Bounds}


62 
\input{Aux}


63 
\input{VectorSpace}


64 
\input{Subspace}


65 
\input{NormedSpace}


66 
\input{Linearform}


67 
\input{FunctionOrder}


68 
\input{FunctionNorm}


69 
\input{ZornLemma}

7917

70 

7927

71 
\clearpage


72 
\part {Lemmas for the Proof}

7917

73 

10687

74 
\input{HahnBanachSupLemmas}


75 
\input{HahnBanachExtLemmas}


76 
\input{HahnBanachLemmas}

7917

77 

7927

78 
\clearpage


79 
\part {The Main Proof}

7917

80 

10687

81 
\input{HahnBanach}

7917

82 
\bibliographystyle{abbrv}

7927

83 
\bibliography{root}

7747

84 


85 
\end{document}
