# 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

## Access Full Article

top## Abstract

top## How to cite

topKeiko 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] Haim Brezis. Functional Analysis, Sobolev Spaces and Partial Differential Equations. Springer, 2011.
- [2] Czesław Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990.
- [3] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
- [4] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
- [5] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
- [6] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
- [7] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599-603, 1991.
- [8] Peter D. Dax. Functional Analysis. Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts. Wiley Interscience, 2002.
- [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] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1): 35-40, 1990.
- [11] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477-481, 1990.
- [12] Eugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.
- [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] 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] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269-275, 2004.
- [16] Bogdan Nowak and Andrzej Trybulec. Hahn-Banach theorem. Formalized Mathematics, 4(1):29-34, 1993.
- [17] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263-264, 1990.
- [18] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991.
- [19] Michael Reed and Barry Simon. Methods of modern mathematical physics. Vol. 1. Academic Press, New York, 1972. Zbl0242.46001
- [20] Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.
- [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] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39-48, 2004.
- [23] Yasumasa Suzuki, Noboru Endou, and Yasunari Shidama. Banach space of absolute summable real sequences. Formalized Mathematics, 11(4):377-380, 2003.
- [24] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003.
- [25] Wojciech A. Trybulec. Subspaces and cosets of subspaces in real linear space. Formalized Mathematics, 1(2):297-301, 1990.
- [26] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
- [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] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
- [29] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.

## Citations in EuDML Documents

top## NotesEmbed ?

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