<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, the separability of real normed spaces and its properties are mainly formalized. In the first section, it is proved that a real normed subspace is separable if it is generated by a countable subset. We used here the fact that the rational numbers form a dense subset of the real numbers. In the second section, the basic properties of the separable normed spaces are discussed. It is applied to isomorphic spaces via bounded linear operators and double dual spaces. In the last section, it is proved that the completeness and reflexivity are transferred to sublinear normed spaces. The formalization is based on [34], and also referred to [7], [14] and [16].</p></abstract>

In this article, the separability of real normed spaces and its properties are mainly formalized. In the first section, it is proved that a real normed subspace is separable if it is generated by a countable subset. We used here the fact that the rational numbers form a dense subset of the real numbers. In the second section, the basic properties of the separable normed spaces are discussed. It is applied to isomorphic spaces via bounded linear operators and double dual spaces. In the last section, it is proved that the completeness and reflexivity are transferred to sublinear normed spaces. The formalization is based on [34], and also referred to [7], [14] and [16].

Separability of Real Normed Spaces and Its Basic Properties

Gifu National College of Technology, Gifu, Japan

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"Separability of Real Normed Spaces and Its Basic Properties"}

In this article, the separability of real normed spaces and its properties are mainly formalized. In the first section, it is proved that a real normed...

Separability of Real Normed Spaces and Its Basic Properties

Online veröffentlicht: 31. März 2015

Seitenbereich: 59 - 65

Eingereicht: 26. Feb. 2015

DOI: https://doi.org/10.2478/forma-2015-0005

Schlüsselwörter
functional analysis, normed linear space, topological vector space

© Kazuhisa Nakasho et al.

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Separability of Real Normed Spaces and Its Basic Properties

Online veröffentlicht: 31. März 2015

Seitenbereich: 59 - 65

Eingereicht: 26. Feb. 2015

DOI: https://doi.org/10.2478/forma-2015-0005

Schlüsselwörterfunctional analysis, normed linear space, topological vector space

© Kazuhisa Nakasho et al.

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Schlüsselwörter
functional analysis, normed linear space, topological vector space