Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

The Hahn Banach Theorem in the Vector Space over the Field of Complex Numbers


Anna Justyna Milewska
University of Bialystok

Summary.

This article contains the Hahn Banach theorem in the vector space over the field of complex numbers.

MML Identifier: HAHNBAN1

The terminology and notation used in this paper have been introduced in the following articles [13] [4] [20] [16] [6] [7] [12] [11] [18] [8] [17] [19] [2] [3] [1] [21] [15] [14] [5] [10] [9]

Contents (PDF format)

  1. Preliminaries
  2. Some Facts on the Field of Complex Numbers
  3. Functionals of Vector Space
  4. The Vector Space of Linear Functionals
  5. Semi Norm of Vector Space
  6. The Hahn Banach Theorem

Bibliography

[1] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. The complex numbers. Journal of Formalized Mathematics, 2, 1990.
[6] Library Committee. Introduction to arithmetic. Journal of Formalized Mathematics, Addenda, 2003.
[7] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[8] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
[9] Anna Justyna Milewska. The field of complex numbers. Journal of Formalized Mathematics, 12, 2000.
[10] Bogdan Nowak and Andrzej Trybulec. Hahn-Banach theorem. Journal of Formalized Mathematics, 5, 1993.
[11] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[12] Jan Popiolek. Some properties of functions modul and signum. Journal of Formalized Mathematics, 1, 1989.
[13] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[14] Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.
[15] Andrzej Trybulec. Natural transformations. Discrete categories. Journal of Formalized Mathematics, 3, 1991.
[16] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[17] Wojciech A. Trybulec. Subspaces and cosets of subspaces in real linear space. Journal of Formalized Mathematics, 1, 1989.
[18] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[19] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Journal of Formalized Mathematics, 2, 1990.
[20] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[21] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.

Received May 23, 2000

[ Download a postscript version, MML identifier index, Mizar home page]