Implicit Function Theorem. Part II

Summary In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz continuous linear operators are discussed. Some norm properties of a direct sum decomposition of Lipschitz continuous linear operator ... View More