|
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">
|
|
|
9 |
<TITLE>HOL/Real/HahnBanach/README</TITLE>
|
|
|
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>
|