Inverse Function Theorem. Part I¹

In this article we formalize in Mizar [1], [2] the inverse function theorem for the class of C¹ 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 𝔼 ↶ ≂ (x, y) ∈ X × Y ↦ (y, x) ∈ Y × 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 [6].

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¹ functions between Banach spaces. We referred to [9], [10], and [3] in the formalization.