equal
deleted
inserted
replaced
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
2 |
|
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> |
|
13 |
|
14 <H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3> |
|
15 |
|
16 Author: Gertrud Bauer, Technische Universität München<P> |
|
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 |
|
37 </BODY> |
|
38 </HTML> |
|