@MISC{NORMSP_4.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Endou, Noboru},
  TITLE = {Separability of Real Normed Spaces and Its Basic Properties},
  SECTION1 = {Separability of Real Normed Space},
  SECTION2 = {Basic Properties of Separable Spaces},
  SECTION3 = {Completeness and Reflexivity of Sublinear Normed Spaces},
  DAY = {26},
  MONTH = {February},
  YEAR = {2015},
  ADDRESS1 = {Shinshu University, Nagano, Japan},
  ADDRESS2 = {Gifu National College of Technology, Gifu, Japan},
  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 \cite{yoshida:1980},
  and also referred to \cite{BOURBAKI:1-5}, \cite{Dunford:1958}
  and \cite{kolmogorov2012}.},
  ACKNOWLEDGEMENT = {We would like to thank Keiko Narita
    and Yasunari Shidama.}
  NOTE = {This work was supported by JSPS KAKENHI 23500029.}}

@BOOK{yoshida:1980,
 AUTHOR    = {Kosaku, Yoshida},
 TITLE     = {Functional Analysis},
 PUBLISHER = {Springer},
 YEAR      = {1980}}

@ARTICLE{BOURBAKI:1-5,
 AUTHOR  = {Bourbaki, Nicolas},
 TITLE   = {Topological Vector Spaces: Chapters 1-5},
 JOURNAL = {Springer},
 YEAR    = {1981}}

@BOOK{Dunford:1958,
 AUTHOR    = {Dunford, N. J. and Schwartz, T.},
 TITLE     = {Linear operators {I}},
 PUBLISHER = {Interscience Publ.},
 YEAR      = {1958}}

@BOOK{kolmogorov2012,
  TITLE      = {Elements of the Theory of Functions and Functional Analysis [Two Volumes in One]},
  AUTHOR     = {Kolmogorov, Andrey and Fomin, Sergei},
  PUBLISHER  = {Martino Fine Books},
  YEAR       = {2012}}
