Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces
By: Kazuhisa Nakasho
and Yasunari Shidama
and Yasunari Shidama Abstract
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.
Language: English
Page range: 247 - 269
Accepted on: Dec 24, 2024
Published on: Dec 31, 2024
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Keywords:
Related subjects:
© 2024 Kazuhisa Nakasho, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.