In this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor ClstoCmp, compact topological spaces as closed interval subset of real numbers. Then using the former definition and referring to the article [10] and the article [5], we defined the normed spaces of continuous functions on closed interval subset of real numbers, and defined the normed spaces of bounded functions on closed interval subset of real numbers. We also proved some related properties. In Sec.2, we proved some lemmas for the proof of F. Riesz theorem. In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous functions on closed interval subset of real numbers, finally. We applied Hahn-Banach theorem (36) in [7], to the proof of the last theorem. For the description of theorems of this section, we also referred to the article [8] and the article [6]. These formalizations are based on [2], [3], [9], and [11].
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this paper we consider the approximate orthogonalities in real normed spaces. Using the notion of approximate orthogonalities in real normed spaces, we provide some new characterizations of rotundity and smoothness of dual spaces.
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In 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 for the proof and proved the theorem of weak sequential compactness of reflexive real Banach spaces. We referred to [36], [23], [24] and [3] in the formalization.
4
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Let X, Y be two Banach spaces. We say that Y is a quasi-quotient of X if there is a continuous operator R: X → Y such that its range, R(X), is dense in Y. Let X be a nonseparable Banach space, and let U, W be closed subspaces of X and Y, respectively. We prove that if X has the Controlled Separable Projection Property (CSPP) (this is a weaker notion than the WCG property) and Y is a quasi-quotient of X, then the structure of Y resembles the structure of a separable Banach space: (a) Y/W is norm-separable iff its dual W ⊥ is weak*-separable, (b) every weak*-separable subset of B Y* is weak*-metrizable, (c) every weak*-null sequence in the unit sphere of Y* contains a “nice“ subsequence; and (d) if U is separable, then X/U also has the CSPP. Property (a) yields an easy way of obtaining separable quotients in a class of Banach spaces. We also study the CSPP for C(K)-spaces, where K is a Mrówka compact space, e.g., we prove that the CSPP is not a three-space property.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.