Abstract
In this article, using the Mizar system [2], [1], 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 [3], [10], [6], [7] in this formalization.