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].
@article{bwmeta1.element.doi-10_2478_forma-2014-0030,
author = {Keiko Narita and Noboru Endou and Yasunari Shidama},
title = {Bidual Spaces and Reflexivity of Real Normed Spaces},
journal = {Formalized Mathematics},
volume = {22},
year = {2014},
pages = {303-311},
zbl = {1316.46014},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_forma-2014-0030}
}
Keiko Narita; Noboru Endou; Yasunari Shidama. Bidual Spaces and Reflexivity of Real Normed Spaces. Formalized Mathematics, Tome 22 (2014) pp. 303-311. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_forma-2014-0030/
[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] | Zbl 1311.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] | Zbl 1298.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. | Zbl 0242.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.