<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

Publicado en línea: 31 mar 2015

Páginas: 59 - 65

Recibido: 26 feb 2015

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

Palabras clave
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

Publicado en línea: 31 mar 2015

Páginas: 59 - 65

Recibido: 26 feb 2015

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

Palabras clavefunctional analysis, normed linear space, topological vector space

© Kazuhisa Nakasho et al.

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

Palabras clave
functional analysis, normed linear space, topological vector space