@MISC{NDIFF10.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Futa, Yuichi},
  TITLE = {Inverse Function Theorem -- Part {I}},
  SECTION1 = {Preliminaries},
  SECTION2 = {A Map Reversing the Order of Product of Two Norm Spaces},
  SECTION3 = {Properties of the Differentiation of the Inverse Mapping},
  SECTION4 = {Inverse Function Theorem for Class of $C^1$ Functions},
  DAY = {30},
  MONTH = {March},
  YEAR = {2021},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  ADDRESS2 = {Tokyo University of Technology\\Tokyo, Japan},
  MSC2010 = {26B10 47A05 47J07 53A07},
  KEYWORDS = {inverse function theorem; Lipschitz continuity; differentiability; implicit function; inverse function},
  SUMMARY = {In this article, we formalized the inverse function theorem for the class 
            of $C^1$ functions between Banach spaces.
            In the first section, we prove several theorems about open sets in 
            real norm space, which are needed in the proof of the inverse function 
            theorem.
            In the next section, we define a function to exchange the order of a product of two normed spaces,
            namely $\mathbb{Exch}(x,y) \in X \times Y \mapsto (y,x) \in Y \times X$,
            and formalized its bijective isometric property and several 
            differentiation properties.
            This map is necessary to change the order of the arguments of a function
            when deriving the inverse function theorem from the implicit function 
            theorem proved in \cite{NDIFF_9.MIZ}.
            In the third section, using the implicit function theorem,
            we prove a theorem that is a necessary component of the proof of the inverse 
            function theorem.
            In the last section, we finally formalized an inverse function theorem 
            for class of $C^1$ functions between Banach spaces.
            We referred to \cite{Schwartz1997a}, \cite{Schwartz1997b}, 
            and \cite{driver2003} in the formalization.},
  ACKNOWLEDGEMENT = {This study was supported in part by JSPS KAKENHI Grant 
           Numbers JP20K19863 and JP17K00182.
           The authors would also like to express their gratitude to
           Prof. Yasunari Shidama for his support and encouragement.}}

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