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