Differentiability Properties of Lipschitzian Bilinear Operators in Real Normed Spaces

Summary

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.