equal
deleted
inserted
replaced
1 |
1 \documentclass[10pt,a4paper,twoside]{article} |
2 \documentclass[11pt,a4paper,twoside]{article} |
2 %\documentclass[11pt,a4paper,twoside]{article} |
3 |
3 |
4 \usepackage{latexsym,theorem} |
4 \usepackage{latexsym,theorem} |
5 \usepackage{isabelle,isabellesym,bbb} |
5 \usepackage{isabelle,isabellesym,bbb} |
6 \usepackage{pdfsetup} %last one! |
6 \usepackage{pdfsetup} %last one! |
7 |
7 |
32 |
32 |
33 \clearpage |
33 \clearpage |
34 \section{Preface} |
34 \section{Preface} |
35 |
35 |
36 This is a fully formal proof of the Hahn-Banach Theorem. It closely follows |
36 This is a fully formal proof of the Hahn-Banach Theorem. It closely follows |
37 the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}. |
37 the informal presentation given in the textbook \cite[{\S} 36]{Heuser:1986}. |
38 Another formal proof of the same theorem has been done in Mizar |
38 Another formal proof of the same theorem has been done in Mizar |
39 \cite{Nowak:1993}. A general overview of the relevance and history of the |
39 \cite{Nowak:1993}. A general overview of the relevance and history of the |
40 Hahn-Banach Theorem is given in \cite{Narici:1996}. |
40 Hahn-Banach Theorem is given in \cite{Narici:1996}. |
41 |
41 |
42 \medskip The document is structured as follows. The first part contains |
42 \medskip The document is structured as follows. The first part contains |
64 \clearpage |
64 \clearpage |
65 \part {Lemmas for the Proof} |
65 \part {Lemmas for the Proof} |
66 |
66 |
67 \input{HahnBanachSupLemmas.tex} |
67 \input{HahnBanachSupLemmas.tex} |
68 \input{HahnBanachExtLemmas.tex} |
68 \input{HahnBanachExtLemmas.tex} |
|
69 \input{HahnBanachLemmas.tex} |
69 |
70 |
70 \clearpage |
71 \clearpage |
71 \part {The Main Proof} |
72 \part {The Main Proof} |
72 |
73 |
73 \input{HahnBanach.tex} |
74 \input{HahnBanach.tex} |