On Implicit and Inverse Function Theorems on Euclidean Spaces
Orcid-Profil30. Dez. 2022
Über diesen Artikel
Online veröffentlicht: 30. Dez. 2022
Seitenbereich: 159 - 168
Akzeptiert: 30. Sept. 2022
DOI: https://doi.org/10.2478/forma-2022-0012
Schlüsselwörter
© 2022 Kazuhisa Nakasho et al., published by Sciendo
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.
Previous Mizar articles [7, 6, 5] formalized the implicit and inverse function theorems for Frechet continuously differentiable maps on Banach spaces. In this paper, using the Mizar system [1], [2], we formalize these theorems on Euclidean spaces by specializing them. We referred to [4], [12], [10], [11] in this formalization.