1.1 --- a/src/HOL/HahnBanach/README.html Wed Jun 24 21:28:02 2009 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,38 +0,0 @@
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/Real/HahnBanach/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ät Mü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>