Bidual Spaces and Reflexivity of Real Normed Spaces

• Autorzy: Keiko Narita , Noboru Endou , Yasunari Shidama
• Języki publikacji: EN

Abstrakty

EN

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].

Słowa kluczowe

EN

continuous dual space; topological duality; reflexivity

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2014
• Tom: 22
• Numer: 4
• Strony: 303-311

Daty

wydano

2014-12-01

otrzymano

2014-11-29

online

2014-12-31

Twórcy

autor

Keiko Narita

• Hirosaki-city Aomori, Japan

autor

Noboru Endou

• Gifu National College of Technology Gifu, Japan

autor

Yasunari Shidama

• Shinshu University Nagano, Japan

Bibliografia

• [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]
• [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]
• [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.
• [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.

Identyfikatory

DOI

10.2478/forma-2014-0030