@MISC{NDIFF_8.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Futa, Yuichi and Shidama, Yasunari},
  TITLE = {Implicit Function Theorem -- Part {I}},
  SECTION1 = {Properties of Lipschitz continuous linear function},
  SECTION2 = {Properties of open and closed sets in Banach space},
  SECTION3 = {Existence and uniqueness of continuous implicit function},
  DAY = {29},
  MONTH = {November},
  YEAR = {2017},
  ADDRESS1 = {Osaka University\\Osaka, Japan},
  ADDRESS2 = {Tokyo University of Technology\\Tokyo, Japan},
  ADDRESS3 = {Shinshu University\\Nagano, Japan},
  MSC2010 = {26B10 53A07},
  KEYWORDS = {implicit function theorem; Banach fixed point theorem; Lipschitz continuity},
  SUMMARY = {In this article, we formalized existence and uniqueness part
    of implicit function theorem.
    In the first section, some composition properties of Lipschitz continuous linear function are discussed.
    In the second section, a definition of closed ball and
    theorems of several properties of open and closed sets in Banach
    space are described.
    In the last section, we formalized existence and uniqueness of continuous
    implicit function in Banach space using Banach fixed point theorem.
    We referred to \cite{Schwartz1997a}, \cite{Schwartz1997b},
    and \cite{driver2003} in this formalization.}}

@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}
}
