isabelle: src/HOL/Hahn_Banach/README.html@f5d95787224f (annotated)

15283 f21466450330 DOCTYPE declaration added webertj parents: 7927 diff changeset	1	<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added webertj parents: 7927 diff changeset	2
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	3	<!-- $Id$ -->
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	4
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	5	<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	6
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	7	<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
31795 be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 29197 diff changeset	9	<TITLE>HOL/Hahn_Banach/README</TITLE>
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	10	</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	11
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	12	<BODY>
7655 21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	13
15283 f21466450330 DOCTYPE declaration added webertj parents: 7927 diff changeset	14	<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
7655 21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	15
15283 f21466450330 DOCTYPE declaration added webertj parents: 7927 diff changeset	16	Author: Gertrud Bauer, Technische Universität München<P>
7655 21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	17
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	18	This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	19	following H. Heuser, Funktionalanalysis, p. 228 -232.
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	20	The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	21	It is a conclusion of Zorn's lemma.<P>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	22
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	23	Two different formaulations of the theorem are presented, one for general real vectorspaces
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	24	and its application to normed vectorspaces. <P>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	25
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	26	The theorem says, that every continous linearform, defined on arbitrary subspaces
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	27	(not only one-dimensional subspaces), can be extended to a continous linearform on
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	28	the whole vectorspace.
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	29
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	30
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	31	<HR>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	32
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	33	<ADDRESS>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	34	<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	35	</ADDRESS>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	36
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	37	</BODY>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	38	</HTML>

author	wenzelm
	Thu, 05 Nov 2009 14:37:39 +0100
changeset 33439	f5d95787224f
parent 31795	be3e1cc5005c
child 36862	952b2b102a0a
permissions	-rw-r--r--