equal
deleted
inserted
replaced
1 
1 
2 \documentclass[10pt,a4paper,twoside]{article} 
2 \documentclass[10pt,a4paper,twoside]{article} 
3 
3 \usepackage{graphicx} 
4 \usepackage{latexsym,theorem} 
4 \usepackage{latexsym,theorem} 
5 \usepackage{isabelle,isabellesym} 
5 \usepackage{isabelle,isabellesym} 
6 \usepackage{pdfsetup} %last one! 
6 \usepackage{pdfsetup} %last one! 
7 
7 
8 \isabellestyle{it} 
8 \isabellestyle{it} 
15 \begin{document} 
15 \begin{document} 
16 
16 
17 \pagestyle{headings} 
17 \pagestyle{headings} 
18 \pagenumbering{arabic} 
18 \pagenumbering{arabic} 
19 
19 
20 \title{The HahnBanach Theorem for Real Vector Spaces} 
20 \title{The HahnBanach Theorem \\ for Real Vector Spaces} 
21 \author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}} 
21 \author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}} 
22 \maketitle 
22 \maketitle 
23 
23 
24 \begin{abstract} 
24 \begin{abstract} 
25 The HahnBanach Theorem is one of the most fundamental results in functional 
25 The HahnBanach Theorem is one of the most fundamental results in functional 
42 \cite{Nowak:1993}. A general overview of the relevance and history of the 
42 \cite{Nowak:1993}. A general overview of the relevance and history of the 
43 HahnBanach Theorem is given in \cite{Narici:1996}. 
43 HahnBanach Theorem is given in \cite{Narici:1996}. 
44 
44 
45 \medskip The document is structured as follows. The first part contains 
45 \medskip The document is structured as follows. The first part contains 
46 definitions of basic notions of linear algebra: vector spaces, subspaces, 
46 definitions of basic notions of linear algebra: vector spaces, subspaces, 
47 normed spaces, continuous linearforms, norm of functions and an order on 
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 
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. 
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) 
50 With these preliminaries, the main proof of the theorem (in its two versions) 
51 is conducted in the third part. 
51 is conducted in the third part. The dependencies of individual theories are 

52 as follows. 
52 
53 

54 \begin{center} 

55 \includegraphics[scale=0.7]{session_graph} 

56 \end{center} 
53 
57 
54 \clearpage 
58 \clearpage 
55 \part {Basic Notions} 
59 \part {Basic Notions} 
56 
60 
57 \input{Bounds} 
61 \input{Bounds} 