author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 36862  952b2b102a0a 
permissions  rwrr 
15283  1 
<!DOCTYPE HTML PUBLIC "//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> 
2 

15582  3 
<HTML> 
4 

5 
<HEAD> 

6 
<meta httpequiv="ContentType" content="text/html; charset=iso88591"> 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset

7 
<TITLE>HOL/Hahn_Banach/README</TITLE> 
15582  8 
</HEAD> 
9 

10 
<BODY> 

7655  11 

15283  12 
<H3>The HahnBanach Theorem for Real Vector Spaces (Isabelle/Isar)</H3> 
7655  13 

15283  14 
Author: Gertrud Bauer, Technische Universität München<P> 
7655  15 

16 
This directory contains the proof of the HahnBanach theorem for real vectorspaces, 

17 
following H. Heuser, Funktionalanalysis, p. 228 232. 

18 
The HahnBanach theorem is one of the fundamental theorems of functioal analysis. 

19 
It is a conclusion of Zorn's lemma.<P> 

20 

21 
Two different formaulations of the theorem are presented, one for general real vectorspaces 

22 
and its application to normed vectorspaces. <P> 

23 

24 
The theorem says, that every continous linearform, defined on arbitrary subspaces 

25 
(not only onedimensional subspaces), can be extended to a continous linearform on 

26 
the whole vectorspace. 

27 

28 

29 
<HR> 

30 

31 
<ADDRESS> 

32 
<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A> 

33 
</ADDRESS> 

34 

15582  35 
</BODY> 
36 
</HTML> 