@MISC{NDIFF_9.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Shidama, Yasunari},
  TITLE = {Implicit Function Theorem -- Part {II}},
  SECTION1 = {Properties of Lipschitz Continuous Linear Operators},
  SECTION2 = {Differentiability of Implicit Function},
  DAY = {27},
  MONTH = {May},
  YEAR = {2019},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  ADDRESS2 = {Shinshu University\\Nagano, Japan},
  MSC2010 = {26B10 47A05 47J07 53A07},
  KEYWORDS = {implicit function theorem; Lipschitz continuity; differentiability; implicit function},
  SUMMARY = {In this article, we formalized differentiabilitiy of implicit function theorem.
            In the first half section, properties of Lipschitz continuous linear operators are discussed.
            Some norm properties of a direct sum decomposition of Lipschitz continuous linear 
             operator are mentioned here.
            In the last half section, differentiability of implicit function in implicit function 
             theorem is formalized.
            The existence and uniqueness of implicit function in \cite{NDIFF_8.MIZ} is cited.
            We referred to \cite{Schwartz1997a}, \cite{Schwartz1997b}, and \cite{driver2003} in the 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}
}
