<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>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.</p>
</abstract>

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.

On Implicit and Inverse Function Theorems on Euclidean Spaces

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"On Implicit and Inverse Function Theorems on Euclidean Spaces"}

Previous Mizar articles [7, 6, 5] formalized the implicit and inverse function theorems for Frechet continuously differentiable maps on Banach spaces. In this...

On Implicit and Inverse Function Theorems on Euclidean Spaces

Data publikacji: 30 gru 2022

Zakres stron: 159 - 168

Przyjęty: 30 wrz 2022

DOI: https://doi.org/10.2478/forma-2022-0012

Słowa kluczowe
implicit function theorem, inverse function theorem, continuously differentiable function

© 2022 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

On Implicit and Inverse Function Theorems on Euclidean Spaces

Data publikacji: 30 gru 2022

Zakres stron: 159 - 168

Przyjęty: 30 wrz 2022

DOI: https://doi.org/10.2478/forma-2022-0012

Słowa kluczoweimplicit function theorem, inverse function theorem, continuously differentiable function

© 2022 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Słowa kluczowe
implicit function theorem, inverse function theorem, continuously differentiable function