src/HOL/Hahn_Banach/README.html
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 36862 952b2b102a0a
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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&auml;t M&uuml;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>