wenzelm@7655: HOL/Real/HahnBanach/README wenzelm@7655: wenzelm@7655:

The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).

wenzelm@7655: wenzelm@7655: Author: Gertrud Bauer, Technische Universität München

wenzelm@7655: wenzelm@7655: This directory contains the proof of the Hahn-Banach theorem for real vectorspaces, wenzelm@7655: following H. Heuser, Funktionalanalysis, p. 228 -232. wenzelm@7655: The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis. wenzelm@7655: It is a conclusion of Zorn's lemma.

wenzelm@7655: wenzelm@7655: Two different formaulations of the theorem are presented, one for general real vectorspaces wenzelm@7655: and its application to normed vectorspaces.

wenzelm@7655: wenzelm@7655: The theorem says, that every continous linearform, defined on arbitrary subspaces wenzelm@7655: (not only one-dimensional subspaces), can be extended to a continous linearform on wenzelm@7655: the whole vectorspace. wenzelm@7655: wenzelm@7655: wenzelm@7655:


wenzelm@7655: wenzelm@7655:
wenzelm@7655: bauerg@in.tum.de wenzelm@7655:
wenzelm@7655: wenzelm@7655: wenzelm@7655: