| author | blanchet |
| Tue, 27 Apr 2010 18:58:05 +0200 | |
| changeset 36485 | 56ce8fc56be3 |
| parent 31795 | be3e1cc5005c |
| child 36862 | 952b2b102a0a |
| permissions | -rw-r--r-- |
| 15283 | 1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
||
| 15582 | 3 |
<!-- $Id$ --> |
4 |
||
5 |
<HTML> |
|
6 |
||
7 |
<HEAD> |
|
8 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
9 |
<TITLE>HOL/Hahn_Banach/README</TITLE> |
| 15582 | 10 |
</HEAD> |
11 |
||
12 |
<BODY> |
|
| 7655 | 13 |
|
| 15283 | 14 |
<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3> |
| 7655 | 15 |
|
| 15283 | 16 |
Author: Gertrud Bauer, Technische Universität München<P> |
| 7655 | 17 |
|
18 |
This directory contains the proof of the Hahn-Banach theorem for real vectorspaces, |
|
19 |
following H. Heuser, Funktionalanalysis, p. 228 -232. |
|
20 |
The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis. |
|
21 |
It is a conclusion of Zorn's lemma.<P> |
|
22 |
||
23 |
Two different formaulations of the theorem are presented, one for general real vectorspaces |
|
24 |
and its application to normed vectorspaces. <P> |
|
25 |
||
26 |
The theorem says, that every continous linearform, defined on arbitrary subspaces |
|
27 |
(not only one-dimensional subspaces), can be extended to a continous linearform on |
|
28 |
the whole vectorspace. |
|
29 |
||
30 |
||
31 |
<HR> |
|
32 |
||
33 |
<ADDRESS> |
|
34 |
<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A> |
|
35 |
</ADDRESS> |
|
36 |
||
| 15582 | 37 |
</BODY> |
38 |
</HTML> |