<abstract xmlns="http://www.w3.org/1999/xhtml"><p>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 are mentioned here.</p><p>In the last half section, differentiability of implicit function in implicit function theorem is formalized. The existence and uniqueness of implicit function in [6] is cited. We referred to [10], [11], and [2] in the formalization.</p></abstract>

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 are mentioned here.In the last half section, differentiability of implicit function in implicit function theorem is formalized. The existence and uniqueness of implicit function in [6] is cited. We referred to [10], [11], and [2] in the formalization.

Implicit Function Theorem. Part II

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"Implicit Function Theorem. Part II"}

In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz...

Implicit Function Theorem. Part II

Publicado en línea: 20 jul 2019

Páginas: 117 - 131

Aceptado: 27 may 2019

DOI: https://doi.org/10.2478/forma-2019-0013

Palabras clave
implicit function theorem, Lipschitz continuity, differentiability, implicit function

© 2019 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Implicit Function Theorem. Part II

Publicado en línea: 20 jul 2019

Páginas: 117 - 131

Aceptado: 27 may 2019

DOI: https://doi.org/10.2478/forma-2019-0013

Palabras claveimplicit function theorem, Lipschitz continuity, differentiability, implicit function

© 2019 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Palabras clave
implicit function theorem, Lipschitz continuity, differentiability, implicit function