Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces
By: Kazuhisa Nakasho 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.