equal
deleted
inserted
replaced
|
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 |