|
7655
|
1 |
<HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
|
|
|
2 |
|
|
|
3 |
<H3> The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).</H3>
|
|
|
4 |
|
|
|
5 |
Author: Gertrud Bauer, Technische Universität München<P>
|
|
|
6 |
|
|
|
7 |
This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
|
|
|
8 |
following H. Heuser, Funktionalanalysis, p. 228 -232.
|
|
|
9 |
The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
|
|
|
10 |
It is a conclusion of Zorn's lemma.<P>
|
|
|
11 |
|
|
|
12 |
Two different formaulations of the theorem are presented, one for general real vectorspaces
|
|
|
13 |
and its application to normed vectorspaces. <P>
|
|
|
14 |
|
|
|
15 |
The theorem says, that every continous linearform, defined on arbitrary subspaces
|
|
|
16 |
(not only one-dimensional subspaces), can be extended to a continous linearform on
|
|
|
17 |
the whole vectorspace.
|
|
|
18 |
|
|
|
19 |
|
|
|
20 |
<HR>
|
|
|
21 |
|
|
|
22 |
<ADDRESS>
|
|
|
23 |
<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
|
|
|
24 |
</ADDRESS>
|
|
|
25 |
|
|
|
26 |
</BODY></HTML>
|
|
|
27 |
|