@MISC{ASCOLI.MIZ,
  AUTHOR = {Yamazaki, Hiroshi and Miyajima, Keiichi and
    Shidama, Yasunari},
  TITLE = {Ascoli-{A}rzela's Theorem},
  SECTION1 = {Equicontinuousness and Equiboundedness of
    Continuous Functions},
  SECTION2 = {Ascoli-Arzela's Theorem},
  DAY = {30},
  MONTH = {June},
  YEAR = {2021},
  ADDRESS1 = {Nagano Prefectural Institute of Technology\\Nagano, Japan},
  ADDRESS2 = {Ibaraki University \\Ibaraki, Japan},
  ADDRESS3 = {Karuizawa Hotch 244-1\\Nagano, Japan},
  MSC2010 = {46B50},
  KEYWORDS = {Ascoli-Arzela's theorem, equicontinuousness of
    continuous functions, equiboundedness of continuous functions },
  SUMMARY = {In this article, the Ascoli-Arzela's theorem
    is formalized. First, we gave definitions of equicontinuousness
    and equiboundedness of a set of continuous
    functions. Next, we formalized the Ascoli-Arzela's theorem
    using those definitions, and proved this theorem.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS
  KAKENHI Grant Numbers JP17K00182.}}

@BOOK{Schwartz1997a,
  TITLE={Th\'{e}orie des ensembles et topologie, tome 1. Analyse},
  AUTHOR={Laurent Schwartz},
  PUBLISHER={Hermann},
  YEAR={1997},
  MONTH={10},}

@BOOK{Schwartz1997b,
  TITLE = {Calcul diff\'{e}rentiel, tome 2. Analyse},
  AUTHOR = {Laurent Schwartz},
  PUBLISHER = {Hermann},
  YEAR = {1997},
  MONTH = {10}}

@BOOK{driver2003,
  TITLE = {Analysis Tools with Applications},
  AUTHOR = {Bruce K. Driver},
  PUBLISHER = {Springer, Berlin},
  YEAR = {2003},
  MONTH = {10}}
