In this article, we deal with dual spaces and the Hahn-Banach Theorem. At the first, we defined dual spaces of real linear spaces and proved related basic properties. Next, we defined dual spaces of real normed spaces. We formed the definitions based on dual spaces of real linear spaces. In addition, we proved properties of the norm about elements of dual spaces. For the proof we referred to descriptions in the article [21]. Finally, applying theorems of the second section, we proved the Hahn-Banach extension theorem in real normed spaces. We have used extensively used [17].This work was supported by JSPS KAKENHI 22300285, 23500029.Narita Keiko - Hirosaki-city Aomori, JapanEndou Noboru - Gifu National College of Technology Gifu, JapanShidam...
In this article, we formalize the differentiability of functions from the set of real numbers into a...
In this article, we formalize isometric differentiable functions on real normed space [17], and thei...
In this article, using the Mizar system [2], [1], we discuss invertible operators on Banach spaces. ...
In this article, we considered bidual spaces and reflexivity of real normed spaces. At first we prov...
AbstractIn this article, the orthogonal projection and the Riesz representation theorem are mainly f...
In this article, the separability of real normed spaces and its properties are mainly formalized. In...
AbstractIn this article, we deal with weak convergence on sequences in real normed spaces, and weak*...
In this article, we formalize topological properties of real normed spaces. In the first part, open ...
In this article, we formalize in Mizar [1], [3] the existence and uniqueness part of the implicit fu...
We would like to express our gratitude to Prof. Yatsuka Nakamura.In this article, we described the c...
This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spac...
SummaryIn this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first s...
In this article, we described basic properties of Riemann integral on functions from R into Real Ban...
In this article we deal with the Riemann integral of functions from R into a real Banach space. The ...
In this article we formalize one of the most important theorems of linear operator theory - the Clos...
In this article, we formalize the differentiability of functions from the set of real numbers into a...
In this article, we formalize isometric differentiable functions on real normed space [17], and thei...
In this article, using the Mizar system [2], [1], we discuss invertible operators on Banach spaces. ...
In this article, we considered bidual spaces and reflexivity of real normed spaces. At first we prov...
AbstractIn this article, the orthogonal projection and the Riesz representation theorem are mainly f...
In this article, the separability of real normed spaces and its properties are mainly formalized. In...
AbstractIn this article, we deal with weak convergence on sequences in real normed spaces, and weak*...
In this article, we formalize topological properties of real normed spaces. In the first part, open ...
In this article, we formalize in Mizar [1], [3] the existence and uniqueness part of the implicit fu...
We would like to express our gratitude to Prof. Yatsuka Nakamura.In this article, we described the c...
This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spac...
SummaryIn this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first s...
In this article, we described basic properties of Riemann integral on functions from R into Real Ban...
In this article we deal with the Riemann integral of functions from R into a real Banach space. The ...
In this article we formalize one of the most important theorems of linear operator theory - the Clos...
In this article, we formalize the differentiability of functions from the set of real numbers into a...
In this article, we formalize isometric differentiable functions on real normed space [17], and thei...
In this article, using the Mizar system [2], [1], we discuss invertible operators on Banach spaces. ...