This article is devoted to the Mizar formalization of various properties of differentiability of Lipschitzian bilinear operators in real normed spaces. Main results include the Lipschitz continuity of partial derivatives, the representation of the total derivative in terms of partial derivatives, and the continuous differentiability of Lipschitzian bilinear operators on open subsets of the product space.
© 2024 Kazuhisa Nakasho, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.