Bidual Spaces and Reflexivity of Real Normed Spaces

Keiko Narita; Noboru Endou; Yasunari Shidama

Formalized Mathematics (2014)

  • Volume: 22, Issue: 4, page 303-311
  • ISSN: 1426-2630

Abstract

top
In this article, we considered bidual spaces and reflexivity of real normed spaces. At first we proved some corollaries applying Hahn-Banach theorem and showed related theorems. In the second section, we proved the norm of dual spaces and defined the natural mapping, from real normed spaces to bidual spaces. We also proved some properties of this mapping. Next, we defined real normed space of R, real number spaces as real normed spaces and proved related theorems. We can regard linear functionals as linear operators by this definition. Accordingly we proved Uniform Boundedness Theorem for linear functionals using the theorem (5) from [21]. Finally, we defined reflexivity of real normed spaces and proved some theorems about isomorphism of linear operators. Using them, we proved some properties about reflexivity. These formalizations are based on [19], [20], [8] and [1].

How to cite

top

Keiko Narita, Noboru Endou, and Yasunari Shidama. "Bidual Spaces and Reflexivity of Real Normed Spaces." Formalized Mathematics 22.4 (2014): 303-311. <http://eudml.org/doc/270906>.

@article{KeikoNarita2014,
abstract = {In this article, we considered bidual spaces and reflexivity of real normed spaces. At first we proved some corollaries applying Hahn-Banach theorem and showed related theorems. In the second section, we proved the norm of dual spaces and defined the natural mapping, from real normed spaces to bidual spaces. We also proved some properties of this mapping. Next, we defined real normed space of R, real number spaces as real normed spaces and proved related theorems. We can regard linear functionals as linear operators by this definition. Accordingly we proved Uniform Boundedness Theorem for linear functionals using the theorem (5) from [21]. Finally, we defined reflexivity of real normed spaces and proved some theorems about isomorphism of linear operators. Using them, we proved some properties about reflexivity. These formalizations are based on [19], [20], [8] and [1].},
author = {Keiko Narita, Noboru Endou, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {continuous dual space; topological duality; reflexivity},
language = {eng},
number = {4},
pages = {303-311},
title = {Bidual Spaces and Reflexivity of Real Normed Spaces},
url = {http://eudml.org/doc/270906},
volume = {22},
year = {2014},
}

TY - JOUR
AU - Keiko Narita
AU - Noboru Endou
AU - Yasunari Shidama
TI - Bidual Spaces and Reflexivity of Real Normed Spaces
JO - Formalized Mathematics
PY - 2014
VL - 22
IS - 4
SP - 303
EP - 311
AB - In this article, we considered bidual spaces and reflexivity of real normed spaces. At first we proved some corollaries applying Hahn-Banach theorem and showed related theorems. In the second section, we proved the norm of dual spaces and defined the natural mapping, from real normed spaces to bidual spaces. We also proved some properties of this mapping. Next, we defined real normed space of R, real number spaces as real normed spaces and proved related theorems. We can regard linear functionals as linear operators by this definition. Accordingly we proved Uniform Boundedness Theorem for linear functionals using the theorem (5) from [21]. Finally, we defined reflexivity of real normed spaces and proved some theorems about isomorphism of linear operators. Using them, we proved some properties about reflexivity. These formalizations are based on [19], [20], [8] and [1].
LA - eng
KW - continuous dual space; topological duality; reflexivity
UR - http://eudml.org/doc/270906
ER -

References

top
  1. [1] Haim Brezis. Functional Analysis, Sobolev Spaces and Partial Differential Equations. Springer, 2011. 
  2. [2] Czesław Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990. 
  3. [3] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  4. [4] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  5. [5] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  6. [6] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  7. [7] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599-603, 1991. 
  8. [8] Peter D. Dax. Functional Analysis. Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts. Wiley Interscience, 2002. 
  9. [9] Noboru Endou, Yasunari Shidama, and Katsumasa Okamura. Baire’s category theorem and some spaces generated from real normed space. Formalized Mathematics, 14(4): 213-219, 2006. doi:10.2478/v10037-006-0024-x.[Crossref] 
  10. [10] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1): 35-40, 1990. 
  11. [11] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477-481, 1990. 
  12. [12] Eugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990. 
  13. [13] Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Topological properties of real normed space. Formalized Mathematics, 22(3):209-223, 2014. doi:10.2478/forma-2014-0024.[Crossref] Zbl1311.46016
  14. [14] Keiko Narita, Noboru Endou, and Yasunari Shidama. Dual spaces and Hahn-Banach theorem. Formalized Mathematics, 22(1):69-77, 2014. doi:10.2478/forma-2014-0007.[Crossref] Zbl1298.46005
  15. [15] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269-275, 2004. 
  16. [16] Bogdan Nowak and Andrzej Trybulec. Hahn-Banach theorem. Formalized Mathematics, 4(1):29-34, 1993. 
  17. [17] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263-264, 1990. 
  18. [18] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991. 
  19. [19] Michael Reed and Barry Simon. Methods of modern mathematical physics. Vol. 1. Academic Press, New York, 1972. Zbl0242.46001
  20. [20] Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991. 
  21. [21] Hideki Sakurai, Hisayoshi Kunimune, and Yasunari Shidama. Uniform boundedness principle. Formalized Mathematics, 16(1):19-21, 2008. doi:10.2478/v10037-008-0003-5.[Crossref] 
  22. [22] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39-48, 2004. 
  23. [23] Yasumasa Suzuki, Noboru Endou, and Yasunari Shidama. Banach space of absolute summable real sequences. Formalized Mathematics, 11(4):377-380, 2003. 
  24. [24] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003. 
  25. [25] Wojciech A. Trybulec. Subspaces and cosets of subspaces in real linear space. Formalized Mathematics, 1(2):297-301, 1990. 
  26. [26] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990. 
  27. [27] Wojciech A. Trybulec. Subspaces of real linear space generated by one, two, or three vectors and their cosets. Formalized Mathematics, 3(2):271-274, 1992. 
  28. [28] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  29. [29] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.