src/HOL/Hahn_Banach/README.html
changeset 31795 be3e1cc5005c
parent 29197 6d4cb27ed19c
child 36862 952b2b102a0a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hahn_Banach/README.html	Wed Jun 24 21:46:54 2009 +0200
     1.3 @@ -0,0 +1,38 @@
     1.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     1.5 +
     1.6 +<!-- $Id$ -->
     1.7 +
     1.8 +<HTML>
     1.9 +
    1.10 +<HEAD>
    1.11 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
    1.12 +  <TITLE>HOL/Hahn_Banach/README</TITLE>
    1.13 +</HEAD>
    1.14 +
    1.15 +<BODY>
    1.16 +
    1.17 +<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
    1.18 +
    1.19 +Author: Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>
    1.20 +
    1.21 +This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
    1.22 +following H. Heuser, Funktionalanalysis, p. 228 -232.
    1.23 +The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
    1.24 +It is a conclusion of Zorn's lemma.<P>
    1.25 +
    1.26 +Two different formaulations of the theorem are presented, one for general real vectorspaces
    1.27 +and its application to normed vectorspaces. <P>
    1.28 +
    1.29 +The theorem says, that every continous linearform, defined on arbitrary subspaces
    1.30 +(not only one-dimensional subspaces), can be extended to a continous linearform on
    1.31 +the whole vectorspace.
    1.32 +
    1.33 +
    1.34 +<HR>
    1.35 +
    1.36 +<ADDRESS>
    1.37 +<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
    1.38 +</ADDRESS>
    1.39 +
    1.40 +</BODY>
    1.41 +</HTML>