Separability of Real Normed Spaces and Its Basic Properties

Summary 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].

Topological Properties of Real Normed Space

Summary In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach’s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67).