@MISC{LOPBAN13.MIZ,
  AUTHOR = {Nakasho, Kazuhisa},
  TITLE = {Invertible Operators on Banach Spaces},
  SECTION1 = {Neumann Series and Invertible Operator},
  SECTION2 = {Isomorphic Mapping to Inverse Operators}
  DAY = {27},
  MONTH = {May},
  YEAR = {2019},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  MSC2010 = {47-00 47A05 47J07},
  KEYWORDS = {Banach space; invertible operator; Neumann series; Isomorphism of Linear Operator Spaces},
  SUMMARY = {In this article, we discuss invertible operators on Banach spaces.
    In the first chapter, we formalized the theorem that denotes any operators that 
    are close enough to an invertible operator are also invertible by 
    using the property of Neumann series.
    In the second chapter, we formalized the continuity of an 
    isomorphism that maps an invertible operator on Banach spaces to its inverse.
    These results are used in the proof of the implicit function theorem.
    We referred to \cite{miyadera:1972}, \cite{yoshida:1980}, \cite{Schwartz1997a}, 
     \cite{Schwartz1997b} in this formalization.},
  ACKNOWLEDGEMENT = {I would like to express my gratitude to Professor Yasunari Shidama for his helpful    advice.}}

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