isabelle: src/HOL/Hahn_Banach/README.html@952b2b102a0a (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	<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	4
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	5	<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	6	<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	7	<TITLE>HOL/Hahn_Banach/README</TITLE>
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	9
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	10	<BODY>
7655 21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	11
15283 f21466450330 DOCTYPE declaration added webertj parents: 7927 diff changeset	12	<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	13
15283 f21466450330 DOCTYPE declaration added webertj parents: 7927 diff changeset	14	Author: Gertrud Bauer, Technische Universität München<P>
7655 21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	15
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	16	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	17	following H. Heuser, Funktionalanalysis, p. 228 -232.
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	18	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	19	It is a conclusion of Zorn's lemma.<P>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	20
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	21	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	22	and its application to normed vectorspaces. <P>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	23
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	24	The theorem says, that every continous linearform, defined on arbitrary subspaces
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	25	(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	26	the whole vectorspace.
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	27
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	28
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	29	<HR>
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	<ADDRESS>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	32	<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	33	</ADDRESS>
21b7b0fd41bd The Hahn-Banach theorem for real vectorspaces; wenzelm parents: diff changeset	34
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	35	</BODY>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	36	</HTML>

author	wenzelm
	Wed, 12 May 2010 14:17:26 +0200
changeset 36862	952b2b102a0a
parent 31795	be3e1cc5005c
permissions	-rw-r--r--