@MISC{TOPMETR4.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Narita, Keiko and Shidama, Yasunari},
  TITLE = {Compactness in Metric Spaces},
  SECTION1 = {Topological Properties of Metric Spaces},
  SECTION2 = {Compactness in Metric Spaces},
  SECTION3 = {Compactness in Norm Spaces},
  SECTION4 = {Topological Properties of the Real Line},
  SECTION5 = {Compactness in the Real Line},
  DAY = {30},
  MONTH = {June},
  YEAR = {2016},
  ADDRESS1 = {Shinshu University\\Nagano, Japan},
  ADDRESS2 = {Hirosaki-city\\Aomori, Japan},
  ADDRESS3 = {Shinshu University\\Nagano, Japan},
  MSC2010 = {46A50 46B50 54E45},
  KEYWORDS = {metric spaces; normed linear spaces; compactness},
  SUMMARY = {In this article, we mainly formalize the equivalence among
  a few compactness definitions of metric spaces, norm spaces,
  and the real line.
  In the first section, we formalized general topological properties of
  metric spaces. We discussed openness and closedness of subsets in
  metric spaces in terms of convergence of element sequences here.
  In the second section, we firstly formalize the definition of
  sequentially compact, and we discuss the equivalence of compactness,
  countable compactness, sequential compactness,
  and totally boundedness with completeness in metric spaces.
  In the third section, we discuss compactness in norm spaces.
  We formalize the equivalence of compactness and sequential
  compactness in norm space here.
  In the fourth section, we formalize topological properties of
  the real line in terms of convergence of real number sequences.
  In the last section, we formalize the equivalence of compactness
  and sequential compactness in the real line.
  These formalizations are based on \cite{yoshida:1980},
  \cite{bourbaki1987elements}, and \cite{bourbaki2013general}.}}

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

@BOOK{bourbaki1987elements,
      TITLE = {Elements of mathematics: Topological vector spaces},
     AUTHOR = {Bourbaki, Nicolas and Eggleston, H.G. and Madan, S.},
       YEAR = {1987},
  PUBLISHER = {Springer-Verlag}}

@book{bourbaki2013general,
  title={General Topology: Chapters 1--4},
  author={Bourbaki, Nicolas},
  year={2013},
  publisher={Springer Science and Business Media}}
