Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces
oraz 31 gru 2024
O artykule
Data publikacji: 31 gru 2024
Zakres stron: 247 - 269
Przyjęty: 24 gru 2024
DOI: https://doi.org/10.2478/forma-2024-0021
Słowa kluczowe
© 2024 Kazuhisa Nakasho et al., published by Sciendo
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.
This article extends the formalization of the theory of differentiation in real normed spaces in the Mizar system. The focus is on higher-order derivatives and the inverse function theorem. Additionally, we encode the differentiability of the inversion operator on invertible linear operators.