@MISC{REAL_NS3.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Okazaki, Hiroyuki and Shidama, Yasunari},
  TITLE = {Finite Dimensional Real Normed Spaces are Proper Metric Spaces},
  SECTION1 = {Bolzano-Weierstrass Theorem and Its Corollary},
  SECTION2 = {L1-norm and Maximum Norm},
  SECTION3 = {Linear Isometry and Its Topological Properties},
  DAY = {30},
  MONTH = {September},
  YEAR = {2021},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  ADDRESS2 = {Shinshu University\\Nagano, Japan},
  ADDRESS3 = {Shinshu University\\Nagano, Japan},
  MSC2010 = {15A04 40A05 46A50},
  KEYWORDS = {real vector space; topological space; normed spaces; L1-norm; maximum Norm; linear isometry; proper metric space},
  SUMMARY = {In this article, we formalize the topological properties of 
    finite-dimensional real normed spaces. In the first section, we formalize the 
    Bolzano-Weierstrass theorem, which states that a bounded sequence of points in 
    an n-dimensional Euclidean space has a certain subsequence that converges
    to a point. As a corollary, it is also shown the equivalence between a subset 
    of an n-dimensional Euclidean space being compact and being closed and bounded. 
    In the next section, we formalize the definitions of L1-norm (Manhattan Norm) 
    and maximum norm and show their topological equivalence in n-dimensional Euclidean 
    spaces and finite-dimensional real linear spaces. In the last section,
    we formalize the linear isometries and their topological properties. Namely, 
    it is shown that a linear isometry between real normed spaces preserves properties 
    such as continuity, the convergence of a sequence, openness, closeness, and 
    compactness of subsets. Finally, it is shown that finite-dimensional real normed 
    spaces are proper metric spaces.
    We referred to \cite{miyadera:1972}, \cite{yoshida:1980}, and 
   \cite{Schwartz1997a} in the formalization.},
  ACKNOWLEDGEMENT = {This study was supported in part by JSPS KAKENHI Grant 
     Numbers 17K00182 and 20K19863.}}
