--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Oct 25 19:24:43 1999 +0200
@@ -12,7 +12,7 @@
text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$
is \emph{continous}, iff it is bounded, i.~e.
\[\exists\ap c\in R.\ap \forall\ap x\in V.\ap
-|f\ap x| \leq c \cdot \norm x.\]
+|f\ap x| \leq c \cdot \norm x\]
In our application no other functions than linearforms are considered,
so we can define continous linearforms as follows:
*};
@@ -48,15 +48,15 @@
is called the \emph{norm} of $f$.
For the non-trivial vector space $V$ the norm can be defined as
-\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}. \]
+\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \]
-For the case that the vector space $V$ contains only the zero vector
-set, the set $B$ this supremum is taken from would be empty, and any
-real number is a supremum of $B$. So it must be guarateed that there
-is an element in $B$. This element must be greater or equal $0$ so
-that $\idt{function{\dsh}norm}$ has the norm properties. Furthermore
-it does not have to change the norm in all other cases, so it must be
-$0$, as all other elements of $B$ are greater or equal $0$.
+For the case that the vector space $V$ contains only the $\zero$
+vector, the set $B$ this supremum is taken from would be empty, and
+any real number is a supremum of $B$. So it must be guarateed that
+there is an element in $B$. This element must be ${} \ge 0$ so that
+$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
+does not have to change the norm in all other cases, so it must be
+$0$, as all other elements of $B$ are ${} \ge 0$.
Thus $B$ is defined as follows.
*};
@@ -250,7 +250,7 @@
txt{* The proof is by case analysis on $x$. *};
- show "?thesis";
+ show ?thesis;
proof (rule case_split);
txt {* For the case $x = \zero$ the thesis follows
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Oct 25 19:24:43 1999 +0200
@@ -12,11 +12,11 @@
text{* We define the \emph{graph} of a (real) function $f$ with the
domain $F$ as the set
-\begin{matharray}{l}
-\{(x, f\ap x). \ap x:F\}.
-\end{matharray}
+\[
+\{(x, f\ap x). \ap x:F\}
+\]
So we are modelling partial functions by specifying the domain and
-the mapping function. We use the notion 'function' also for the graph
+the mapping function. We use the notion ``function'' also for the graph
of a function.
*};
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Oct 25 19:24:43 1999 +0200
@@ -10,7 +10,7 @@
text {*
We present the proof of two different versions of the Hahn-Banach
- Theorem, closely following \cite{Heuser:1986}.
+ Theorem, closely following \cite[\S36]{Heuser:1986}.
*};
subsection {* The case of general linear spaces *};
@@ -49,7 +49,7 @@
the union of all functions in the chain is again a norm preserving
function. (The union is an upper bound for all elements.
It is even the least upper bound, because every upper bound of $M$
- is also an upper bound for $\cup\; c$.) *};
+ is also an upper bound for $\Union c$.) *};
have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";
proof -;
@@ -91,7 +91,7 @@
qed;
qed;
- txt {* According to Zorn's Lemma there exists
+ txt {* According to Zorn's Lemma there is
a maximal norm-preserving extension $g\in M$. *};
with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
@@ -283,7 +283,7 @@
thus ?thesis; ..;
qed;
- txt {* We have shown, that $h$ can still be extended to
+ txt {* We have shown that $h$ can still be extended to
some $h_0$, in contradiction to the assumption that
$h$ is a maximal element. *};
@@ -293,7 +293,7 @@
thus ?thesis; by contradiction;
qed;
-txt{* It follows $H = E$ and the thesis can be shown. *};
+txt{* It follows $H = E$, and the thesis can be shown. *};
show "is_linearform E h & (ALL x:F. h x = f x)
& (ALL x:E. h x <= p x)";
@@ -372,8 +372,8 @@
txt{* We define the function $p$ on $E$ as follows:
\begin{matharray}{l}
- p\ap x = \fnorm f * \norm x\\
- % p\ap x = \fnorm f * \fnorm x.\\
+ p\ap x = \fnorm f \cdot \norm x\\
+ % p\ap x = \fnorm f \cdot \fnorm x\\
\end{matharray}
*};
@@ -408,7 +408,7 @@
finally; show ?thesis; .;
qed;
- txt{* Furthermore $p$ obeys the triangle inequation: *};
+ txt{* Furthermore, $p$ obeys the triangle inequation: *};
show "p (x + y) <= p x + p y";
proof -;
@@ -478,7 +478,7 @@
a solution
for the inequation
\begin{matharray}{l}
- \forall\ap x\in E.\ap |g\ap x| \leq c * \norm x.
+ \forall\ap x\in E.\ap |g\ap x| \leq c \cdot \norm x
\end{matharray} *};
have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Oct 25 19:24:43 1999 +0200
@@ -3,7 +3,7 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Extending a non-ma\-xi\-mal function *};
+header {* Extending a non-maximal function *};
theory HahnBanachExtLemmas = FunctionNorm:;
@@ -30,7 +30,7 @@
\end{matharray}
it suffices to show that
\begin{matharray}{l}
-\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v.
+\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v
\end{matharray}
*};
@@ -84,7 +84,7 @@
show ?thesis;
proof (intro exI conjI ballI);
- txt {* For all $y\in F$ is $a\ap y \leq \xi$. *};
+ txt {* For all $y\in F$ holds $a\ap y \leq \xi$. *};
fix y; assume y: "y:F";
show "a y <= xi";
@@ -93,7 +93,7 @@
qed (force!);
next;
- txt {* For all $y\in F$ is $\xi\leq b\ap y$. *};
+ txt {* For all $y\in F$ holds $\xi\leq b\ap y$. *};
fix y; assume "y:F";
show "xi <= b y";
@@ -115,8 +115,8 @@
qed;
qed;
-text{* The function $h_0$ is defined as a linear extension of $h$
-to $H_0$. $h_0$ is linear. *};
+text{* The function $h_0$ is defined as a canonical linear extension
+of $h$ to $H_0$. *};
lemma h0_lf:
"[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
@@ -142,7 +142,7 @@
fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
txt{* We now have to show that $h_0$ is linear
- w.~r.~t.~addition, i.~e.~
+ w.~r.~t.~addition, i.~e.\
$h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
for $x_1, x_2\in H$. *};
@@ -192,8 +192,8 @@
txt{* We further have to show that $h_0$ is linear
w.~r.~t.~scalar multiplication,
- i.~e.~ $c\in real$ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
- for $x\in H$ and real $c$.
+ i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
+ for $x\in H$ and any real number $c$.
*};
next;
@@ -268,7 +268,7 @@
by (rule h0_definite);
txt{* Now we show
- $h\ap y + a * xi\leq p\ap (y\plus a \mult x_0)$
+ $h\ap y + a \cdot xi\leq p\ap (y\plus a \mult x_0)$
by case analysis on $a$. *};
also; have "... <= p (y + a <*> x0)";
@@ -278,7 +278,7 @@
with vs y a; show ?thesis; by simp;
txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
- $\frac{y}{a}$. *};
+ $y/a$. *};
next;
assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
@@ -308,7 +308,7 @@
thus ?thesis; by simp;
txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
- as $\frac{y}{a}$. *};
+ as $y/a$. *};
next;
assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon Oct 25 19:24:43 1999 +0200
@@ -15,7 +15,7 @@
Let $E$ be a real vector space with a quasinorm $q$ on $E$.
$F$ is a subspace of $E$ and $f$ a linearform on $F$. We
consider a chain $c$ of norm preserving extensions of $f$, such that
-$\cup\; c = \idt{graph}\ap H\ap h$.
+$\Union c = \idt{graph}\ap H\ap h$.
We will show some properties about the limit function $h$,
i.~e.~the supremum of the chain $c$.
*};
@@ -348,8 +348,8 @@
thus ?thesis;
proof (elim UnionE chainE2);
- txt{* Since both $(x, y) \in \cup\; c$ and $(x, z) \in cup c$
- they are menbers of some graphs $G_1$ and $G_2$, resp.~, such that
+ txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
+ they are members of some graphs $G_1$ and $G_2$, resp., such that
both $G_1$ and $G_2$ are members of $c$*};
fix G1 G2; assume
@@ -390,13 +390,11 @@
qed;
qed;
-text{* The limit function $h$ is linear: Every element $x$
-in the domain of $h$ is in the domain of
-a function $h'$ in the chain of norm preserving extensions.
-Futher $h$ is an extension of $h'$ so the value
-of $x$ are identical for $h'$ and $h$.
-Finally, the function $h'$ is linear by construction of $M$.
-*};
+text{* The limit function $h$ is linear: every element $x$ in the
+domain of $h$ is in the domain of a function $h'$ in the chain of norm
+preserving extensions. Furthermore, $h$ is an extension of $h'$ so
+the value of $x$ are identical for $h'$ and $h$. Finally, the
+function $h'$ is linear by construction of $M$. *};
lemma sup_lf:
"[| M = norm_pres_extensions E p F f; c: chain M;
@@ -439,7 +437,7 @@
by (rule some_H'h');
txt{* We have to show that h is linear w.~r.~t.
- skalar multiplication. *};
+ scalar multiplication. *};
thus "h (a <*> x) = a * h x";
proof (elim exE conjE);
@@ -494,10 +492,10 @@
qed;
qed;
-text{* The domain $H$ of the limit function is a superspace
-of $F$, since $F$ is a subset of $H$. The existence of
-the $\zero$ element in $F$ and the closeness properties
-follow from the fact that $F$ is a vectorspace. *};
+text{* The domain $H$ of the limit function is a superspace of $F$,
+since $F$ is a subset of $H$. The existence of the $\zero$ element in
+$F$ and the closure properties follow from the fact that $F$ is a
+vectorspace. *};
lemma sup_supF:
"[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
@@ -528,7 +526,7 @@
qed;
qed;
-text{* The domain $H$ of the limt function is a subspace
+text{* The domain $H$ of the limit function is a subspace
of $E$. *};
lemma sup_subE:
@@ -588,7 +586,7 @@
qed;
qed;
- txt{* $H$ is closed under skalar multiplication. *};
+ txt{* $H$ is closed under scalar multiplication. *};
show "ALL x:H. ALL a. a <*> x : H";
proof (intro ballI allI);
@@ -610,8 +608,8 @@
qed;
qed;
-text {* The limit functon is bounded by
-the norm $p$ as well, simce all elements in the chain are norm preserving.
+text {* The limit function is bounded by
+the norm $p$ as well, since all elements in the chain are norm preserving.
*};
lemma sup_norm_pres:
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Mon Oct 25 19:24:43 1999 +0200
@@ -72,7 +72,8 @@
subsection {* Norms *};
-text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only $\zero$ to $0$. *};
+text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the
+$\zero$ vector to $0$. *};
constdefs
is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
--- a/src/HOL/Real/HahnBanach/README.html Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/README.html Mon Oct 25 19:24:43 1999 +0200
@@ -1,6 +1,6 @@
<HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
-<H3> The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).</H3>
+<H3> The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).</H3>
Author: Gertrud Bauer, Technische Universität München<P>
--- a/src/HOL/Real/HahnBanach/ROOT.ML Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML Mon Oct 25 19:24:43 1999 +0200
@@ -2,7 +2,7 @@
ID: $Id$
Author: Gertrud Bauer, TU Munich
-The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
+The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
*)
time_use_thy "Bounds";
--- a/src/HOL/Real/HahnBanach/Subspace.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Mon Oct 25 19:24:43 1999 +0200
@@ -213,9 +213,8 @@
instance set :: (plus) plus; by intro_classes;
defs vs_sum_def:
- "U + V == {x. EX u:U. EX v:V. x = u + v}";
+ "U + V == {x. EX u:U. EX v:V. x = u + v}";(***
-(***
constdefs
vs_sum ::
"['a::{minus, plus} set, 'a set] => 'a set" (infixl "+" 65)
@@ -318,7 +317,7 @@
text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero
element is the only common element of $U$ and $V$. For every element
$x$ of the direct sum of $U$ and $V$ the decomposition in
-$x = u + v$ with $u:U$ and $v:V$ is unique.*};
+$x = u + v$ with $u \in U$ and $v \in V$ is unique.*};
lemma decomp:
"[| is_vectorspace E; is_subspace U E; is_subspace V E;
@@ -352,7 +351,7 @@
text {* An application of the previous lemma will be used in the
proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$
of the direct sum of a vectorspace $H$ and the linear closure of
-$x_0$ the components $y:H$ and $a$ are unique. *};
+$x_0$ the components $y \in H$ and $a$ are unique. *};
lemma decomp_H0:
"[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
@@ -426,7 +425,7 @@
text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$
are unique, so the function $h_0$ defined by
-$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *};
+$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
lemma h0_definite:
"[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Oct 25 19:24:43 1999 +0200
@@ -9,9 +9,10 @@
subsection {* Signature *};
-text {* For the definition of real vector spaces a type $\alpha$ is
-considered, on which the operations addition and real scalar
-multiplication are defined, and which has an zero element.*};
+text {* For the definition of real vector spaces a type $\alpha$
+of the sort $\idt{plus}, \idt{minus}$ is considered, on which a
+real scalar multiplication $\mult$ is defined, and which has an zero
+element $\zero$.*};
consts
(***
@@ -24,8 +25,9 @@
prod :: "[real, 'a] => 'a" (infixr "\<prod>" 70)
zero :: 'a ("\<zero>");
-text {* The unary and binary minus can be considered as
+(* text {* The unary and binary minus can be considered as
abbreviations: *};
+*)
(***
constdefs
@@ -37,15 +39,14 @@
subsection {* Vector space laws *};
-text {* A \emph{vector space} is a non-empty set $V$ of elements
-from $\alpha$ with the following vector space laws:
-The set $V$ is closed under addition and scalar multiplication,
-addition is associative and commutative. $\minus x$ is the inverse
-of $x$ w.~r.~t.~addition and $\zero$ is the neutral element of
-addition.
-Addition and multiplication are distributive.
-Scalar multiplication is associative and the real $1$ is the neutral
-element of scalar multiplication.
+text {* A \emph{vector space} is a non-empty set $V$ of elements from
+ $\alpha$ with the following vector space laws: The set $V$ is closed
+ under addition and scalar multiplication, addition is associative
+ and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
+ and $\zero$ is the neutral element of addition. Addition and
+ multiplication are distributive; scalar multiplication is
+ associative and the real $1$ is the neutral element of scalar
+ multiplication.
*};
constdefs
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Mon Oct 25 19:24:43 1999 +0200
@@ -13,8 +13,8 @@
In our application $S$ is a set of sets, ordered by set inclusion. Since
the union of a chain of sets is an upperbound for all elements of the
chain, the conditions of Zorn's lemma can be modified:
-If $S$ is non-empty, it suffices to show that for every non-empty
-chain $c$ in $S$ the union of $c$ also lies in $S$:
+if $S$ is non-empty, it suffices to show that for every non-empty
+chain $c$ in $S$ the union of $c$ also lies in $S$.
*};
theorem Zorn's_Lemma:
@@ -35,7 +35,7 @@
assume "c={}";
with aS; show ?thesis; by fast;
- txt{* If $c$ is non-empty, then $\cup\; c$
+ txt{* If $c$ is non-empty, then $\Union c$
is an upperbound of $c$, that lies in $S$. *};
next;
--- a/src/HOL/Real/HahnBanach/document/notation.tex Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Mon Oct 25 19:24:43 1999 +0200
@@ -2,7 +2,7 @@
\renewcommand{\isamarkupheader}[1]{\section{#1}}
\newcommand{\isasymbollambda}{${\mathtt{\lambda}}$}
-\parindent 0pt \parskip 0.5ex
+
\newcommand{\name}[1]{\textsf{#1}}
@@ -34,16 +34,17 @@
\newcommand{\Le}{\le}
\newcommand{\Lt}{\lt}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\ap}{\mathbin{\!}}
+\newcommand{\ap}{\mathbin{}}
+\newcommand{\Union}{\bigcup}
-\newcommand{\norm}[1]{\|\, #1\,\|}
-\newcommand{\fnorm}[1]{\|\, #1\,\|}
-\newcommand{\zero}{{\mathord{\mathbf {0}}}}
-\newcommand{\plus}{{\mathbin{\;\mathtt {+}\;}}}
-\newcommand{\minus}{{\mathbin{\;\mathtt {-}\;}}}
-\newcommand{\mult}{{\mathbin{\;\mathbf {\odot}\;}}}
-\newcommand{\1}{{\mathord{\mathrm{1}}}}
+\newcommand{\norm}[1]{\left\|#1\right\|}
+\newcommand{\fnorm}[1]{\left\|#1\right\|}
+\newcommand{\zero}{\mathord{\mathbf 0}}
+\newcommand{\plus}{\mathbin{\mathbf +}}
+\newcommand{\minus}{\mathbin{\mathbf -}}
+\newcommand{\mult}{\mathbin{\mathbf\odot}}
+\newcommand{\1}{\mathord{\mathrm{1}}}
%\newcommand{\zero}{{\mathord{\small\sl\tt {<0>}}}}
%\newcommand{\plus}{{\mathbin{\;\small\sl\tt {[+]}\;}}}
%\newcommand{\minus}{{\mathbin{\;\small\sl\tt {[-]}\;}}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/document/root.bib Mon Oct 25 19:24:43 1999 +0200
@@ -0,0 +1,27 @@
+
+@Book{Heuser:1986,
+ author = {H. Heuser},
+ title = {Funktionalanalysis: Theorie und Anwendung},
+ publisher = {Teubner},
+ year = 1986
+}
+
+@InCollection{Narici:1996,
+ author = {L. Narici and E. Beckenstein},
+ title = {The {Hahn-Banach Theorem}: The Life and Times},
+ booktitle = {Topology Atlas},
+ publisher = {York University, Toronto, Ontario, Canada},
+ year = 1996,
+ note = {\url{http://at.yorku.ca/topology/preprint.htm} and
+ \url{http://at.yorku.ca/p/a/a/a/16.htm}}
+}
+
+@Article{Nowak:1993,
+ author = {B. Nowak and A. Trybulec},
+ title = {{Hahn-Banach} Theorem},
+ journal = {Journal of Formalized Mathematics},
+ year = {1993},
+ volume = {5},
+ institution = {University of Bialystok},
+ note = {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}}
+}
--- a/src/HOL/Real/HahnBanach/document/root.tex Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Mon Oct 25 19:24:43 1999 +0200
@@ -12,32 +12,42 @@
\pagestyle{headings}
\pagenumbering{arabic}
-\title{The Hahn-Banach Theorem for Real Vectorspaces}
+\title{The Hahn-Banach Theorem for Real Vector Spaces}
\author{Gertrud Bauer}
\maketitle
\begin{abstract}
-The Hahn-Banach theorem is one of the most important theorems
-of functional analysis. We present the fully formal proof of two versions of
-the theorem, one for general linear spaces and one for normed spaces
-as a corollary of the first.
-
-The first part contains the definition of basic notions of
-linear algebra, such as vector spaces, subspaces, normed spaces,
-continous 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 the extension of a non-maximal function,
-which are needed for the proof of the main theorem.
-
-The third part is the proof of the theorem in its two different versions.
-
+ 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}
-\part {Basic notions}
+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}
@@ -49,15 +59,17 @@
\input{FunctionNorm.tex}
\input{ZornLemma.tex}
-\part {Lemmas for the proof}
+\clearpage
+\part {Lemmas for the Proof}
\input{HahnBanachSupLemmas.tex}
\input{HahnBanachExtLemmas.tex}
-\part {The proof}
+\clearpage
+\part {The Main Proof}
\input{HahnBanach.tex}
\bibliographystyle{abbrv}
-\bibliography{bib}
+\bibliography{root}
\end{document}