src/HOL/Real/HahnBanach/document/root.tex
 changeset 11851 d190028f43c5 parent 10687 c186279eecea child 13548 36cb5fb8188c
equal inserted replaced
11850:cdfc3fce577e 11851:d190028f43c5
     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 Hahn-Banach Theorem for Real Vector Spaces}
    20 \title{The Hahn-Banach 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 Hahn-Banach Theorem is one of the most fundamental results in functional
    25   The Hahn-Banach 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 Hahn-Banach Theorem is given in \cite{Narici:1996}.
    43 Hahn-Banach 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 linear-forms, 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 non-maximal functions.
    49 supremum (w.r.t.\ the function order) and extension of non-maximal 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}