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.11 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
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 +