The Hahn-Banach theorem for real vectorspaces;
authorwenzelm
Wed Sep 29 15:35:09 1999 +0200 (1999-09-29)
changeset 765521b7b0fd41bd
parent 7654 57c4cea8b137
child 7656 2f18c0ffc348
The Hahn-Banach theorem for real vectorspaces;
src/HOL/Real/HahnBanach/README.html
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/HahnBanach/README.html	Wed Sep 29 15:35:09 1999 +0200
     1.3 @@ -0,0 +1,27 @@
     1.4 +<HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
     1.5 +
     1.6 +<H3> The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).</H3>
     1.7 +
     1.8 +Author:     Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>
     1.9 +
    1.10 +This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
    1.11 +following H. Heuser, Funktionalanalysis, p. 228 -232.
    1.12 +The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
    1.13 +It is a conclusion of Zorn's lemma.<P>
    1.14 +
    1.15 +Two different formaulations of the theorem are presented, one for general real vectorspaces
    1.16 +and its application to normed vectorspaces. <P>
    1.17 +
    1.18 +The theorem says, that every continous linearform, defined on arbitrary subspaces
    1.19 +(not only one-dimensional subspaces), can be extended to a continous linearform on
    1.20 +the whole vectorspace.
    1.21 +
    1.22 +
    1.23 +<HR>
    1.24 +
    1.25 +<ADDRESS>
    1.26 +<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
    1.27 +</ADDRESS>
    1.28 +
    1.29 +</BODY></HTML>
    1.30 +