AbstractIn this article, we deal with weak convergence on sequences in real normed spaces, and weak* convergence on sequences in dual spaces of real normed spaces. In the first section, we proved some topological properties of dual spaces of real normed spaces. We used these theorems for proofs of Section 3. In Section 2, we defined weak convergence and weak* convergence, and proved some properties. By RNS_Real Mizar functor, real normed spaces as real number spaces already defined in the article [18], we regarded sequences of real numbers as sequences of RNS_Real. So we proved the last theorem in this section using the theorem (8) from [25]. In Section 3, we defined weak sequential compactness of real normed spaces. We showed some lemmas f...
SummaryIn this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first s...
This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spac...
AbstractIn this article we introduce the convergence of extended realvalued double sequences [16], [...
In this article, we considered bidual spaces and reflexivity of real normed spaces. At first we prov...
In this article, the separability of real normed spaces and its properties are mainly formalized. In...
In this article, we formalize topological properties of real normed spaces. In the first part, open ...
We would like to express our gratitude to Prof. Yatsuka Nakamura.In this article, we described the c...
In this article we deal with the Riemann integral of functions from R into a real Banach space. The ...
AbstractIn this article, the orthogonal projection and the Riesz representation theorem are mainly f...
In this article, we formalize isometric differentiable functions on real normed space [17], and thei...
In this article, we formalize the differentiability of functions from the set of real numbers into a...
In this article, we deal with dual spaces and the Hahn-Banach Theorem. At the first, we defined dual...
In this article, we formalize in Mizar [1], [2] the topological properties of finite-dimensional rea...
In this article, we formalize in Mizar [1], [3] the existence and uniqueness part of the implicit fu...
In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definition...
SummaryIn this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first s...
This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spac...
AbstractIn this article we introduce the convergence of extended realvalued double sequences [16], [...
In this article, we considered bidual spaces and reflexivity of real normed spaces. At first we prov...
In this article, the separability of real normed spaces and its properties are mainly formalized. In...
In this article, we formalize topological properties of real normed spaces. In the first part, open ...
We would like to express our gratitude to Prof. Yatsuka Nakamura.In this article, we described the c...
In this article we deal with the Riemann integral of functions from R into a real Banach space. The ...
AbstractIn this article, the orthogonal projection and the Riesz representation theorem are mainly f...
In this article, we formalize isometric differentiable functions on real normed space [17], and thei...
In this article, we formalize the differentiability of functions from the set of real numbers into a...
In this article, we deal with dual spaces and the Hahn-Banach Theorem. At the first, we defined dual...
In this article, we formalize in Mizar [1], [2] the topological properties of finite-dimensional rea...
In this article, we formalize in Mizar [1], [3] the existence and uniqueness part of the implicit fu...
In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definition...
SummaryIn this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first s...
This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spac...
AbstractIn this article we introduce the convergence of extended realvalued double sequences [16], [...