@MISC{PRVECT_4.MIZ,
  AUTHOR = {Okazaki, Hiroyuki and Nakasho, Kazuhisa},
  TITLE = {The 3-fold Product Space of Real Normed Spaces and its Properties},
  SECTION1 = {3-Variable Function & 3-fold Cartesian product},
  SECTION2 = {3-fold Product Space of Real Linear Spaces},
  SECTION3 = {3-fold Product Space of Real Normed Spaces},
  DAY = {30},
  MONTH = {November},
  YEAR = {2021},
  ADDRESS1 = {Shinshu University\\Nagano, Japan},
  ADDRESS2 = {Yamaguchi University\\Yamaguchi, Japan},
  MSC2010 = {26-00 46-00 46B15 46B20},
  KEYWORDS = {3-fold product spaces; linear spaces;normed spaces},
  SUMMARY = {In this article, we formalize the 3-fold product space of real normed      spaces for usefulness in application fields such as engineering, although the   formalization of the 2-fold product
  space of real normed spaces has been stored in the MML \cite{PRVECT_2.ABS}.
  First, we prove some theorems about the 3-variable function and 3-fold Cartesian   product for preparation.
  Then we formalize the definition of 3-fold product space of real linear spaces.
  Finally, we formulate the definition of 3-fold product space of real normed spaces.
   We referred to \cite{YOSHIDA1980} and \cite{READSIMON1980} in the formalization.},
  ACKNOWLEDGEMENT = {The authors would also like to express our gratitude to Prof.   Yasunari Shidama for his support and encouragement.}}

@BOOK{YOSHIDA1980,
      AUTHOR = {Yoshida, Kosaku},
      TITLE = {Functional Analysis},
      PUBLISHER = {Springer-Verlag},
      YEAR = {1980}}

@BOOK{READSIMON1980,
      AUTHOR = {Read, Michael and Simon, Barry},
      TITLE = {Functional Analysis (Methods of Modern Mathematical Physics)},
      PUBLISHER = {Academic Press},
      YEAR = {1980}}

