<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

Data publikacji: 31 mar 2015

Zakres stron: 59 - 65

Otrzymano: 26 lut 2015

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

Słowa kluczowe
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

Data publikacji: 31 mar 2015

Zakres stron: 59 - 65

Otrzymano: 26 lut 2015

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

Słowa kluczowefunctional analysis, normed linear space, topological vector space

© Kazuhisa Nakasho et al.

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

Słowa kluczowe
functional analysis, normed linear space, topological vector space