@MISC{REAL_NS2.MIZ,
 AUTHOR = {Nakasho, Kazuhisa and Okazaki, Hiroyuki and Shidama, Yasunari},
  TITLE = {Real Vector Space and Related Notions},
  SECTION1 = {Common Properties Between Norm and Topology
    in Finite Dimensional Linear Spaces},
  SECTION2 = {Finite Dimensional Vector Spaces over Real Field},
  DAY = {30},
  MONTH = {June},
  YEAR = {2021},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  ADDRESS2 = {Shinshu University\\Nagano, Japan},
  ADDRESS3 = {Shinshu University\\Nagano, Japan},
  MSC2010 = {15A03 26-00 46A50 46B15 46B20},
  KEYWORDS = {real vector space; topological space; normed spaces},
  SUMMARY = {In this paper, we discuss the properties that hold in finite dimensional
    vector spaces and related spaces. In the Mizar language, variables are strictly
    typed, and their type conversion requires a complicated process. Our purpose is
    to formalize that some properties of finite dimensional vector spaces are
    preserved in type transformations, and to contain the complexity of type
    transformations into this paper.
    Specifically, we show that properties such as algebraic structure, subsets, finite
    sequences and their sums, linear combination, linear independence, and affine
    independence are preserved in type conversions among TOP-REAL(n),
    REAL-NS(n), and n-VectSp_over F_Real.
    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.}}
