Topological Properties of Real Normed Space

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

Full description

Bibliographic Details
Main Authors: Nakasho Kazuhisa, Futa Yuichi, Shidama Yasunari
Format: Article
Language:English
Published: Sciendo 2014-09-01
Series:Formalized Mathematics
Subjects:
Online Access:https://doi.org/10.2478/forma-2014-0024