@MISC{NDIFF11.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Shidama, Yasunari},
  TITLE = {Implicit Function Theorem -- Part {III} and Inverse Function Theorem -- Part {II}},
  SECTION1 = {Matrix and Linear Transformation on Euclidean Spaces},
  SECTION2 = {Total Derivative and Partial Derivative},
  SECTION3 = {Jacobian Matrix},
  SECTION4 = {Implicit and Inverse Function Theorems on Euclidean Spaces},
  DAY = {30}, 
  MONTH = {September},
  YEAR = {2022},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  ADDRESS2 = {Karuizawa Hotch 244-1\\Nagano, Japan},
  MSC2010 = {26B10 47J07 68V20},
  KEYWORDS = {implicit function theorem; inverse function theorem; continuously differentiable function},
  SUMMARY = {Previous Mizar articles \cite{NDIFF_8.ABS,NDIFF_9.ABS,NDIFF10.ABS} formalized the implicit
  and inverse function theorems for Frechet continuously differentiable maps on Banach spaces.
  In this paper, we formalize these theorems on Euclidean spaces by specializing them.
    We referred to \cite{miyadera:1972}, \cite{yoshida:1980}, \cite{Schwartz1997a}, \cite{Schwartz1997b}
    in this formalization.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS KAKENHI Grant Number JP20K19863.}}

@BOOK{miyadera:1972,
 AUTHOR={Isao Miyadera},
 TITLE={Functional Analysis},
 PUBLISHER={Riko-Gaku-Sya},
 YEAR=1972}

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

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